awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst_2 : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
⊢ hI.IsDPMorphism hK (g.comp f)

Tactic:
⟨le_trans (map_map f g ▸ map_mono hf.1) hg.1, fun a ha ↦ ?_⟩

Premises used: DividedPowers.IsDPMorphism.ideal_comp, DividedPowers.IsDPMorphism.mk, le_trans
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst_2 : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
refine : ∀ {n : ℕ} (a : A) (ha : a ∈ I), hK.dpow n ((g.comp f : (a : A) → C) a) = (g.comp f : (a : A) → C) (hI.dpow n a)
⊢ hI.IsDPMorphism hK (g.comp f)

Tactic:
refine ⟨le_trans (map_map f g ▸ map_mono hf.1) hg.1, fun a ha ↦ ?_⟩
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst_2 : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
simp : hK.dpow n ((g : (a : B) → C) ((f : (a : A) → B) a : B)) = (g : (a : B) → C) ((f : (a : A) → B) (hI.dpow n a) : B)
⊢ hK.dpow n ((g.comp f : (a : A) → C) a) = (g.comp f : (a : A) → C) (hI.dpow n a)

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply]

Premises used: RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst_2 : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
a₁ : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
⊢ hK.dpow n ((g : (a : B) → C) ((f : (a : A) → B) a : B)) = (g : (a : B) → C) ((f : (a : A) → B) (hI.dpow n a) : B)

Tactic:
rw [← hf.2 a ha, hg.2]

Premises used: DividedPowers.IsDPMorphism.dpow_comp
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst_2 : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ Membership.mem (α := B) J ((f : (a : A) → B) a : B)

Tactic:
hf.1 (mem_map_of_mem f ha)

Premises used: DividedPowers.IsDPMorphism.ideal_comp, Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.DividedPowers.DPMorphism
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
C : Type u_3
inst_2 : CommSemiring C
K : Ideal C
hK : DividedPowers K
f : A →+* B
g : B →+* C
hg : hJ.IsDPMorphism hK g
hf : hI.IsDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ Membership.mem (α := B) J ((f : (a : A) → B) a : B)

Tactic:
exact hf.1 (mem_map_of_mem f ha)

Premises used: DividedPowers.IsDPMorphism.ideal_comp, Ideal.mem_map_of_mem
-- 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
h h' : hI.DPMorphism hJ
hh' :
  Eq (α := (a : A) → B) ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B)) h)
    ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B)) h')
mk :
  ∀ (toRingHom : A →+* B) (ideal_comp : map toRingHom I ≤ J)
    (dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom : (a : A) → B) a) = (toRingHom : (a : A) → B) (hI.dpow n a))
    (hh' :
      Eq (α := (a : A) → B)
        ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B))
          { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp })
        ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B)) h')),
    { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp : hI.DPMorphism hJ } = h'
⊢ h = h'

Tactic:
cases h
-- 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
h' : hI.DPMorphism hJ
toRingHom : A →+* B
ideal_comp : map toRingHom I ≤ J
dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom : (a : A) → B) a) = (toRingHom : (a : A) → B) (hI.dpow n a)
hh' :
  Eq (α := (a : A) → B)
    ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B))
      { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp })
    ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B)) h')
mk :
  ∀ (toRingHom_1 : A →+* B) (ideal_comp_1 : map toRingHom_1 I ≤ J)
    (dpow_comp_1 :
      ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom_1 : (a : A) → B) a) = (toRingHom_1 : (a : A) → B) (hI.dpow n a))
    (hh' :
      Eq (α := (a : A) → B)
        ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B))
          { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp })
        ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B))
          { toRingHom := toRingHom_1, ideal_comp := ideal_comp_1, dpow_comp := @dpow_comp_1 })),
    { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp : hI.DPMorphism hJ } =
      { toRingHom := toRingHom_1, ideal_comp := ideal_comp_1, dpow_comp := @dpow_comp_1 }
⊢ { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp : hI.DPMorphism hJ } = h'

Tactic:
cases h'
-- 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
toRingHom : A →+* B
ideal_comp : map toRingHom I ≤ J
dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom : (a : A) → B) a) = (toRingHom : (a : A) → B) (hI.dpow n a)
toRingHom_1 : A →+* B
ideal_comp_1 : map toRingHom_1 I ≤ J
dpow_comp_1 : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom_1 : (a : A) → B) a) = (toRingHom_1 : (a : A) → B) (hI.dpow n a)
hh' :
  Eq (α := (a : A) → B)
    ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B))
      { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp })
    ((fun (h : hI.DPMorphism hJ) ↦ ((⇑h.toRingHom : (a : A) → B) : (a : A) → B))
      { toRingHom := toRingHom_1, ideal_comp := ideal_comp_1, dpow_comp := @dpow_comp_1 })
mk : toRingHom = toRingHom_1
⊢ { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := @dpow_comp : hI.DPMorphism hJ } =
    { toRingHom := toRingHom_1, ideal_comp := ideal_comp_1, dpow_comp := @dpow_comp_1 }

Tactic:
congr
-- 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
toRingHom : A →+* B
ideal_comp : map toRingHom I ≤ J
dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom : (a : A) → B) a) = (toRingHom : (a : A) → B) (hI.dpow n a)
toRingHom_1 : A →+* B
ideal_comp_1 : map toRingHom_1 I ≤ J
dpow_comp_1 : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom_1 : (a : A) → B) a) = (toRingHom_1 : (a : A) → B) (hI.dpow n a)
hh' : Eq (α := (a : A) → B) (⇑toRingHom : (a : A) → B) (⇑toRingHom_1 : (a : A) → B)
mk : ∀ (x : A), Eq.{u_4 + 1} (α := B) ((toRingHom : (a : A) → B) x : B) ((toRingHom_1 : (a : A) → B) x : B)
⊢ toRingHom = toRingHom_1

Tactic:
ext
-- 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
toRingHom : A →+* B
ideal_comp : map toRingHom I ≤ J
dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom : (a : A) → B) a) = (toRingHom : (a : A) → B) (hI.dpow n a)
toRingHom_1 : A →+* B
ideal_comp_1 : map toRingHom_1 I ≤ J
dpow_comp_1 : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((toRingHom_1 : (a : A) → B) a) = (toRingHom_1 : (a : A) → B) (hI.dpow n a)
hh' : Eq (α := (a : A) → B) (⇑toRingHom : (a : A) → B) (⇑toRingHom_1 : (a : A) → B)
x : A
mk mk₁ : Eq.{u_4 + 1} (α := B) ((toRingHom_1 : (a : A) → B) x : B) ((toRingHom_1 : (a : A) → B) x : B)
⊢ Eq.{u_4 + 1} (α := B) ((toRingHom : (a : A) → B) x : B) ((toRingHom_1 : (a : A) → B) x : B)

Tactic:
rw [hh']
-- 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 : hI.DPMorphism hJ
⊢ Eq (α := (a : A) → B) (⇑f.toRingHom : (a : A) → B) (⇑f : (a : A) → B)

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 : hI.DPMorphism hJ
a : A
⊢ Eq.{u_4 + 1} (α := B) ((f.toRingHom : (a : A) → B) a : B) ((f : (a : A) → B) a : B)

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 : hI.DPMorphism hJ
⊢ hI.IsDPMorphism hJ f.toRingHom

Tactic:
⟨f.ideal_comp, f.dpow_comp⟩

Premises used: DividedPowers.DPMorphism.dpow_comp, DividedPowers.DPMorphism.ideal_comp, DividedPowers.IsDPMorphism.mk
-- 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
a b : 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)} a
hy :
  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)} b
simp :
  a + b ∈ I ∧
    ∀ (n : ℕ),
      (f : (a : A) → B) (hI.dpow n (a + b)) =
        hJ.dpow n (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B))
⊢ 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)} (a + b)

Tactic:
simp only [mem_setOf_eq, map_add] at hx hy ⊢

Premises used: map_add, Set.mem_setOf_eq
-- 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
a b : A
hx : a ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
hy : b ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n b) = hJ.dpow n ((f : (a : A) → B) b)
⊢ a + b ∈ I ∧
    ∀ (n : ℕ),
      (f : (a : A) → B) (hI.dpow n (a + b)) =
        hJ.dpow n (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B))

Tactic:
⟨I.add_mem hx.1 hy.1, fun n ↦ ?_⟩

Premises used: Ideal.add_mem, And.left, And.intro
-- 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
a b : A
hx : a ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
hy : b ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n b) = hJ.dpow n ((f : (a : A) → B) b)
refine :
  ∀ (n : ℕ),
    (f : (a : A) → B) (hI.dpow n (a + b)) =
      hJ.dpow n (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B))
⊢ a + b ∈ I ∧
    ∀ (n : ℕ),
      (f : (a : A) → B) (hI.dpow n (a + b)) =
        hJ.dpow n (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B))

Tactic:
refine ⟨I.add_mem hx.1 hy.1, fun n ↦ ?_⟩
-- 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
a b : A
hx : a ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
hy : b ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n b) = hJ.dpow n ((f : (a : A) → B) b)
n : ℕ
rw :
  Eq.{u_4 + 1} (α := B)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (f : (a : A) → B) (hI.dpow x.1 a * hI.dpow x.2 b))
    (∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b))
⊢ (f : (a : A) → B) (hI.dpow n (a + b)) =
    hJ.dpow n (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B))

Tactic:
rw [hI.dpow_add hx.1 hy.1, map_sum,
      hJ.dpow_add (hf (mem_map_of_mem f hx.1)) (hf (mem_map_of_mem f hy.1))]

Premises used: Ideal.mem_map_of_mem, DividedPowers.dpow_add, map_sum, And.left
-- 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
a b : A
hx : a ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
hy : b ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n b) = hJ.dpow n ((f : (a : A) → B) b)
n : ℕ
h :
  Eq.{u_4 + 1} (α := (x : ℕ × ℕ) → B) (fun (x : ℕ × ℕ) ↦ (f : (a : A) → B) (hI.dpow x.1 a * hI.dpow x.2 b))
    fun (k : ℕ × ℕ) ↦ hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b)
⊢ Eq.{u_4 + 1} (α := B)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, (f : (a : A) → B) (hI.dpow x.1 a * hI.dpow x.2 b))
    (∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b))

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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
a b : A
hx : a ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
hy : b ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n b) = hJ.dpow n ((f : (a : A) → B) b)
n : ℕ
h :
  ∀ (k : ℕ × ℕ),
    (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
      hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b)
⊢ Eq.{u_4 + 1} (α := (x : ℕ × ℕ) → B) (fun (x : ℕ × ℕ) ↦ (f : (a : A) → B) (hI.dpow x.1 a * hI.dpow x.2 b))
    fun (k : ℕ × ℕ) ↦ hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b)

Tactic:
ext k
-- 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
a b : A
hx : a ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)
hy : b ∈ I ∧ ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n b) = hJ.dpow n ((f : (a : A) → B) b)
n : ℕ
k : ℕ × ℕ
h :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow k.1 a) : B) ((f : (a : A) → B) (hI.dpow k.2 b) : B) =
    hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b)
h₁ :
  HMul.hMul (β := B) (hJ.dpow k.1 ((f : (a : A) → B) a)) ((f : (a : A) → B) (hI.dpow k.2 b) : B) =
    hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b)
h₂ h₃ :
  hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b) =
    hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b)
⊢ (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
    hJ.dpow k.1 ((f : (a : A) → B) a) * hJ.dpow k.2 ((f : (a : A) → B) b)

Tactic:
rw [map_mul, hx.2, hy.2]

Premises used: map_mul, And.right
-- 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
simp : ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 0
⊢ 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)} 0

Tactic:
simp only [mem_setOf_eq, Submodule.zero_mem, map_zero, true_and]

Premises used: map_zero, Set.mem_setOf_eq, Submodule.zero_mem, true_and
-- 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
zero : (f : (a : A) → B) 1 = hJ.dpow 0 0
zero₁ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
zero₂ zero₃ : Eq.{u_4 + 1} (α := B) 1 1
⊢ (f : (a : A) → B) (hI.dpow 0 0) = hJ.dpow 0 0

Tactic:
rw [hI.dpow_zero I.zero_mem, hJ.dpow_zero J.zero_mem, map_one]

Premises used: Ideal.zero_mem, DividedPowers.dpow_zero, map_one
-- 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
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)
succ₂ succ₃ : Eq.{u_4 + 1} (α := B) 0 0
⊢ (f : (a : A) → B) (hI.dpow (n + 1) 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]

Premises used: map_zero, DividedPowers.dpow_eval_zero, Nat.succ_ne_zero
-- 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
n : ℕ
zero : (f : (a : A) → B) (hI.dpow 0 0) = hJ.dpow 0 0
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
⊢ (f : (a : A) → B) (hI.dpow n 0) = hJ.dpow n 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]

Premises used: map_zero, DividedPowers.dpow_eval_zero, Ideal.zero_mem, DividedPowers.dpow_zero, Nat.succ_ne_zero, map_one
-- 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
⊢ 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)

Tactic:
⟨I.smul_mem r hx.1, (fun n ↦ ?_)⟩

Premises used: Set.Mem, setOf, And.left, And.intro, Submodule.smul_mem
-- 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
refine : ∀ (n : ℕ), (f : (a : A) → B) (hI.dpow n (r • x)) = hJ.dpow n ((f : (a : A) → B) (r • 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)

Tactic:
refine ⟨I.smul_mem r hx.1, (fun n ↦ ?_)⟩