awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
e_a : Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) 1 : Ft) : K) (1 : K)
⊢ Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)
have e_a₁ : Eq.{u_2 + 1} (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) 1 : K) (1 : K)
Tactic: refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
e_a : Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) 1 : Ft) : K) (1 : K)
e_a₁ : Eq.{u_2 + 1} (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) 1 : K) (1 : K)
⊢ Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)
have e_a₂ : ∀ (a b : F⟮X⟯),
  (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) (a * b) : Ft) =
    HMul.hMul (α := K) (β := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) a : Ft) : K)
      ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) b : Ft) : K)
Tactic: refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
e_a : Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) 1 : Ft) : K) (1 : K)
e_a₁ : Eq.{u_2 + 1} (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) 1 : K) (1 : K)
e_a₂ :
  ∀ (a b : F⟮X⟯),
    (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) (a * b) : Ft) =
      HMul.hMul (α := K) (β := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) a : Ft) : K)
        ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) b : Ft) : K)
⊢ Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)
have e_a₃ : ∀ (a b : F⟮X⟯),
  (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) (a * b) =
    HMul.hMul (α := K) (β := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) a : K)
      ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) b : K)
Tactic: refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
e_a : Eq.{u_2 + 1} (α := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) 1 : Ft) : K) (1 : K)
e_a₁ : Eq.{u_2 + 1} (α := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) 1 : K) (1 : K)
e_a₂ :
  ∀ (a b : F⟮X⟯),
    (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) (a * b) : Ft) =
      HMul.hMul (α := K) (β := K) ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) a : Ft) : K)
        ((algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) b : Ft) : K)
e_a₃ :
  ∀ (a b : F⟮X⟯),
    (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) (a * b) =
      HMul.hMul (α := K) (β := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) a : K)
        ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) b : K)
⊢ Eq (α := (x : F⟮X⟯) → K) (fun (c : F⟮X⟯) ↦ (algebraMap Ft K : (a : Ft) → K) ((e : (a : F⟮X⟯) → Ft) c : Ft))
    (⇑(algebraMap F⟮X⟯ K) : (a : F⟮X⟯) → K)
have e_a₄ : ∀ (a : F[X]),
  Eq.{u_2 + 1} (α := K)
    ((algebraMap Ft K : (a : Ft) → K)
        ((e : (a : F⟮X⟯) → Ft) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) a : F⟮X⟯) : Ft) :
      K)
    ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) a : F⟮X⟯) : K)
Tactic: refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
⊢ FunctionField F K ↔ FiniteDimensional Ft K
have this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
Tactic: have : ∀ (c) (x : K), e c • x = c • x := by
    intro c x
    rw [Algebra.smul_def, Algebra.smul_def]
    congr
    refine congr_fun (f := fun c => algebraMap Ft K (e c)) ?_ c
    refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
      simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
⊢ FunctionField F K ↔ FiniteDimensional Ft K
have mp : FunctionField F K → FiniteDimensional Ft K
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
mp : FunctionField F K → FiniteDimensional Ft K
⊢ FunctionField F K ↔ FiniteDimensional Ft K
have mpr : FiniteDimensional Ft K → FunctionField F K
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
⊢ FunctionField F K
have mpr : ∀ (c : Ft) (x : K), HSMul.hSMul.{u_1, u_2, u_2} (α := F⟮X⟯) ((e.symm.toRingEquiv : (a : Ft) → F⟮X⟯) c : F⟮X⟯) x = c • x
Tactic: refine (b.mapCoeffs e.symm ?_).finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
c : Ft
x : K
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := F⟮X⟯) ((e.symm.toRingEquiv : (a : Ft) → F⟮X⟯) c : F⟮X⟯) x = c • x
have h₁ : c = (e : (a : F⟮X⟯) → Ft) ((e.symm : (a : Ft) → F⟮X⟯) c : F⟮X⟯)
Tactic: convert! (this (e.symm c) x).symm
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
have rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K)
  (⇑(@RingHom.comp _ F⟮X⟯ _ _ Semiring.toNonAssocSemiring _ (algebraMap F⟮X⟯ K) (algebraMap F[X] F⟮X⟯)) :
    (a : F[X]) → K)
Tactic: rw [IsScalarTower.algebraMap_eq F[X] F⟮X⟯ K]
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := ↥(ringOfIntegers F K))
    (⇑(algebraMap F[X] ↥(ringOfIntegers F K)) : (a : F[X]) → ↥(ringOfIntegers F K))
have hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
Tactic: have hinj : Function.Injective (algebraMap F[X] K) := by
    rw [IsScalarTower.algebraMap_eq F[X] F⟮X⟯ K]
    exact (algebraMap F⟮X⟯ K).injective.comp (IsFractionRing.injective F[X] F⟮X⟯)
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := ↥(ringOfIntegers F K))
    (⇑(algebraMap F[X] ↥(ringOfIntegers F K)) : (a : F[X]) → ↥(ringOfIntegers F K))
have rw : ∀ (a : F[X]),
  Eq.{u_2 + 1} (α := ↥(ringOfIntegers F K))
      ((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) a : ↥(ringOfIntegers F K))
      (0 : ↥(ringOfIntegers F K)) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero (algebraMap F[X] (↥(ringOfIntegers F K)))]
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
p : F[X]
hp :
  Eq.{u_2 + 1} (α := ↥(ringOfIntegers F K))
    ((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p : ↥(ringOfIntegers F K))
    (0 : ↥(ringOfIntegers F K))
⊢ p = 0
have hp₁ : Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0
Tactic: rw [← Subtype.coe_inj, Subalgebra.coe_zero] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
p : F[X]
hp : Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0
⊢ p = 0
have rw : ∀ (hinj : ∀ (a : F[X]), Eq.{u_2 + 1} (α := K) ((algebraMap F[X] K : (a : F[X]) → K) a : K) (0 : K) → a = 0) (p : F[X])
  (hp :
    Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0),
  p = 0
Tactic: rw [injective_iff_map_eq_zero (algebraMap F[X] K)] at hinj
Cleared hypotheses: hinj, p, hp
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (hypothesis)
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
⊢ FiniteDimensional (↥Fyx) K
have this₁ : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
Tactic: have := FiniteDimensional.adjoin_algebraMap_X (F := F) (K := K)
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (goal)
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this_7 : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
⊢ FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯)) K
have rw : FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)) K
Tactic: rw [adjoin_simple_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.FunctionField (hypothesis)
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this_7 : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
⊢ FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)) K
have this₁ : IsScalarTower (↥F⟮x⟯) (↥Fxy) K
Tactic: have : IsScalarTower F⟮x⟯ Fxy K := isScalarTower_mid' F⟮x⟯⟮y⟯
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))) = gaussSum χ ψ
have simp : Eq.{v + 1} (α := R')
  (∑ i : R,
    HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R')
      (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') ((↑a : R) * i) : R')))
  (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))
Tactic: simp only [gaussSum, mulShift_apply, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ Eq.{v + 1} (α := R')
    (∑ i : R,
      HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R')
        (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') ((↑a : R) * i) : R')))
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))
have simp_rw : Eq.{v + 1} (α := R')
  (∑ x : R,
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') ((↑a : R) * x) : R') ((ψ : (a : R) → R') ((↑a : R) * x) : R'))
  (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') a : R') ((ψ : (a : R) → R') a : R'))
Tactic: simp_rw [← mul_assoc, ← map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ gaussSum χ (ψ.mulShift (↑a : R)) = HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R') (gaussSum χ ψ)
have rw : gaussSum χ (ψ.mulShift (↑a : R)) =
  HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R')
    (HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))))
Tactic: rw [← gaussSum_mulShift χ ψ a, inv_apply_eq_inv,
    Ring.inverse_mul_cancel_left _ _ (a.isUnit.map χ)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
rw :
  gaussSum χ (ψ.mulShift (↑a : R)) =
    HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))))
⊢ gaussSum χ (ψ.mulShift (↑a : R)) = HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R') (gaussSum χ ψ)
have rw₁ : gaussSum χ (ψ.mulShift (↑a : R)) =
  HMul.hMul (α := R') (Ring.inverse ((χ : (a : R) → R') (↑a : R)) : R')
    (HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))))
Tactic: rw [← gaussSum_mulShift χ ψ a, inv_apply_eq_inv,
    Ring.inverse_mul_cancel_left _ _ (a.isUnit.map χ)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
rw :
  gaussSum χ (ψ.mulShift (↑a : R)) =
    HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))))
rw₁ :
  gaussSum χ (ψ.mulShift (↑a : R)) =
    HMul.hMul (α := R') (Ring.inverse ((χ : (a : R) → R') (↑a : R)) : R')
      (HMul.hMul (α := R') ((χ : (a : R) → R') (↑a : R) : R') (gaussSum χ (ψ.mulShift (↑a : R))))
⊢ gaussSum χ (ψ.mulShift (↑a : R)) = HMul.hMul (α := R') ((χ⁻¹ : (a : R) → R') (↑a : R) : R') (gaussSum χ ψ)
have rw₂ : gaussSum χ (ψ.mulShift (↑a : R)) = gaussSum χ (ψ.mulShift (↑a : R))
Tactic: rw [← gaussSum_mulShift χ ψ a, inv_apply_eq_inv,
    Ring.inverse_mul_cancel_left _ _ (a.isUnit.map χ)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ gaussSum χ ψ * gaussSum φ ψ =
    ∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R')
have rw : Eq.{v + 1} (α := R')
  (∑ i : R,
    ∑ j : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
        HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
  (∑ t : R,
    ∑ x : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
        ((ψ : (a : R) → R') t : R'))
Tactic: rw [gaussSum, gaussSum, sum_mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
| Eq.{v + 1} (α := R')
    (∑ i : R,
      ∑ j : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
have h : ∀ (x x_1 : R),
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R') *
    HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') x_1 : R') ((ψ : (a : R) → R') x_1 : R')
Tactic: enter [1, 2, x, 2, x_1]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x x_1 : R
| HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') x : R') *
    HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') x_1 : R') ((ψ : (a : R) → R') x_1 : R')
have h : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
  HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R')
Tactic: rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
| Eq.{v + 1} (α := R')
    (∑ i : R,
      ∑ j : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
have h : ∀ (x x_1 : R),
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
    HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R')
Tactic: enter [1, 2, x, 2, x_1]; rw [mul_mul_mul_comm]