awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' L
inst_10 : IsScalarTower F L' L
inst_11 : Algebra L' E
inst_12 : IsScalarTower F L' E
inst_13 : IsScalarTower L' L E
h :
  Eq (α := L' →ₐ[F] E) (IsScalarTower.toAlgHom F L' E)
    (AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L))
⊢ LE.le (α := Subalgebra F E) (AlgHom.range (IsScalarTower.toAlgHom F L' E))
    (AlgHom.range (IsScalarTower.toAlgHom F L E))

Tactic:
convert! AlgHom.range_comp_le_range (IsScalarTower.toAlgHom F L' L) (IsScalarTower.toAlgHom F L E)

Premises used: AlgHom.range_comp_le_range, IsScalarTower.toAlgHom
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' L
inst_10 : IsScalarTower F L' L
inst_11 : Algebra L' E
inst_12 : IsScalarTower F L' E
inst_13 : IsScalarTower L' L E
h :
  ∀ (x : L'),
    Eq.{v + 1} (α := E) ((IsScalarTower.toAlgHom F L' E : (a : L') → E) x : E)
      ((AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L) : (a : L') → E) x : E)
⊢ Eq (α := L' →ₐ[F] E) (IsScalarTower.toAlgHom F L' E)
    (AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L))

Tactic:
ext
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' L
inst_10 : IsScalarTower F L' L
inst_11 : Algebra L' E
inst_12 : IsScalarTower F L' E
inst_13 : IsScalarTower L' L E
x : L'
⊢ Eq.{v + 1} (α := E) ((IsScalarTower.toAlgHom F L' E : (a : L') → E) x : E)
    ((AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L) : (a : L') → E) x : E)

Tactic:
IsScalarTower.algebraMap_apply L' L E _

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' L
inst_10 : IsScalarTower F L' L
inst_11 : Algebra L' E
inst_12 : IsScalarTower F L' E
inst_13 : IsScalarTower L' L E
x : L'
⊢ Eq.{v + 1} (α := E) ((IsScalarTower.toAlgHom F L' E : (a : L') → E) x : E)
    ((AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L) : (a : L') → E) x : E)

Tactic:
exact IsScalarTower.algebraMap_apply L' L E _

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B A' B' : IntermediateField F E
H : A.LinearDisjoint ↥B
hA : A' ≤ A
hB : B' ≤ B
⊢ A'.LinearDisjoint ↥B'

Tactic:
H.of_le_left hA |>.of_le_right hB

Premises used: IntermediateField.LinearDisjoint.of_le_right, IntermediateField.LinearDisjoint.of_le_left
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
A' : IntermediateField F E
H : A.LinearDisjoint L
hA : A' ≤ A
L' : Type u_1
inst_7 : Field L'
inst_8 : Algebra F L'
inst_9 : Algebra L' L
inst_10 : IsScalarTower F L' L
inst_11 : Algebra L' E
inst_12 : IsScalarTower F L' E
inst_13 : IsScalarTower L' L E
⊢ A'.LinearDisjoint L'

Tactic:
H.of_le_left hA |>.of_le_right' L'

Premises used: IntermediateField.LinearDisjoint.of_le_left, IntermediateField.LinearDisjoint.of_le_right'
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
H : A.LinearDisjoint ↥B
⊢ A ⊓ B = ⊥

Tactic:
toSubalgebra_injective (linearDisjoint_iff'.1 H).inf_eq_bot

Premises used: Subalgebra.LinearDisjoint.inf_eq_bot, IntermediateField.linearDisjoint_iff', IntermediateField.toSubalgebra_injective, Iff.mp
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
H : A.LinearDisjoint ↥A
⊢ A = ⊥

Tactic:
inf_idem A ▸ H.inf_eq_bot

Premises used: Eq.rec, IntermediateField.LinearDisjoint.inf_eq_bot, inf_idem
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
H : A.LinearDisjoint ↥B
⊢ Module.rank F ↥(A ⊔ B) = Module.rank F ↥A * Module.rank F ↥B

Tactic:
have h := le_sup_toSubalgebra A B
  (rank_sup_le A B).antisymm <|
    (linearDisjoint_iff'.1 H).rank_sup_of_free.ge.trans <|
      (Subalgebra.inclusion h).toLinearMap.rank_le_of_injective (Subalgebra.inclusion_injective h)

Premises used: AlgHom.toLinearMap, Eq.ge, Subalgebra.LinearDisjoint.rank_sup_of_free, IntermediateField.linearDisjoint_iff', LE.le.antisymm, LinearMap.rank_le_of_injective, Subalgebra.inclusion, Subalgebra.inclusion_injective, Iff.mp, IntermediateField.rank_sup_le, LE.le.trans, IntermediateField.le_sup_toSubalgebra
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
H : A.LinearDisjoint ↥B
⊢ finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B

Tactic:
simpa only [map_mul] using congr(Cardinal.toNat $(H.rank_sup))

Premises used: map_mul
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : FiniteDimensional.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥B
H : finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B
rwa rwa₁ rwa₂ rwa₃ :
  finrank.{u, v} F ↥(A ⊔ B).toSubalgebra = finrank.{u, v} F ↥A.toSubalgebra * finrank.{u, v} F ↥B.toSubalgebra
⊢ finrank.{u, v} F ↥(A.toSubalgebra ⊔ B.toSubalgebra) =
    finrank.{u, v} F ↥A.toSubalgebra * finrank.{u, v} F ↥B.toSubalgebra

Tactic:
rwa [← sup_toSubalgebra_of_left]

Premises used: IntermediateField.sup_toSubalgebra_of_left
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : Module.Finite.{u, v} F ↥A
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
⊢ finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B

Tactic:
have := h₁.finrank_sup
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : Module.Finite.{u, v} F ↥A
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
this : finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B
rwa : ∀ (this : finrank.{u, v} F ↥⊤ = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B), finrank (↥A) E = finrank.{u, v} F ↥B
rwa₁ : ∀ (this : finrank F E = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B), finrank (↥A) E = finrank.{u, v} F ↥B
rwa₂ :
  ∀ (this : finrank.{u, v} F ↥A * finrank (↥A) E = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B),
    finrank (↥A) E = finrank.{u, v} F ↥B
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : finrank (↥A) E = finrank.{u, v} F ↥B), finrank (↥A) E = finrank.{u, v} F ↥B
⊢ finrank (↥A) E = finrank.{u, v} F ↥B

Tactic:
rwa [h₂, finrank_top', ← finrank_mul_finrank F A E, mul_right_inj' finrank_pos.ne'] at this

Premises used: Membership.mem, Subtype, LT.lt.ne', IntermediateField.finrank_top', Module.finrank_mul_finrank, mul_right_inj', Module.finrank_pos
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : Module.Finite.{u, v} F ↥B
h₁ : A.LinearDisjoint ↥B
h₂ rwa rwa₁ rwa₂ rwa₃ : A ⊔ B = ⊤
⊢ B ⊔ A = ⊤

Tactic:
rwa [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
H : finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B
⊢ A.LinearDisjoint ↥B

Tactic:
apply LinearDisjoint.of_finrank_sup

Premises used: IntermediateField.LinearDisjoint.of_finrank_sup
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
H : finrank (↥B) E = finrank.{u, v} F ↥A
⊢ finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B

Tactic:
rw [h₁, finrank_top', ← Module.finrank_mul_finrank F B E, mul_comm, mul_left_inj'
    Module.finrank_pos.ne']

Premises used: Membership.mem, Subtype, LT.lt.ne', IntermediateField.finrank_top', Module.finrank_mul_finrank, mul_comm, mul_left_inj', Module.finrank_pos
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ IsGalois (↥B) E

Tactic:
have : IsGalois B E := IsGalois.sup_right A B h₁
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
this : IsGalois (↥B) E
H : Nat.card.{v} Gal(E/↥B) = Nat.card.{v} Gal(↥A/F)
⊢ finrank (↥B) E = finrank.{u, v} F ↥A

Tactic:
rw [← IsGalois.card_aut_eq_finrank, ← IsGalois.card_aut_eq_finrank]

Premises used: IsGalois.card_aut_eq_finrank
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
this : IsGalois (↥B) E
⊢ Nat.card.{v} Gal(E/↥B) = Nat.card.{v} Gal(↥A/F)

Tactic:
Nat.card_congr <| Equiv.ofBijective (restrictRestrictAlgEquivMapHom _ _ _ _)
    ⟨restrictRestrictAlgEquivMapHom_injective _ _ h₁,
      restrictRestrictAlgEquivMapHom_surjective _ _ h₂⟩

Premises used: IntermediateField.restrictRestrictAlgEquivMapHom_surjective, IntermediateField.restrictRestrictAlgEquivMapHom_injective, Nat.card_congr, And.intro, Equiv.ofBijective, IntermediateField.restrictRestrictAlgEquivMapHom, DFunLike.coe
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
this : IsGalois (↥B) E
⊢ Nat.card.{v} Gal(E/↥B) = Nat.card.{v} Gal(↥A/F)

Tactic:
exact Nat.card_congr <| Equiv.ofBijective (restrictRestrictAlgEquivMapHom _ _ _ _)
    ⟨restrictRestrictAlgEquivMapHom_injective _ _ h₁,
      restrictRestrictAlgEquivMapHom_surjective _ _ h₂⟩

Premises used: IntermediateField.restrictRestrictAlgEquivMapHom_surjective, IntermediateField.restrictRestrictAlgEquivMapHom_injective, Nat.card_congr, And.intro, Equiv.ofBijective, IntermediateField.restrictRestrictAlgEquivMapHom, DFunLike.coe
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
⊢ IntermediateField.map C.val A' = A

Tactic:
have hA : IntermediateField.map C.val A' = A := lift_restrict le_sup_left
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
⊢ IntermediateField.map C.val B' = B

Tactic:
have hB : IntermediateField.map C.val B' = B := lift_restrict le_sup_right
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
suffices : A'.LinearDisjoint ↥B'
⊢ A.LinearDisjoint ↥B

Tactic:
suffices A'.LinearDisjoint B' from hA ▸ hB ▸ LinearDisjoint.map this C.val
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
rw : lift (A' ⊔ B') = lift (F := C) ⊤
rw₁ : lift (A' ⊔ B') = C
rw₂ : lift A' ⊔ lift B' = C
rw₃ : A ⊔ lift B' = C
rw₄ rw₅ : A ⊔ B = C
⊢ A' ⊔ B' = ⊤

Tactic:
rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]

Premises used: IntermediateField.lift_inj, le_sup_left, IntermediateField.lift_top, le_sup_right, IntermediateField.lift_sup, IntermediateField.lift_restrict
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
⊢ A' ⊔ B' = ⊤

Tactic:
have h₁ : A' ⊔ B' = ⊤ := by
    rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
rw : lift (A' ⊓ B') = lift (F := C) ⊥
rw₁ : lift (A' ⊓ B') = ⊥
rw₂ : lift A' ⊓ lift B' = ⊥
rw₃ : A ⊓ lift B' = ⊥
rw₄ : A ⊓ B = ⊥
rw₅ rw₆ : Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊥
⊢ A' ⊓ B' = ⊥

Tactic:
rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]

Premises used: IntermediateField.lift_inj, le_sup_left, IntermediateField.lift_inf, le_sup_right, IntermediateField.lift_bot, IntermediateField.lift_restrict
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
⊢ A' ⊓ B' = ⊥

Tactic:
have h₂ : A' ⊓ B' = ⊥ := by
    rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
h₂ : A' ⊓ B' = ⊥
⊢ IsGalois.{u, v} F ↥A'

Tactic:
have : IsGalois F A' := IsGalois.of_algEquiv <| restrict_algEquiv ..
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
h₂ : A' ⊓ B' = ⊥
this : IsGalois.{u, v} F ↥A'
⊢ A'.LinearDisjoint ↥B'

Tactic:
of_inf_eq_bot_aux h₁ h₂

Premises used: _private.0.IntermediateField.LinearDisjoint.of_inf_eq_bot_aux
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
h₂ : A' ⊓ B' = ⊥
this : IsGalois.{u, v} F ↥A'
⊢ A'.LinearDisjoint ↥B'

Tactic:
exact of_inf_eq_bot_aux h₁ h₂

Premises used: _private.0.IntermediateField.LinearDisjoint.of_inf_eq_bot_aux
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
inst_3 : IsGalois.{u, v} F ↥A
inst_4 : FiniteDimensional.{u, v} F ↥A
inst_5 : FiniteDimensional.{u, v} F ↥B
⊢ A.LinearDisjoint ↥B ↔ A ⊓ B = ⊥

Tactic:
⟨fun h ↦ inf_eq_bot h, fun h ↦ of_inf_eq_bot h⟩

Premises used: IntermediateField.LinearDisjoint.inf_eq_bot, IntermediateField.LinearDisjoint.of_inf_eq_bot, Iff.intro
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank F ↥A

Tactic:
Eq.trans ?_ (Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left H)

Premises used: Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left, Eq.trans
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
refine :
  Module.rank L ↥(adjoin L (↑A : Set E)) =
    Module.rank ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))
      ↥(Algebra.adjoin ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)) (↑A.toSubalgebra : Set E))
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank F ↥A

Tactic:
refine Eq.trans ?_ (Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left H)

Premises used: Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left, Eq.trans
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
set :
  let L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E);
  Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank ↥L' ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) =
    Module.rank ↥(AlgHom.range (IsScalarTower.toAlgHom F L E))
      ↥(Algebra.adjoin ↥(AlgHom.range (IsScalarTower.toAlgHom F L E)) (↑A.toSubalgebra : Set E))

Tactic:
set L' := (IsScalarTower.toAlgHom F L E).range

Premises used: IsScalarTower.toAlgHom, AlgHom.range
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
rw :
  Eq (α := Subsemiring E)
    (Subsemiring.closure (Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E) ∪ (↑A : Set E)))
    (Subsemiring.closure (Set.range (ι := ↥L') (⇑(algebraMap (↥L') E) : (a : ↥L') → E) ∪ (↑A : Set E)))
⊢ Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))

Tactic:
rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring]

Premises used: IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic, Or.symm, Algebra.adjoin_toSubsemiring
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
e_s :
  Eq (α := Set E) (Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E))
    (Set.range (ι := ↥L') (⇑(algebraMap (↥L') E) : (a : ↥L') → E))
⊢ Eq (α := Subsemiring E)
    (Subsemiring.closure (Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E) ∪ (↑A : Set E)))
    (Subsemiring.closure (Set.range (ι := ↥L') (⇑(algebraMap (↥L') E) : (a : ↥L') → E) ∪ (↑A : Set E)))

Tactic:
congr 2
-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
i : AlgEquiv.{u, w, v} F L ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
e_s :
  ∀ (x : E),
    Membership.mem (γ := Set E) (Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E)) x ↔
      Membership.mem (γ := Set E) (Set.range (ι := ↥L') (⇑(algebraMap (↥L') E) : (a : ↥L') → E)) x
⊢ Eq (α := Set E) (Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E))
    (Set.range (ι := ↥L') (⇑(algebraMap (↥L') E) : (a : ↥L') → E))

Tactic:
ext x