K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
⊢ F = E
apply eq_of_le_of_finrank_le h_le
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
have h1 := finrank_mul_finrank K F L
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
h2 : finrank K { x // x ∈ E } * finrank { x // x ∈ E } L = finrank K L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
have h2 := finrank_mul_finrank K E L
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
h2 : finrank K { x // x ∈ E } * finrank { x // x ∈ E } L = finrank K L
h3 : 0 < finrank { x // x ∈ E } L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
h2 : finrank K { x // x ∈ E } * finrank { x // x ∈ E } L = finrank K L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
have h3 : 0 < finrank E L := finrank_pos
no goals
K : Type u_1
L : Type u_2
L' : Type ?u.284724
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S F E : IntermediateField K L
inst✝ : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank { x // x ∈ F } L ≤ finrank { x // x ∈ E } L
h1 : finrank K { x // x ∈ F } * finrank { x // x ∈ F } L = finrank K L
h2 : finrank K { x // x ∈ E } * finrank { x // x ∈ E } L = finrank K L
h3 : 0 < finrank { x // x ∈ E } L
⊢ finrank K { x // x ∈ E } ≤ finrank K { x // x ∈ F }
nlinarith