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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
⊢ ∃ (x : Finset ι) (x_1 : ι → S) (_ :
    Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0
have h : ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
  (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
Tactic: use s
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
have h : ∀ (a : K) (hag : ∀ i ∈ s, IsLocalization.IsInteger R (a * g i)) (j : ι) (hjs : j ∈ s)
  (hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)),
  ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
Tactic: obtain ⟨a, hag, j, hjs, hgI⟩ := Ideal.exist_integer_multiples_notMem hRS s g hj's hj'g
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
hag : ∀ i ∈ s, IsLocalization.IsInteger R (a * g i)
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
have h : ∀ (g'' : (i : ι) → i ∈ s → R) (hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i),
  ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
Tactic: choose g'' hg'' using hag
Cleared hypotheses: hag
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
have hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
Tactic: have hg' : ∀ i ∈ s, algebraMap _ _ (g' i) = a * g i := by
    intro i hi; exact (congr_arg _ (dif_pos hi)).trans (hg'' i hi)
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
have hgI₁ : ∀ (x : R), (algebraMap R K : (a : R) → K) x = a * g j → x ∉ RingHom.ker (F := R →+* S) f
Tactic: simp only [FractionalIdeal.mem_coeIdeal, not_exists, not_and'] at hgI
Cleared hypotheses: hgI
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
have hgI₁ : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
Tactic: have hgI : algebraMap R S (g' j) ≠ 0 := by
    simp only [FractionalIdeal.mem_coeIdeal, not_exists, not_and'] at hgI
    exact hgI _ (hg' j hjs)
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
have h : Eq.{u_4 + 1} (α := V')
  (∑ i ∈ s,
    HSMul.hSMul.{v, u_4, u_4} (α := S) (β := V') ((fun (i : ι) ↦ ((f : (a : R) → S) (g' i) : S)) i)
      (((⇑f' : (a : V'') → V') ∘ b) i))
  0
Tactic: refine ⟨fun i => algebraMap R S (g' i), ?_, j, hjs, hgI⟩
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := V) ((F : (a : V'') → V) (∑ i ∈ s, g' i • b i) : V) (0 : V)
have rw : Eq.{u_3 + 1} (α := V) (∑ x ∈ s, (F : (a : V'') → V) (g' x • b x))
  (∑ x ∈ s, a • HSMul.hSMul (β := V) (g x) (((⇑F : (a : V'') → V) ∘ b) x))
Tactic: rw [map_sum, ← smul_zero a, ← eq, Finset.smul_sum]
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := V) (∑ x ∈ s, (F : (a : V'') → V) (g' x • b x))
    (∑ x ∈ s, a • HSMul.hSMul (β := V) (g x) (((⇑F : (a : V'') → V) ∘ b) x))
have refine : ∀ x ∈ s, (F : (a : V'') → V) (g' x • b x) = a • HSMul.hSMul (β := V) (g x) (((⇑F : (a : V'') → V) ∘ b) x)
Tactic: refine Finset.sum_congr rfl ?_
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
i : ι
hi : i ∈ s
⊢ (F : (a : V'') → V) (g' i • b i) = a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
have rw : HSMul.hSMul (β := V) (g' i) ((F : (a : V'') → V) (b i) : V) =
  a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
Tactic: rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_apply]
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
i : ι
hi : i ∈ s
rw :
  HSMul.hSMul (β := V) (g' i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
⊢ (F : (a : V'') → V) (g' i • b i) = a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := K) (β := V) ((algebraMap R K : (a : R) → K) (g' i) : K)
    ((F : (a : V'') → V) (b i) : V) =
  a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
Tactic: rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_apply]
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
i : ι
hi : i ∈ s
rw :
  HSMul.hSMul (β := V) (g' i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := K) (β := V) ((algebraMap R K : (a : R) → K) (g' i) : K)
      ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
⊢ (F : (a : V'') → V) (g' i • b i) = a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
have rw₂ : HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
  a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
Tactic: rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_apply]
-- 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
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
i : ι
hi : i ∈ s
rw :
  HSMul.hSMul (β := V) (g' i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := K) (β := V) ((algebraMap R K : (a : R) → K) (g' i) : K)
      ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₂ :
  HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
⊢ (F : (a : V'') → V) (g' i • b i) = a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
have rw₃ : HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
  HSMul.hSMul (β := V) (a • g i) (((⇑F : (a : V'') → V) ∘ b) i)
Tactic: rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_apply]