awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
h : (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 0
⊢ (f : (a : A) → B) (hI.dpow (n + 1) 0) = hJ.dpow (n + 1) 0
have succ : (f : (a : A) → B) 0 = hJ.dpow (n + 1) 0
Tactic: rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
h : (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 0
succ : (f : (a : A) → B) 0 = hJ.dpow (n + 1) 0
⊢ (f : (a : A) → B) (hI.dpow (n + 1) 0) = hJ.dpow (n + 1) 0
have succ₁ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B)
Tactic: rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
h : (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 0
succ : (f : (a : A) → B) 0 = hJ.dpow (n + 1) 0
succ₁ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B)
⊢ (f : (a : A) → B) (hI.dpow (n + 1) 0) = hJ.dpow (n + 1) 0
have succ₂ : Eq.{u_4 + 1} (α := B) 0 0
Tactic: rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
⊢ (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 0
have zero : (f : (a : A) → B) (hI.dpow 0 0) = hJ.dpow 0 0
Tactic: induction n with
    | zero => rw [hI.dpow_zero I.zero_mem, hJ.dpow_zero J.zero_mem, map_one]
    | succ n => rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
n : ℕ
zero : (f : (a : A) → B) (hI.dpow 0 0) = hJ.dpow 0 0
⊢ (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 0
have succ : ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 0 → (f : (a : A) → B) (hI.dpow (n + 1) 0) = hJ.dpow (n + 1) 0
Tactic: induction n with
    | zero => rw [hI.dpow_zero I.zero_mem, hJ.dpow_zero J.zero_mem, map_one]
    | succ n => rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
⊢ Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} (r • x)
have refine : ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
Tactic: refine ⟨I.smul_mem r hx.1, (fun n ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
n : ℕ
⊢ (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
have rw : (f : (a : A) → B) (hI.dpow n (r * x)) = hJ.dpow n ((f : (a : A) → B) (r * x))
Tactic: rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
n : ℕ
rw : (f : (a : A) → B) (hI.dpow n (r * x)) = hJ.dpow n ((f : (a : A) → B) (r * x))
⊢ (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
have rw₁ : (f : (a : A) → B) (r ^ n * hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) (r * x))
Tactic: rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
n : ℕ
rw : (f : (a : A) → B) (hI.dpow n (r * x)) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₁ : (f : (a : A) → B) (r ^ n * hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) (r * x))
⊢ (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
have rw₂ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
  hJ.dpow n ((f : (a : A) → B) (r * x))
Tactic: rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
n : ℕ
rw : (f : (a : A) → B) (hI.dpow n (r * x)) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₁ : (f : (a : A) → B) (r ^ n * hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₂ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n ((f : (a : A) → B) (r * x))
⊢ (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
have rw₃ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
  hJ.dpow n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r : B) ((f : (a : A) → B) x : B))
Tactic: rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
n : ℕ
rw : (f : (a : A) → B) (hI.dpow n (r * x)) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₁ : (f : (a : A) → B) (r ^ n * hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₂ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n ((f : (a : A) → B) (r * x))
rw₃ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r : B) ((f : (a : A) → B) x : B))
⊢ (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
have rw₄ : HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) r : B) n) ((f : (a : A) → B) (hI.dpow n x) : B) =
  hJ.dpow n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r : B) ((f : (a : A) → B) x : B))
Tactic: rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
n : ℕ
rw : (f : (a : A) → B) (hI.dpow n (r * x)) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₁ : (f : (a : A) → B) (r ^ n * hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₂ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n ((f : (a : A) → B) (r * x))
rw₃ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r : B) ((f : (a : A) → B) x : B))
rw₄ :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) r : B) n) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r : B) ((f : (a : A) → B) x : B))
⊢ (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
have rw₅ : HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) r : B) n) ((f : (a : A) → B) (hI.dpow n x) : B) =
  HPow.hPow (α := B) ((f : (a : A) → B) r : B) n * hJ.dpow n ((f : (a : A) → B) x)
Tactic: rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx :
  Membership.mem (γ := Set A)
    {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)} x
n : ℕ
rw : (f : (a : A) → B) (hI.dpow n (r * x)) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₁ : (f : (a : A) → B) (r ^ n * hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) (r * x))
rw₂ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n ((f : (a : A) → B) (r * x))
rw₃ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (r ^ n) : B) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r : B) ((f : (a : A) → B) x : B))
rw₄ :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) r : B) n) ((f : (a : A) → B) (hI.dpow n x) : B) =
    hJ.dpow n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) r : B) ((f : (a : A) → B) x : B))
rw₅ :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) r : B) n) ((f : (a : A) → B) (hI.dpow n x) : B) =
    HPow.hPow (α := B) ((f : (a : A) → B) r : B) n * hJ.dpow n ((f : (a : A) → B) x)
⊢ (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • x))
have rw₆ : HPow.hPow (α := B) ((f : (a : A) → B) r : B) n * hJ.dpow n ((f : (a : A) → B) x) =
  HPow.hPow (α := B) ((f : (a : A) → B) r : B) n * hJ.dpow n ((f : (a : A) → B) x)
Tactic: rw [smul_eq_mul, hI.dpow_mul hx.1, map_mul, map_mul, map_pow,
      hJ.dpow_mul (hf (mem_map_of_mem f hx.1)), hx.2 n]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (hypothesis)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
x : A
hx : x ∈ I
⊢ hJ.dpow n ((f : (a : A) → B) x) = (f : (a : A) → B) (hI.dpow n x)
have hS' : S ⊆ (↑(hI.ideal_from_ringHom hJ hf) : Set A)
Tactic: have hS' : S ⊆ ideal_from_ringHom hI hJ hf := fun y hy ↦ by
      simp only [mem_coe, ideal_from_ringHom, Submodule.mem_mk]
      exact ⟨hS ▸ subset_span hy, fun n => h y hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (hypothesis)
Goal:
A_1 : Type u_1
B_1 : Type u_2
inst : CommSemiring A_1
inst_1 : CommSemiring B_1
I_1 : Ideal A_1
J_1 : Ideal B_1
hI_1 : DividedPowers I_1
hJ_1 : DividedPowers J_1
A : Type u_3
B : Type u_4
inst_2 : CommSemiring A
inst_3 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
x : A
hx : x ∈ I
hS' : S ⊆ (↑(hI.ideal_from_ringHom hJ hf) : Set A)
⊢ hJ.dpow n ((f : (a : A) → B) x) = (f : (a : A) → B) (hI.dpow n x)
have hS'₁ : I ≤ hI.ideal_from_ringHom hJ hf
Tactic: rw [← span_le, ← hS] at hS'
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, Membership.mem (α := B) J ((f : (a : A) → B) s : B)
hdp : ∀ {n : ℕ}, ∀ a ∈ S, (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
h : map f I ≤ J
n : ℕ
a : A
ha : a ∈ I
⊢ hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
have rw : hJ.dpow n (((fromGens hI hJ (S := S) hS h sorry).toRingHom : (a : A) → B) a) =
  ((fromGens hI hJ (S := S) hS h sorry).toRingHom : (a : A) → B) (hI.dpow n a)
Tactic: rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, Membership.mem (α := B) J ((f : (a : A) → B) s : B)
hdp : ∀ {n : ℕ}, ∀ a ∈ S, (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
h : map f I ≤ J
n : ℕ
a : A
ha : a ∈ I
rw :
  hJ.dpow n (((fromGens hI hJ (S := S) hS h ⋯).toRingHom : (a : A) → B) a) =
    ((fromGens hI hJ (S := S) hS h ⋯).toRingHom : (a : A) → B) (hI.dpow n a)
⊢ hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
have rw₁ : Eq.{u_4 + 1} (α := B) (((fromGens hI hJ (S := S) hS h sorry).toRingHom : (a : A) → B) (hI.dpow n a) : B)
  (((fromGens hI hJ (S := S) hS h sorry).toRingHom : (a : A) → B) (hI.dpow n a) : B)
Tactic: rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, Membership.mem (α := B) J ((f : (a : A) → B) s : B)
hdp : ∀ {n : ℕ}, ∀ a ∈ S, (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
⊢ hI.IsDPMorphism hJ f
have suffices : map f I ≤ J
Tactic: suffices h : I.map f ≤ J by
    exact ⟨h, fun a ha ↦ by
      rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, Membership.mem (α := B) J ((f : (a : A) → B) s : B)
hdp : ∀ {n : ℕ}, ∀ a ∈ S, (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
⊢ map f I ≤ J
have rw : (⇑f : (a : A) → B) '' S ⊆ (↑J : Set B)
Tactic: rw [hS, map_span, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
⊢ hJ.IsDPMorphism hK g
have hS' : ∀ (s : B),
  Membership.mem (γ := Set B) ((⇑f : (a : A) → B) '' (↑I : Set A)) s →
    Membership.mem (α := C) K ((g : (a : B) → C) s : C)
Tactic: apply on_span _ _ heq
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
hS' :
  ∀ (s : B),
    Membership.mem (γ := Set B) ((⇑f : (a : A) → B) '' (↑I : Set A)) s →
      Membership.mem (α := C) K ((g : (a : B) → C) s : C)
⊢ hJ.IsDPMorphism hK g
have hdp : ∀ {n : ℕ} (a : B),
  Membership.mem (γ := Set B) ((⇑f : (a : A) → B) '' (↑I : Set A)) a →
    (g : (a : B) → C) (hJ.dpow n a) = hK.dpow n ((g : (a : B) → C) a)
Tactic: apply on_span _ _ heq
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
a : A
ha : a ∈ (↑I : Set A)
⊢ Membership.mem (α := C) K ((g : (a : B) → C) ((f : (a : A) → B) a : B) : C)
have hS' : Membership.mem (α := C) K ((g.comp f : (a : A) → C) a : C)
Tactic: rw [← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ (↑I : Set A)
⊢ (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g : (a : B) → C) ((f : (a : A) → B) a : B))
have hdp : (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g.comp f : (a : A) → C) a)
Tactic: rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ (↑I : Set A)
hdp : (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g.comp f : (a : A) → C) a)
⊢ (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g : (a : B) → C) ((f : (a : A) → B) a : B))
have hdp₁ : Eq.{u_5 + 1} (α := C) ((g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) : C)
  ((g.comp f : (a : A) → C) (hI.dpow n a) : C)
Tactic: rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ (↑I : Set A)
hdp : (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g.comp f : (a : A) → C) a)
hdp₁ :
  Eq.{u_5 + 1} (α := C) ((g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) : C)
    ((g.comp f : (a : A) → C) (hI.dpow n a) : C)
⊢ (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g : (a : B) → C) ((f : (a : A) → B) a : B))
have hdp₂ : Eq.{u_5 + 1} (α := C) ((g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) : C)
  ((g : (a : B) → C) ((f : (a : A) → B) (hI.dpow n a) : B) : C)
Tactic: rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ (↑I : Set A)
hdp : (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g.comp f : (a : A) → C) a)
hdp₁ :
  Eq.{u_5 + 1} (α := C) ((g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) : C)
    ((g.comp f : (a : A) → C) (hI.dpow n a) : C)
hdp₂ :
  Eq.{u_5 + 1} (α := C) ((g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) : C)
    ((g : (a : B) → C) ((f : (a : A) → B) (hI.dpow n a) : B) : C)
⊢ (g : (a : B) → C) (hJ.dpow n ((f : (a : A) → B) a)) = hK.dpow n ((g : (a : B) → C) ((f : (a : A) → B) a : B))
have hdp₃ : Eq.{u_5 + 1} (α := C) ((g : (a : B) → C) ((f : (a : A) → B) (hI.dpow n a) : B) : C)
  ((g : (a : B) → C) ((f : (a : A) → B) (hI.dpow n a) : B) : C)
Tactic: rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]