K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
let S1 := E1.toSubalgebra
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
let S2 := E2.toSubalgebra
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
⊢ ∀ (x : L), x ∈ S1 ⊔ S2 → x⁻¹ ∈ S1 ⊔ S2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
refine'
  le_antisymm
    (show _ ≤ (S1 ⊔ S2).toIntermediateField _ from
      sup_le (show S1 ≤ _ from le_sup_left) (show S2 ≤ _ from le_sup_right))
    (le_sup_toSubalgebra E1 E2)
no goals
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
⊢ IsField { x // x ∈ S1 ⊔ S2 }
exact
  isField_of_isIntegral_of_isField'
    (isIntegral_sup.mpr ⟨Algebra.isIntegral_of_finite K E1, Algebra.isIntegral_of_finite K E2⟩)
    (Field.toIsField K)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
⊢ x⁻¹ ∈ S1 ⊔ S2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
⊢ ∀ (x : L), x ∈ S1 ⊔ S2 → x⁻¹ ∈ S1 ⊔ S2
intro x hx
case pos
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
hx' : { val := x, property := hx } = 0
⊢ x⁻¹ ∈ S1 ⊔ S2

case neg
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
hx' : ¬{ val := x, property := hx } = 0
⊢ x⁻¹ ∈ S1 ⊔ S2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
⊢ x⁻¹ ∈ S1 ⊔ S2
by_cases hx' : (⟨x, hx⟩ : (S1 ⊔ S2 : Subalgebra K L)) = 0
case pos
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
hx' : { val := x, property := hx } = 0
⊢ 0 ∈ S1 ⊔ S2
case pos
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
hx' : { val := x, property := hx } = 0
⊢ x⁻¹ ∈ S1 ⊔ S2
rw [← Subtype.coe_mk x, hx', Subalgebra.coe_zero, inv_zero]
no goals
case pos
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
hx' : { val := x, property := hx } = 0
⊢ 0 ∈ S1 ⊔ S2
exact (S1 ⊔ S2).zero_mem
case neg.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
hx' : ¬{ val := x, property := hx } = 0
y : { x // x ∈ S1 ⊔ S2 }
h : { val := x, property := hx } * y = 1
⊢ x⁻¹ ∈ S1 ⊔ S2
case neg
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h1 : FiniteDimensional K { x // x ∈ E1 }
h2 : FiniteDimensional K { x // x ∈ E2 }
S1 : Subalgebra K L := E1.toSubalgebra
S2 : Subalgebra K L := E2.toSubalgebra
this : IsField { x // x ∈ S1 ⊔ S2 }
x : L
hx : x ∈ S1 ⊔ S2
hx' : ¬{ val := x, property := hx } = 0
⊢ x⁻¹ ∈ S1 ⊔ S2
obtain ⟨y, h⟩ := this.mul_inv_cancel hx'