awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
inst_3 : Finite ι
S : ι → IntermediateField F E
h : ∀ (i : ι), (S i).FG
⊢ FG.{u_1, u_2} (F := F) (E := E) (⨆ (i : ι), S i)
have choose : ∀ (s : (i : ι) → Finset E) (hs : ∀ (i : ι), adjoin F (↑(s i) : Set E) = S i),
  FG.{u_1, u_2} (F := F) (E := E) (⨆ (i : ι), S i)
Tactic: choose s hs using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
inst_3 : Finite ι
S : ι → IntermediateField F E
s : (i : ι) → Finset E
hs : ∀ (i : ι), adjoin F (↑(s i) : Set E) = S i
⊢ FG.{u_1, u_2} (F := F) (E := E) (⨆ (i : ι), S i)
have simp_rw : FG.{u_1, u_2} (E := E) (adjoin F (⋃ (i : ι), (↑(s i) : Set E)))
Tactic: simp_rw [← hs, ← adjoin_iUnion]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ P (adjoin F (↑S : Set E))
have refine_1 : P (adjoin F (↑∅ : Set E))
Tactic: refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
refine_1 : P (adjoin F (↑∅ : Set E))
⊢ P (adjoin F (↑S : Set E))
have refine_2 : ∀ (x : E) (x_1 : Finset E) (ha : x ∈ S),
  x_1 ⊆ S → x ∉ x_1 → ∀ (h : P (adjoin F (↑x_1 : Set E))), P (adjoin F (↑(insert x x_1) : Set E))
Tactic: refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
x : E
x_1 : Finset E
ha : x ∈ S
h_1 : x_1 ⊆ S
h_2 : x ∉ x_1
h : P (adjoin F (↑x_1 : Set E))
⊢ P (adjoin F (↑(insert x x_1) : Set E))
have refine_2 : P (restrictScalars F (L' := ↥(adjoin F (↑x_1 : Set E))) (↥(adjoin F (↑x_1 : Set E)))⟮x⟯)
Tactic: rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ P (adjoin F (↑S : Set E))
have refine_1 : P (adjoin F (↑∅ : Set E))
Tactic: classical
  refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
  · simp [base]
  · rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]
    exact ih (adjoin F _) _ ha h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
refine_1 : P (adjoin F (↑∅ : Set E))
⊢ P (adjoin F (↑S : Set E))
have refine_2 : ∀ (x : E) (x_1 : Finset E) (ha : x ∈ S),
  x_1 ⊆ S → x ∉ x_1 → ∀ (h : P (adjoin F (↑x_1 : Set E))), P (adjoin F (↑(insert x x_1) : Set E))
Tactic: classical
  refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
  · simp [base]
  · rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]
    exact ih (adjoin F _) _ ha h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
K : IntermediateField F E
hK : K.FG
⊢ P K
have obtain : ∀ (S : Finset E), P (adjoin F (↑S : Set E))
Tactic: obtain ⟨S, rfl⟩ := hK
Cleared hypotheses: K, hK
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
L : Type u_2
inst : Field L
F : Subfield L
⊢ extendScalars ⋯ = ⊥
have h : ∀ (x : L), x ∈ extendScalars sorry ↔ Membership.mem (γ := IntermediateField (↥F) L) ⊥ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
L : Type u_2
inst : Field L
F : Subfield L
x : L
⊢ x ∈ extendScalars ⋯ ↔ Membership.mem (γ := IntermediateField (↥F) L) ⊥ x
have h : x ∈ F ↔ Membership.mem (γ := Set L) (Set.range (ι := ↥F) (⇑(algebraMap (↥F) L) : (a : ↥F) → L)) x
Tactic: rw [mem_extendScalars, IntermediateField.mem_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Defs (goal)
Goal:
L : Type u_2
inst : Field L
F : Subfield L
x : L
⊢ x ∈ F ↔ Membership.mem (γ := Set L) (Set.range (ι := ↥F) (⇑(algebraMap (↥F) L) : (a : ↥F) → L)) x
have h : Membership.mem (γ := Set L) (Set.range (ι := ↥F) (⇑(algebraMap (↥F) L) : (a : ↥F) → L)) x → x ∈ F
Tactic: refine ⟨fun h ↦ ⟨⟨x, h⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ F = E
have apply : finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
Tactic: apply eq_of_le_of_finrank_le h_le
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
have h1 : finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L
Tactic: have h1 := finrank_mul_finrank K F L
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L
⊢ finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
have h2 : finrank.{u_1, u_2} K ↥E * finrank (↥E) L = finrank K L
Tactic: have h2 := finrank_mul_finrank K E L
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L
h2 : finrank.{u_1, u_2} K ↥E * finrank (↥E) L = finrank K L
⊢ finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
have h3 : 0 < finrank (↥E) L
Tactic: have h3 : 0 < finrank E L := finrank_pos
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L
h2 : finrank.{u_1, u_2} K ↥E * finrank (↥E) L = finrank K L
h3 : 0 < finrank (↥E) L
⊢ finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
have nlinarith : finrank.{u_1, u_2} K ↥F < finrank.{u_1, u_2} K ↥E →
  -1 + -(HMul.hMul (α := ℤ) (↑(finrank.{u_1, u_2} K ↥F) : ℤ) (↑(finrank (↥F) L) : ℤ) - (↑(finrank K L) : ℤ)) +
            (HMul.hMul (α := ℤ) (↑(finrank.{u_1, u_2} K ↥E) : ℤ) (↑(finrank (↥E) L) : ℤ) - (↑(finrank K L) : ℤ)) +
          (HAdd.hAdd (α := ℤ) 0 1 - (↑(finrank (↥E) L) : ℤ)) +
        (0 -
          HSub.hSub (α := ℤ) 0 (↑(finrank (↥E) L) : ℤ) *
            (HAdd.hAdd (α := ℤ) (↑(finrank.{u_1, u_2} K ↥F) : ℤ) 1 - (↑(finrank.{u_1, u_2} K ↥E) : ℤ))) +
      (0 -
        HSub.hSub (α := ℤ) 0 (↑(finrank.{u_1, u_2} K ↥F) : ℤ) *
          HSub.hSub (α := ℤ) (↑(finrank (↥F) L) : ℤ) (↑(finrank (↥E) L) : ℤ)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ F = E
have refine : ∀ (l : L) (hl : l ∈ E), l ∈ F
Tactic: refine le_antisymm h_le (fun l hl ↦ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
⊢ l ∈ F
have rwa : l ∈ extendScalars sorry
Tactic: rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
    ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
rwa : l ∈ extendScalars ⋯
⊢ l ∈ F
have rwa₁ : l ∈ extendScalars h_le
Tactic: rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
    ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
⊢ finrank (↥E) L < finrank (↥F) L
have this₁ : IsScalarTower (↥F) (↥E) L
Tactic: have : IsScalarTower F E L := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L < finrank (↥F) L
have refine_1 : finrank (↥E) L ≤ finrank (↥F) L
Tactic: refine lt_of_le_of_ne ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
refine_1 : finrank (↥E) L ≤ finrank (↥F) L
⊢ finrank (↥E) L < finrank (↥F) L
have refine_2 : finrank (↥E) L ≠ finrank (↥F) L
Tactic: refine lt_of_le_of_ne ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Algebraic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : Algebra ↥F ↥E := (inclusion h).toAlgebra
⊢ finrank (↥E) L ∣ finrank (↥F) L
have this : IsScalarTower (↥F) (↥E) L
Tactic: have : IsScalarTower F E L := IsScalarTower.of_algebraMap_eq fun x ↦ rfl
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
⊢ (S.toIntermediateField inv_mem).toSubalgebra = S
have h : ∀ (x : L), x ∈ (S.toIntermediateField inv_mem).toSubalgebra ↔ x ∈ S
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ S.toIntermediateField ⋯ = S
have h : ∀ (x : L), x ∈ S.toIntermediateField sorry ↔ x ∈ S
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
⊢ x⁻¹ ∈ S
have pos : ∀ (hx0 : x = 0), x⁻¹ ∈ S
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
pos : ∀ (hx0 : x = 0), x⁻¹ ∈ S
⊢ x⁻¹ ∈ S
have neg : ∀ (hx0 : ¬x = 0), x⁻¹ ∈ S
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : x = 0
⊢ x⁻¹ ∈ S
have pos : 0 ∈ S
Tactic: rw [hx0, inv_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
⊢ x⁻¹ ∈ S
have neg : ∀ (y : ↥S) (hy : Subtype.mk (p := fun (x : L) ↦ x ∈ S) x hx * y = 1), x⁻¹ ∈ S
Tactic: obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0 from Subtype.coe_ne_coe.1 hx0)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : Subtype.mk (p := fun (x : L) ↦ x ∈ S) x hx * y = 1
⊢ x⁻¹ ∈ S
have hy₁ : x⁻¹ = (↑y : L)
Tactic: rw [Subtype.ext_iff, S.coe_mul, S.coe_one, Subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
⊢ (S.toIntermediateField' hS).toSubalgebra = S
have h : ∀ (x : L), x ∈ (S.toIntermediateField' hS).toSubalgebra ↔ x ∈ S
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ S.toIntermediateField' ⋯ = S
have h : ∀ (x : L), x ∈ S.toIntermediateField' sorry ↔ x ∈ S
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L'
x : L
hx : x ∈ (Subalgebra.comap f S.toSubalgebra).carrier
⊢ Membership.mem (α := L') S ((f : (a : L) → L') x⁻¹ : L')
have rw : Membership.mem (α := L') S (((f : (a : L) → L') x)⁻¹ : L')
Tactic: rw [map_inv₀ f x]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ a₂ : IntermediateField K L
h : a₁.toSubalgebra = a₂.toSubalgebra
⊢ a₁ = a₂
have h₁ : ∀ (x : L), x ∈ a₁ ↔ x ∈ a₂
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ a₂ : IntermediateField K L
h : a₁.toSubfield = a₂.toSubfield
⊢ a₁ = a₂
have h₁ : ∀ (x : L), x ∈ a₁ ↔ x ∈ a₂
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a₁ a₂ : IntermediateField K L
h : a₁.toSubfield = a₂.toSubfield
x : L
⊢ x ∈ a₁ ↔ x ∈ a₂
have h₁ : x ∈ a₁.toSubfield ↔ x ∈ a₂.toSubfield
Tactic: simp_rw [← mem_toSubfield, h]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
a₁ a₂ : IntermediateField K L
h : map f a₁ = map f a₂
⊢ a₁ = a₂
have rwa : ∀ (h : (map f a₁).toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
Tactic: rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
a₁ a₂ : IntermediateField K L
h : map f a₁ = map f a₂
rwa : ∀ (h : (map f a₁).toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
⊢ a₁ = a₂
have rwa₁ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
Tactic: rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
a₁ a₂ : IntermediateField K L
h : map f a₁ = map f a₂
rwa : ∀ (h : (map f a₁).toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
rwa₁ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
⊢ a₁ = a₂
have rwa₂ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = Subalgebra.map f a₂.toSubalgebra), a₁ = a₂
Tactic: rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
a₁ a₂ : IntermediateField K L
h : map f a₁ = map f a₂
rwa : ∀ (h : (map f a₁).toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
rwa₁ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
rwa₂ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = Subalgebra.map f a₂.toSubalgebra), a₁ = a₂
⊢ a₁ = a₂
have rwa₃ : ∀ (h : a₁.toSubalgebra = a₂.toSubalgebra), a₁ = a₂
Tactic: rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
a₁ a₂ : IntermediateField K L
h : map f a₁ = map f a₂
rwa : ∀ (h : (map f a₁).toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
rwa₁ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = (map f a₂).toSubalgebra), a₁ = a₂
rwa₂ : ∀ (h : Subalgebra.map f a₁.toSubalgebra = Subalgebra.map f a₂.toSubalgebra), a₁ = a₂
rwa₃ : ∀ (h : a₁.toSubalgebra = a₂.toSubalgebra), a₁ = a₂
⊢ a₁ = a₂
have rwa₄ : ∀ (h : a₁ = a₂), a₁ = a₂
Tactic: rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
hx : Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L)) x
⊢ Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L)) x
have rwa : ∃ (y : K), (algebraMap K L : (a : K) → L) y = x
Tactic: rwa [Set.mem_range, ← RingHom.mem_fieldRange]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
U V : IntermediateField L' L
H : Eq (α := IntermediateField K L) (restrictScalars K U) (restrictScalars K V)
x : L
⊢ x ∈ U ↔ x ∈ V
have rw : Membership.mem (γ := IntermediateField K L) (restrictScalars K U) x ↔ x ∈ V
Tactic: rw [← mem_restrictScalars K, H, mem_restrictScalars]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
U V : IntermediateField L' L
H : Eq (α := IntermediateField K L) (restrictScalars K U) (restrictScalars K V)
x : L
rw : Membership.mem (γ := IntermediateField K L) (restrictScalars K U) x ↔ x ∈ V
⊢ x ∈ U ↔ x ∈ V
have rw₁ : Membership.mem (γ := IntermediateField K L) (restrictScalars K V) x ↔ x ∈ V
Tactic: rw [← mem_restrictScalars K, H, mem_restrictScalars]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
inst_5 : Algebra L' L
inst_6 : IsScalarTower K L' L
U V : IntermediateField L' L
H : Eq (α := IntermediateField K L) (restrictScalars K U) (restrictScalars K V)
x : L
rw : Membership.mem (γ := IntermediateField K L) (restrictScalars K U) x ↔ x ∈ V
rw₁ : Membership.mem (γ := IntermediateField K L) (restrictScalars K V) x ↔ x ∈ V
⊢ x ∈ U ↔ x ∈ V
have rw₂ : x ∈ V ↔ x ∈ V
Tactic: rw [← mem_restrictScalars K, H, mem_restrictScalars]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_6
inst_3 : Field K
inst_4 : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra
have rw : (f.comp L.val).fieldRange.toSubalgebra = Subalgebra.map f L.toSubalgebra
Tactic: rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_6
inst_3 : Field K
inst_4 : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
rw : (f.comp L.val).fieldRange.toSubalgebra = Subalgebra.map f L.toSubalgebra
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra
have rw₁ : (f.comp L.val).range = Subalgebra.map f L.toSubalgebra
Tactic: rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_6
inst_3 : Field K
inst_4 : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
rw : (f.comp L.val).fieldRange.toSubalgebra = Subalgebra.map f L.toSubalgebra
rw₁ : (f.comp L.val).range = Subalgebra.map f L.toSubalgebra
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra
have rw₂ : Subalgebra.map f L.val.range = Subalgebra.map f L.toSubalgebra
Tactic: rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]