awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
rw : (↑(m.uniformBell x_1) : A) * hI.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
rw₁ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
rw₂ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = hI'.dpow m (hI'.dpow x_1 x)
⊢ hI.dpow m (hI.dpow x_1 x) = hI'.dpow m (hI.dpow x_1 x)
have rw₃ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x
Tactic: rw [hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
⊢ hI.dpow m (hI'.dpow x_1 x) = hI'.dpow m (hI'.dpow x_1 x)
have rw : hI.dpow m (hI.dpow x_1 x) = hI'.dpow m (hI.dpow x_1 x)
Tactic: rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
rw : hI.dpow m (hI.dpow x_1 x) = hI'.dpow m (hI.dpow x_1 x)
⊢ hI.dpow m (hI'.dpow x_1 x) = hI'.dpow m (hI'.dpow x_1 x)
have rw₁ : (↑(m.uniformBell x_1) : A) * hI.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
Tactic: rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
rw : hI.dpow m (hI.dpow x_1 x) = hI'.dpow m (hI.dpow x_1 x)
rw₁ : (↑(m.uniformBell x_1) : A) * hI.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
⊢ hI.dpow m (hI'.dpow x_1 x) = hI'.dpow m (hI'.dpow x_1 x)
have rw₂ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
Tactic: rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
rw : hI.dpow m (hI.dpow x_1 x) = hI'.dpow m (hI.dpow x_1 x)
rw₁ : (↑(m.uniformBell x_1) : A) * hI.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
rw₂ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
⊢ hI.dpow m (hI'.dpow x_1 x) = hI'.dpow m (hI'.dpow x_1 x)
have rw₃ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = hI'.dpow m (hI'.dpow x_1 x)
Tactic: rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
x_1 : ℕ
hn : x_1 ≠ 0
x : A
hx : x ∈ hI.dpEqualizer hI'
m : ℕ
rw : hI.dpow m (hI.dpow x_1 x) = hI'.dpow m (hI.dpow x_1 x)
rw₁ : (↑(m.uniformBell x_1) : A) * hI.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
rw₂ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = hI'.dpow m (hI.dpow x_1 x)
rw₃ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = hI'.dpow m (hI'.dpow x_1 x)
⊢ hI.dpow m (hI'.dpow x_1 x) = hI'.dpow m (hI'.dpow x_1 x)
have rw₄ : (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x = (↑(m.uniformBell x_1) : A) * hI'.dpow (m * x_1) x
Tactic: rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'
have rw : (⇑f : (a : A) → B) '' (↑I : Set A) ⊆ (↑(hK.dpEqualizer hK') : Set B)
Tactic: rw [Ideal.map, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ (↑I : Set A)
n : ℕ
⊢ hK.dpow n ((f : (a : A) → B) a) = hK'.dpow n ((f : (a : A) → B) a)
have rw : (f : (a : A) → B) (hI.dpow n a) = hK'.dpow n ((f : (a : A) → B) a)
Tactic: rw [hIK.2 a ha, hIK'.2 a ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
a : A
ha : a ∈ (↑I : Set A)
n : ℕ
rw : (f : (a : A) → B) (hI.dpow n a) = hK'.dpow n ((f : (a : A) → B) a)
⊢ hK.dpow n ((f : (a : A) → B) a) = hK'.dpow n ((f : (a : A) → B) a)
have rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow n a) : B) ((f : (a : A) → B) (hI.dpow n a) : B)
Tactic: rw [hIK.2 a ha, hIK'.2 a ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A_1 : Type u_1
inst : CommSemiring A_1
I_1 : Ideal A_1
hI_1 hI' : DividedPowers I_1
A : Type u_2
inst_1 : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (A := A ⧸ J) (Ideal.map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x : ℕ
hn : x ≠ 0
a : A
h : a ∈ J ⊓ I
haJ : a ∈ (↑J : Set A)
haI : a ∈ (↑I : Set A)
⊢ hI.dpow x a ∈ J ⊓ I
have refine : hI.dpow x a ∈ (↑J : Set A)
Tactic: refine ⟨?_, hI.dpow_mem hn haI⟩
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A_1 : Type u_1
inst : CommSemiring A_1
I_1 : Ideal A_1
hI_1 hI' : DividedPowers I_1
A : Type u_2
inst_1 : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (A := A ⧸ J) (Ideal.map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x : ℕ
hn : x ≠ 0
a : A
h : a ∈ J ⊓ I
haJ : a ∈ (↑J : Set A)
haI : a ∈ (↑I : Set A)
⊢ hI.dpow x a ∈ (↑J : Set A)
have rw : hJ.dpow x ((φ.toRingHom : (a : A) → A ⧸ J) a) = 0
Tactic: rw [SetLike.mem_coe, ← Quotient.eq_zero_iff_mem, ← hφ, ← φ.dpow_comp a haI]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A_1 : Type u_1
inst : CommSemiring A_1
I_1 : Ideal A_1
hI_1 hI' : DividedPowers I_1
A : Type u_2
inst_1 : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (A := A ⧸ J) (Ideal.map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x : ℕ
hn : x ≠ 0
a : A
h : a ∈ J ⊓ I
haJ : a ∈ (↑J : Set A)
haI : a ∈ (↑I : Set A)
ha0 : Eq (α := A ⧸ J) ((φ.toRingHom : (a : A) → A ⧸ J) a : A ⧸ J) (0 : A ⧸ J)
⊢ hJ.dpow x ((φ.toRingHom : (a : A) → A ⧸ J) a) = 0
have rw : hJ.dpow x 0 = 0
Tactic: rw [ha0, hJ.dpow_eval_zero hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A_1 : Type u_1
inst : CommSemiring A_1
I_1 : Ideal A_1
hI_1 hI' : DividedPowers I_1
A : Type u_2
inst_1 : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (A := A ⧸ J) (Ideal.map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x : ℕ
hn : x ≠ 0
a : A
h : a ∈ J ⊓ I
haJ : a ∈ (↑J : Set A)
haI : a ∈ (↑I : Set A)
ha0 : Eq (α := A ⧸ J) ((φ.toRingHom : (a : A) → A ⧸ J) a : A ⧸ J) (0 : A ⧸ J)
rw : hJ.dpow x 0 = 0
⊢ hJ.dpow x ((φ.toRingHom : (a : A) → A ⧸ J) a) = 0
have rw₁ : Eq.{u_2 + 1} (α := A ⧸ J) 0 0
Tactic: rw [ha0, hJ.dpow_eval_zero hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A_1 : Type u_1
inst : CommSemiring A_1
I_1 : Ideal A_1
hI_1 hI' : DividedPowers I_1
A : Type u_2
inst_1 : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (A := A ⧸ J) (Ideal.map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x : ℕ
hn : x ≠ 0
a : A
h : a ∈ J ⊓ I
haJ : a ∈ (↑J : Set A)
haI : a ∈ (↑I : Set A)
⊢ hJ.dpow x ((φ.toRingHom : (a : A) → A ⧸ J) a) = 0
have suffices : Eq (α := A ⧸ J) ((φ.toRingHom : (a : A) → A ⧸ J) a : A ⧸ J) (0 : A ⧸ J)
Tactic: suffices ha0 : φ.toRingHom a = 0 by
      rw [ha0, hJ.dpow_eval_zero hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A_1 : Type u_1
inst : CommSemiring A_1
I_1 : Ideal A_1
hI_1 hI' : DividedPowers I_1
A : Type u_2
inst_1 : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers (A := A ⧸ J) (Ideal.map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) I)
φ : hI.DPMorphism hJ
hφ : φ.toRingHom = Ideal.Quotient.mk J
x : ℕ
hn : x ≠ 0
a : A
h : a ∈ J ⊓ I
haJ : a ∈ (↑J : Set A)
haI : a ∈ (↑I : Set A)
⊢ Eq (α := A ⧸ J) ((φ.toRingHom : (a : A) → A ⧸ J) a : A ⧸ J) (0 : A ⧸ J)
have rw : a ∈ J
Tactic: rw [hφ, Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ dpow hI f n x = 0
have hnc : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
Tactic: rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
⊢ dpow hI f n x = 0
have rw : Eq (α := B)
  (Function.extend (fun (a : ↥I) ↦ (f : (a : A) → B) (↑a : A)) (fun (a : ↥I) ↦ (f : (a : A) → B) (hI.dpow n (↑a : A))) 0
    x)
  0
Tactic: classical
    rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
rw :
  Eq (α := B)
    (Function.extend (fun (a : ↥I) ↦ (f : (a : A) → B) (↑a : A)) (fun (a : ↥I) ↦ (f : (a : A) → B) (hI.dpow n (↑a : A)))
      0 x)
    0
⊢ dpow hI f n x = 0
have rw₁ : Eq.{u_2 + 1} (α := B)
  (if h : ∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x then
    (f : (a : A) → B) (hI.dpow n (↑(Classical.choose (p := fun (x_1 : ↥I) ↦ (f : (a : A) → B) (↑x_1 : A) = x) h) : A))
  else 0 x)
  0
Tactic: classical
    rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
rw :
  Eq (α := B)
    (Function.extend (fun (a : ↥I) ↦ (f : (a : A) → B) (↑a : A)) (fun (a : ↥I) ↦ (f : (a : A) → B) (hI.dpow n (↑a : A)))
      0 x)
    0
rw₁ :
  Eq.{u_2 + 1} (α := B)
    (if h : ∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x then
      (f : (a : A) → B) (hI.dpow n (↑(Classical.choose (p := fun (x_1 : ↥I) ↦ (f : (a : A) → B) (↑x_1 : A) = x) h) : A))
    else 0 x)
    0
⊢ dpow hI f n x = 0
have rw₂ : Eq.{u_2 + 1} (α := B) (0 x) 0
Tactic: classical
    rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
rw :
  Eq (α := B)
    (Function.extend (fun (a : ↥I) ↦ (f : (a : A) → B) (↑a : A)) (fun (a : ↥I) ↦ (f : (a : A) → B) (hI.dpow n (↑a : A)))
      0 x)
    0
rw₁ :
  Eq.{u_2 + 1} (α := B)
    (if h : ∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x then
      (f : (a : A) → B) (hI.dpow n (↑(Classical.choose (p := fun (x_1 : ↥I) ↦ (f : (a : A) → B) (↑x_1 : A) = x) h) : A))
    else 0 x)
    0
rw₂ : Eq.{u_2 + 1} (α := B) (0 x) 0
⊢ dpow hI f n x = 0
have hnc : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
Tactic: classical
    rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
rw :
  Eq (α := B)
    (Function.extend (fun (a : ↥I) ↦ (f : (a : A) → B) (↑a : A)) (fun (a : ↥I) ↦ (f : (a : A) → B) (hI.dpow n (↑a : A)))
      0 x)
    0
rw₁ :
  Eq.{u_2 + 1} (α := B)
    (if h : ∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x then
      (f : (a : A) → B) (hI.dpow n (↑(Classical.choose (p := fun (x_1 : ↥I) ↦ (f : (a : A) → B) (↑x_1 : A) = x) h) : A))
    else 0 x)
    0
rw₂ : Eq.{u_2 + 1} (α := B) (0 x) 0
hnc : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
⊢ dpow hI f n x = 0
have rw₃ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: classical
    rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hx' : x ∉ J
rw :
  Eq (α := B)
    (Function.extend (fun (a : ↥I) ↦ (f : (a : A) → B) (↑a : A)) (fun (a : ↥I) ↦ (f : (a : A) → B) (hI.dpow n (↑a : A)))
      0 x)
    0
rw₁ :
  Eq.{u_2 + 1} (α := B)
    (if h : ∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x then
      (f : (a : A) → B) (hI.dpow n (↑(Classical.choose (p := fun (x_1 : ↥I) ↦ (f : (a : A) → B) (↑x_1 : A) = x) h) : A))
    else 0 x)
    0
rw₂ : Eq.{u_2 + 1} (α := B) (0 x) 0
hnc : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
rw₃ : Eq.{u_2 + 1} (α := B) 0 0
hnc₁ : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
rw₄ : Eq.{u_2 + 1} (α := B) 0 0
hnc₂ hnc₃ : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
⊢ dpow hI f n x = 0
have hnc₄ : ∀ (a : A) (ha : a ∈ I) (hx' : ((f : (a : A) → B) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ I) a ha) : A) : B) ∉ J), False
Tactic: classical
    rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)
Cleared hypotheses: x, hx'
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
⊢ dpow hI f 0 x = 1
have obtain : ∀ (a : A) (ha : a ∈ I) (hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)), dpow hI f 0 ((f : (a : A) → B) a) = 1
Tactic: obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
⊢ dpow hI f 0 ((f : (a : A) → B) a) = 1
have rw : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow 0 a) : B) (1 : B)
Tactic: rw [dpow_apply' hI hIf ha, hI.dpow_zero ha, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow 0 a) : B) (1 : B)
⊢ dpow hI f 0 ((f : (a : A) → B) a) = 1
have rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
Tactic: rw [dpow_apply' hI hIf ha, hI.dpow_zero ha, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow 0 a) : B) (1 : B)
rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
⊢ dpow hI f 0 ((f : (a : A) → B) a) = 1
have rw₂ : Eq.{u_2 + 1} (α := B) 1 1
Tactic: rw [dpow_apply' hI hIf ha, hI.dpow_zero ha, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
⊢ dpow hI f 1 x = x
have obtain : ∀ (a : A) (ha : a ∈ I) (hax : (f : (a : A) → B) a = x), dpow hI f 1 x = x
Tactic: obtain ⟨a, ha, hax⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : (f : (a : A) → B) a = x
⊢ dpow hI f 1 x = x
have rw : dpow hI f 1 ((f : (a : A) → B) a) = (f : (a : A) → B) a
Tactic: rw [← hax, dpow_apply' hI hIf ha, hI.dpow_one ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : (f : (a : A) → B) a = x
rw : dpow hI f 1 ((f : (a : A) → B) a) = (f : (a : A) → B) a
⊢ dpow hI f 1 x = x
have rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow 1 a) : B) ((f : (a : A) → B) a : B)
Tactic: rw [← hax, dpow_apply' hI hIf ha, hI.dpow_one ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : (f : (a : A) → B) a = x
rw : dpow hI f 1 ((f : (a : A) → B) a) = (f : (a : A) → B) a
rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow 1 a) : B) ((f : (a : A) → B) a : B)
⊢ dpow hI f 1 x = x
have rw₂ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) a : B)
Tactic: rw [← hax, dpow_apply' hI hIf ha, hI.dpow_one ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ dpow hI f n x ∈ J
have rw : ∀ (hx : Membership.mem (γ := Ideal B) (Ideal.map f I) x), Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n x)
Tactic: rw [hIJ] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x : B
hn : n ≠ 0
hx : Membership.mem (γ := Ideal B) (Ideal.map f I) x
⊢ Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n x)
have obtain : ∀ (a : A) (ha : a ∈ I)
  (hx : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) a : B)),
  Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n ((f : (a : A) → B) a))
Tactic: obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) a : B)
⊢ Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n ((f : (a : A) → B) a))
have rw : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) (hI.dpow n a) : B)
Tactic: rw [dpow_apply' hI hIf ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x y : B
hx : x ∈ J
hy : y ∈ J
⊢ dpow hI f n (x + y) = ∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, dpow hI f k.1 x * dpow hI f k.2 y
have obtain : ∀ (a : A) (ha : a ∈ I) (hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)),
  dpow hI f n (HAdd.hAdd (α := B) ((f : (a : A) → B) a : B) y) =
    ∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, dpow hI f k.1 ((f : (a : A) → B) a) * dpow hI f k.2 y
Tactic: obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
Cleared hypotheses: x, hx