awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
rw₆ 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)
⊢ (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]

Premises used: Ideal.mem_map_of_mem, map_pow, DividedPowers.dpow_mul, map_mul, And.right, And.left, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
y : A
hy : y ∈ S
⊢ Membership.mem (γ := AddSubmonoid A)
    { carrier := {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)},
      add_mem' := ⋯, zero_mem' := ⋯ }
    y

Tactic:
⟨hS ▸ subset_span hy, fun n => h y hy⟩

Premises used: Ideal.subset_span, Set.Mem, setOf, Eq.rec, And.intro, Eq.symm
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
y : A
hy : y ∈ S
⊢ Membership.mem (γ := AddSubmonoid A)
    { carrier := {x : A | x ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n x) = hJ.dpow n ((f : (a : A) → B) x)},
      add_mem' := ⋯, zero_mem' := ⋯ }
    y

Tactic:
exact ⟨hS ▸ subset_span hy, fun n => h y hy⟩
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
⊢ 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⟩
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
⊢ I ≤ hI.ideal_from_ringHom hJ hf

Tactic:
rw [← span_le, ← hS] at hS'

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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' : I ≤ hI.ideal_from_ringHom hJ hf
⊢ hJ.dpow n ((f : (a : A) → B) x) = (f : (a : A) → B) (hI.dpow n x)

Tactic:
((hS' hx).2 n).symm

Premises used: And.right, Eq.symm
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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' : I ≤ hI.ideal_from_ringHom hJ hf
⊢ hJ.dpow n ((f : (a : A) → B) x) = (f : (a : A) → B) (hI.dpow n x)

Tactic:
exact ((hS' hx).2 n).symm

Premises used: And.right, Eq.symm
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
⊢ map (F := A →+* A) (RingHom.id A) I ≤ I

Tactic:
simp only [map_id, le_refl]

Premises used: le_refl, Ideal.map_id
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
n : ℕ
x : A
h : x ∈ I
⊢ hI.dpow n ((RingHom.id A : (a : A) → A) x) = (RingHom.id A : (a : A) → A) (hI.dpow n x)

Tactic:
simp only [RingHom.id_apply]

Premises used: RingHom.id_apply
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
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)
⊢ (fromGens hI hJ (S := S) hS hf ⋯).toRingHom = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := B) (((fromGens hI hJ (S := S) hS h ⋯).toRingHom : (a : A) → B) (hI.dpow n a) : B)
    (((fromGens hI hJ (S := S) hS h ⋯).toRingHom : (a : A) → B) (hI.dpow n a) : B)
⊢ hJ.dpow n ((f : (a : A) → B) a) = (f : (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]

Premises used: DividedPowers.DPMorphism.dpow_comp, DividedPowers.DPMorphism.fromGens_coe, DividedPowers.DPMorphism.fromGens
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
⊢ hI.IsDPMorphism hJ f

Tactic:
exact ⟨h, fun a ha ↦ by
      rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]⟩
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
suffices : map f I ≤ J
⊢ hI.IsDPMorphism hJ f

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]⟩
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
rw : (⇑f : (a : A) → B) '' S ⊆ (↑J : Set B)
⊢ map f I ≤ J

Tactic:
rw [hS, map_span, span_le]

Premises used: Ideal.span_le, Ideal.map_span
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
a : A
has : a ∈ S
⊢ Membership.mem (α := B) (↑J : Set B) ((f : (a : A) → B) a : B)

Tactic:
hS' a has

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
a : A
has : a ∈ S
⊢ Membership.mem (α := B) (↑J : Set B) ((f : (a : A) → B) a : B)

Tactic:
exact hS' a has
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
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)
⊢ hJ.IsDPMorphism hK g

Tactic:
apply on_span _ _ heq

Premises used: DividedPowers.IsDPMorphism.on_span
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
hS' : Membership.mem (α := C) K ((g.comp f : (a : A) → C) a : C)
⊢ Membership.mem (α := C) K ((g : (a : B) → C) ((f : (a : A) → B) a : B) : C)

Tactic:
rw [← RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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.comp f : (a : A) → C) a : C)

Tactic:
hh.1 (mem_map_of_mem _ ha)

Premises used: DividedPowers.IsDPMorphism.ideal_comp, Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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.comp f : (a : A) → C) a : C)

Tactic:
exact hh.1 (mem_map_of_mem _ ha)

Premises used: DividedPowers.IsDPMorphism.ideal_comp, Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
hdp₃ 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)
⊢ (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))

Tactic:
rw [← RingHom.comp_apply, hh.2 a ha, RingHom.comp_apply, hf.2 a ha]

Premises used: DividedPowers.IsDPMorphism.dpow_comp, RingHom.comp_apply
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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
g : hJ.DPMorphism hK
f : hI.DPMorphism hJ
⊢ (g.comp f).toRingHom = g.comp f.toRingHom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
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)
n : ℕ
⊢ ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
(IsDPMorphism.on_span hI hJ hS hS' hdp).2

Premises used: DividedPowers.IsDPMorphism.on_span, DividedPowers.IsDPMorphism.dpow_comp
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
h_eq : ∀ (n : ℕ) {a : A}, a ∈ I → hI'.dpow n a = hI.dpow n a
⊢ hI' = hI

Tactic:
ext n a
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h : a ∈ I
pos : ∀ (ha : a ∈ I), hI'.dpow n a = hI.dpow n a
neg : ∀ (ha : a ∉ I), hI'.dpow n a = hI.dpow n a
⊢ hI'.dpow n a = hI.dpow n a

Tactic:
by_cases ha : a ∈ I
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a

Tactic:
hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha

Premises used: DividedPowers.dpow_comp_from_gens
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
pos : ∀ s ∈ S, Membership.mem (α := A) I ((RingHom.id A : (a : A) → A) s : A)
pos₁ : ∀ {n : ℕ}, ∀ a ∈ S, (RingHom.id A : (a : A) → A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A : (a : A) → A) a)
⊢ hI'.dpow n a = hI.dpow n a

Tactic:
refine hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha

Premises used: DividedPowers.dpow_comp_from_gens
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
s : A
hs : s ∈ S
pos : Membership.mem (γ := Ideal A) (span S) s
⊢ Membership.mem (α := A) I ((RingHom.id A : (a : A) → A) s : A)

Tactic:
simp only [RingHom.id_apply, hS]

Premises used: RingHom.id_apply
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
s : A
hs : s ∈ S
⊢ Membership.mem (γ := Ideal A) (span S) s

Tactic:
subset_span hs

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
s : A
hs : s ∈ S
⊢ Membership.mem (γ := Ideal A) (span S) s

Tactic:
exact subset_span hs

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
m : ℕ
b : A
hb : b ∈ S
⊢ (RingHom.id A : (a : A) → A) (hI.dpow m b) = hI'.dpow m ((RingHom.id A : (a : A) → A) b)

Tactic:
simpa only [RingHom.id_apply] using (hdp b hb)

Premises used: RingHom.id_apply
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h : a ∈ I
ha : a ∉ I
neg : hI'.dpow n a = 0
neg₁ neg₂ : Eq.{u_3 + 1} (α := A) 0 0
⊢ hI'.dpow n a = hI.dpow n a

Tactic:
rw [hI.dpow_null ha, hI'.dpow_null ha]

Premises used: DividedPowers.dpow_null
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
x : A
hx : x ∉ I
⊢ Eq.{u_1 + 1} (α := A)
    (if hx : x ∈ I then
      ⋯.choose (p := fun (a : A) ↦ ∃ (_ : n ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow n ((f : (a : A) → B) x))
    else 0)
    0

Tactic:
simp [dif_neg hx]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
x : A
hx : x ∈ I
simp : hJ.dpow 0 ((f : (a : A) → B) x) = 1
⊢ Eq.{u_1 + 1} (α := A)
    (if hx : x ∈ I then
      Exists.choose (p := fun (a : A) ↦
        ∃ (_ : Ne (α := ℕ) 0 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow 0 ((f : (a : A) → B) x)) ⋯
    else 0)
    1

Tactic:
simp only [dif_pos hx, ← hf.eq_iff, (Exists.choose_spec (hmem 0 hx)).2, map_one]

Premises used: Exists.choose_spec, Function.Injective.eq_iff, dif_pos, map_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
x : A
hx : x ∈ I
rw rw₁ : Eq.{u_2 + 1} (α := B) 1 1
⊢ hJ.dpow 0 ((f : (a : A) → B) x) = 1

Tactic:
rw [hJ.dpow_zero (hIJ ▸ Ideal.mem_map_of_mem f hx)]

Premises used: DividedPowers.dpow_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
x : A
hx : x ∈ I
⊢ (if hx : x ∈ I then
      Exists.choose (p := fun (a : A) ↦
        ∃ (_ : Ne (α := ℕ) 1 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow 1 ((f : (a : A) → B) x)) ⋯
    else 0) =
    x

Tactic:
simpa only [dif_pos hx, ← hf.eq_iff, (Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2]
      using hJ.dpow_one (hIJ ▸ Ideal.mem_map_of_mem f hx)

Premises used: Exists.choose_spec, Function.Injective.eq_iff, dif_pos, DividedPowers.dpow_one
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
x : A
hn : n ≠ 0
hx : x ∈ I
⊢ (if hx : x ∈ I then
      ⋯.choose (p := fun (a : A) ↦ ∃ (_ : n ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow n ((f : (a : A) → B) x))
    else 0) ∈
    I

Tactic:
simpa only [dif_pos hx] using (Exists.choose_spec (hmem n hx)).1 hn

Premises used: Exists.choose_spec, dif_pos
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ x + y ∈ I

Tactic:
have hxy : x + y ∈ I := Ideal.add_mem _ hx hy