awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
⊢ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)
have rw : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p (Submodule.map M.mkQ ⊤)
Tactic: rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
rw : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p (Submodule.map M.mkQ ⊤)
⊢ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)
have rw₁ : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p (LinearMap.range M.mkQ)
Tactic: rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
rw : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p (Submodule.map M.mkQ ⊤)
rw₁ : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p (LinearMap.range M.mkQ)
⊢ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)
have rw₂ : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤
Tactic: rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
⊢ Eq.{v + 1} (α := Submodule R (S ⧸ M)) (Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)) ⊤
have rw : Eq.{v + 1} (α := Submodule R (S ⧸ M)) (Submodule.map M.mkQ (Submodule.restrictScalars R (map (F := R →+* S) f p))) ⊤
Tactic: rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
rw :
  Eq.{v + 1} (α := Submodule R (S ⧸ M)) (Submodule.map M.mkQ (Submodule.restrictScalars R (map (F := R →+* S) f p))) ⊤
⊢ Eq.{v + 1} (α := Submodule R (S ⧸ M)) (Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)) ⊤
have rw₁ : Eq.{v + 1} (α := Submodule R (S ⧸ M)) ⊤ ⊤
Tactic: rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
⊢ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
have p₁ : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)
Tactic: calc
      p • ⊤ = Submodule.map M.mkQ (p • ⊤) := by
        rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
      _ = ⊤ := by rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
p₁ : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)
⊢ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
have p₂ : Eq.{v + 1} (α := Submodule R (S ⧸ M)) (Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)) ⊤
Tactic: calc
      p • ⊤ = Submodule.map M.mkQ (p • ⊤) := by
        rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
      _ = ⊤ := by rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
have smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
Tactic: have smul_top_eq : p • (⊤ : Submodule R (S ⧸ M)) = ⊤ := by
    calc
      p • ⊤ = Submodule.map M.mkQ (p • ⊤) := by
        rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
      _ = ⊤ := by rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ HSMul.hSMul (β := Submodule R (S ⧸ M)) p (Submodule.span R (Set.range a))
have rw : Membership.mem (γ := Submodule R (S ⧸ M)) ⊤ x
Tactic: rw [ha, smul_top_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ HSMul.hSMul (β := Submodule R (S ⧸ M)) p (Submodule.span R (Set.range a))
have rw : x ∈ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤
Tactic: { rw [ha, smul_top_eq]; exact Submodule.mem_top }
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
x : S ⧸ M
rw : x ∈ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule R (S ⧸ M)) p (Submodule.span R (Set.range a))
have rw₁ : Membership.mem (γ := Submodule R (S ⧸ M)) ⊤ x
Tactic: { rw [ha, smul_top_eq]; exact Submodule.mem_top }
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
x : S ⧸ M
⊢ ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
have obtain : ∀ (a'' : Fin n →₀ R) (ha'' : ∀ (i : Fin n), Membership.mem (α := R) p ((a'' : (a : Fin n) → R) i : R))
  (hx : (a''.sum fun (i : Fin n) (c : R) ↦ c • a i) = x),
  ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
Tactic: obtain ⟨a'', ha'', hx⟩ := (Submodule.mem_ideal_smul_span_iff_exists_sum p a x).1
      (by { rw [ha, smul_top_eq]; exact Submodule.mem_top } :
        x ∈ p • Submodule.span R (Set.range a))
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
x : S ⧸ M
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), Membership.mem (α := R) p ((a'' : (a : Fin n) → R) i : R)
hx : (a''.sum fun (i : Fin n) (c : R) ↦ c • a i) = x
⊢ ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
have refine : ∑ i : Fin n, HSMul.hSMul.{u, v, v} (α := R) ((fun (i : Fin n) ↦ ((a'' : (a : Fin n) → R) i : R)) i) (a i) = x
Tactic: refine ⟨fun i => a'' i, fun i => ha'' _, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
x : S ⧸ M
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), Membership.mem (α := R) p ((a'' : (a : Fin n) → R) i : R)
hx : (a''.sum fun (i : Fin n) (c : R) ↦ c • a i) = x
⊢ ∑ i : Fin n, HSMul.hSMul.{u, v, v} (α := R) ((fun (i : Fin n) ↦ ((a'' : (a : Fin n) → R) i : R)) i) (a i) = x
have h : ∀ (i : Fin n), HSMul.hSMul.{u, v, v} (α := R) 0 (a i) = 0
Tactic: rw [← hx, Finsupp.sum_fintype]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
have exists_sum : ∀ (x : S ⧸ M), ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
Tactic: have exists_sum : ∀ x : S ⧸ M, ∃ a' : Fin n → R, (∀ i, a' i ∈ p) ∧ ∑ i, a' i • a i = x := by
    intro x
    obtain ⟨a'', ha'', hx⟩ := (Submodule.mem_ideal_smul_span_iff_exists_sum p a x).1
      (by { rw [ha, smul_top_eq]; exact Submodule.mem_top } :
        x ∈ p • Submodule.span R (Set.range a))
    · refine ⟨fun i => a'' i, fun i => ha'' _, ?_⟩
      rw [← hx, Finsupp.sum_fintype]
      exact fun _ => zero_smul _ _
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
have choose : ∀ (A' : (i : Fin n) → Fin n → R) (hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p)
  (hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i),
  Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
Tactic: choose A' hA'p hA' using fun i => exists_sum (a i)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : (i : Fin n) → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R :=
  HSub.hSub (α := Matrix (Fin n) (Fin n) R) (β := Matrix (Fin n) (Fin n) R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) A' : Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
B : Matrix (Fin n) (Fin n) R := A.adjugate
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
have A_smul : ∀ (i : Fin n), Eq.{v + 1} (α := S ⧸ M) (∑ j : Fin n, A i j • a j) 0
Tactic: have A_smul : ∀ i, ∑ j, A i j • a j = 0 := by
    intros
    simp [A, Matrix.sub_apply, Matrix.of_apply, Matrix.one_apply, sub_smul,
      Finset.sum_sub_distrib, hA', sub_self]