awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ Eq (α := L' →ₐ[F] E) (IsScalarTower.toAlgHom F L' E)
    (AlgHom.comp (IsScalarTower.toAlgHom F L E) (IsScalarTower.toAlgHom F L' L))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ finrank.{u, v} F ↥(A.toSubalgebra ⊔ B.toSubalgebra) =
    finrank.{u, v} F ↥A.toSubalgebra * finrank.{u, v} F ↥B.toSubalgebra
have rwa : finrank.{u, v} F ↥(A ⊔ B).toSubalgebra = finrank.{u, v} F ↥A.toSubalgebra * finrank.{u, v} F ↥B.toSubalgebra
Tactic: rwa [← sup_toSubalgebra_of_left]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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 (↥A) E = finrank.{u, v} F ↥B
have this : finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B
Tactic: have := h₁.finrank_sup
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ finrank (↥A) E = finrank.{u, v} F ↥B
have rwa : ∀ (this : finrank.{u, v} F ↥⊤ = finrank.{u, v} F ↥A * 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ finrank (↥A) E = finrank.{u, v} F ↥B
have rwa₁ : ∀ (this : finrank F E = finrank.{u, v} F ↥A * 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ finrank (↥A) E = finrank.{u, v} F ↥B
have 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
Tactic: rwa [h₂, finrank_top', ← finrank_mul_finrank F A E, mul_right_inj' finrank_pos.ne'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ finrank (↥A) E = finrank.{u, v} F ↥B
have rwa₃ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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 = ⊥
⊢ A.LinearDisjoint ↥B
have H : finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B
Tactic: apply LinearDisjoint.of_finrank_sup
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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 = ⊥
⊢ finrank.{u, v} F ↥(A ⊔ B) = finrank.{u, v} F ↥A * finrank.{u, v} F ↥B
have H : finrank (↥B) E = finrank.{u, v} F ↥A
Tactic: rw [h₁, finrank_top', ← Module.finrank_mul_finrank F B E, mul_comm, mul_left_inj'
    Module.finrank_pos.ne']
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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 = ⊥
⊢ finrank (↥B) E = finrank.{u, v} F ↥A
have this : IsGalois (↥B) E
Tactic: have : IsGalois B E := IsGalois.sup_right A B h₁
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ finrank (↥B) E = finrank.{u, v} F ↥A
have H : Nat.card.{v} Gal(E/↥B) = Nat.card.{v} Gal(↥A/F)
Tactic: rw [← IsGalois.card_aut_eq_finrank, ← IsGalois.card_aut_eq_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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 ⋯
⊢ A.LinearDisjoint ↥B
have hA : IntermediateField.map C.val A' = A
Tactic: have hA : IntermediateField.map C.val A' = A := lift_restrict le_sup_left
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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
⊢ A.LinearDisjoint ↥B
have hB : IntermediateField.map C.val B' = B
Tactic: have hB : IntermediateField.map C.val B' = B := lift_restrict le_sup_right
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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.LinearDisjoint ↥B
have suffices : A'.LinearDisjoint ↥B'
Tactic: suffices A'.LinearDisjoint B' from hA ▸ hB ▸ LinearDisjoint.map this C.val
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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' = ⊤
have rw : lift (A' ⊔ B') = lift (F := C) ⊤
Tactic: rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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) ⊤
⊢ A' ⊔ B' = ⊤
have rw₁ : lift (A' ⊔ B') = C
Tactic: rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ A' ⊔ B' = ⊤
have rw₂ : lift A' ⊔ lift B' = C
Tactic: rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ A' ⊔ B' = ⊤
have rw₃ : A ⊔ lift B' = C
Tactic: rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ A' ⊔ B' = ⊤
have rw₄ : A ⊔ B = C
Tactic: rw [← lift_inj, lift_top, lift_sup, lift_restrict le_sup_left, lift_restrict le_sup_right]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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'.LinearDisjoint ↥B'
have h₁ : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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' = ⊥
have rw : lift (A' ⊓ B') = lift (F := C) ⊥
Tactic: rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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) ⊥
⊢ A' ⊓ B' = ⊥
have rw₁ : lift (A' ⊓ B') = ⊥
Tactic: rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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') = ⊥
⊢ A' ⊓ B' = ⊥
have rw₂ : lift A' ⊓ lift B' = ⊥
Tactic: rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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' = ⊥
⊢ A' ⊓ B' = ⊥
have rw₃ : A ⊓ lift B' = ⊥
Tactic: rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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 = ⊥
⊢ A' ⊓ B' = ⊥
have rw₅ : Eq.{v + 1} (α := IntermediateField F E) ⊥ ⊥
Tactic: rw [← lift_inj, lift_bot, lift_inf, lift_restrict le_sup_left, lift_restrict le_sup_right, h]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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'.LinearDisjoint ↥B'
have h₂ : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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' = ⊥
⊢ A'.LinearDisjoint ↥B'
have this : IsGalois.{u, v} F ↥A'
Tactic: have : IsGalois F A' := IsGalois.of_algEquiv <| restrict_algEquiv ..
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
have 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))
Tactic: refine Eq.trans ?_ (Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left H)
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
⊢ Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))
have 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)))
Tactic: rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
⊢ 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)))
have 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))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
⊢ Eq (α := Set E) (Set.range.{v, w + 1} (ι := L) (⇑(algebraMap L E) : (a : L) → E))
    (Set.range (ι := ↥L') (⇑(algebraMap (↥L') E) : (a : ↥L') → E))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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)
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
have e_s : (∃ (y : L), (algebraMap L E : (a : L) → E) y = x) ↔
  ∃ (a : E) (b : a ∈ L'), (algebraMap (↥L') E : (a : ↥L') → E) (Subtype.mk (p := fun (a : E) ↦ a ∈ L') a b) = x
Tactic: simp only [Set.mem_range, Subtype.exists]
-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (hypothesis)
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)
⊢ Module.rank L ↥(adjoin L (↑A : Set E)) = Module.rank ↥L' ↥(Algebra.adjoin ↥L' (↑A.toSubalgebra : Set E))
have heq : Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
  (Subalgebra.toSubsemiring (R := ↥L') (Algebra.adjoin ↥L' (↑A : Set E)))
Tactic: have heq : (adjoin L (A : Set E)).toSubalgebra.toSubsemiring =
      (Algebra.adjoin L' (A : Set E)).toSubsemiring := by
    rw [adjoin_intermediateField_toSubalgebra_of_isAlgebraic _ _ halg.symm,
      Algebra.adjoin_toSubsemiring, Algebra.adjoin_toSubsemiring]
    congr 2
    ext x
    simp only [Set.mem_range, Subtype.exists]
    exact ⟨fun ⟨y, h⟩ ↦ ⟨x, ⟨y, h⟩, rfl⟩, fun ⟨a, ⟨y, h1⟩, h2⟩ ↦ ⟨y, h1.trans h2⟩⟩