awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hx : x ∉ J
rw : ((e.symm : (a : B) → A) x : A) ∉ I
⊢ Eq.{u_2 + 1} (α := B) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) (0 : B)

Tactic:
rw [EmbeddingLike.map_eq_zero_iff, hI.dpow_null]

Premises used: DividedPowers.dpow_null, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hx : x ∉ J
rwa : x ∉ Ideal.map e I
rwa₁ rwa₂ rwa₃ rwa₄ : x ∉ J
⊢ ((e.symm : (a : B) → A) x : A) ∉ I

Tactic:
rwa [symm_apply_mem_of_equiv_iff, h]

Premises used: Ideal.symm_apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x : B
hx : x ∈ J
rw : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
⊢ Eq.{u_2 + 1} (α := B) ((e : (a : A) → B) (hI.dpow 0 ((e.symm : (a : B) → A) x)) : B) (1 : B)

Tactic:
rw [EmbeddingLike.map_eq_one_iff, hI.dpow_zero]

Premises used: EmbeddingLike.map_eq_one_iff, DividedPowers.dpow_zero
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x : B
hx : x ∈ J
rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)

Tactic:
rwa [symm_apply_mem_of_equiv_iff, h]

Premises used: Ideal.symm_apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x_1 : B
hx : x_1 ∈ J
x : Membership.mem (α := A) I ((e.symm : (a : B) → A) x_1 : A)
⊢ (e : (a : A) → B) (hI.dpow 1 ((e.symm : (a : B) → A) x_1)) = x_1

Tactic:
rw [dpow_one, RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, DividedPowers.dpow_one
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x_1 : B
hx : x_1 ∈ J
x : Membership.mem (γ := Ideal B) (Ideal.map e I) x_1
x₁ x₂ x₃ x₄ : x_1 ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x_1 : A)

Tactic:
rwa [I.symm_apply_mem_of_equiv_iff, h]

Premises used: Ideal.symm_apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
rw : hI.dpow n ((e.symm : (a : B) → A) x) ∈ I
⊢ Membership.mem (α := B) J ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)

Tactic:
rw [← h, I.apply_mem_of_equiv_iff]

Premises used: Ideal.apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
apply : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
⊢ hI.dpow n ((e.symm : (a : B) → A) x) ∈ I

Tactic:
apply hI.dpow_mem hn

Premises used: DividedPowers.dpow_mem
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)

Tactic:
rwa [I.symm_apply_mem_of_equiv_iff, h]

Premises used: Ideal.symm_apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x y : B
hx : x ∈ J
hy : y ∈ J
simp :
  Eq.{u_2 + 1} (α := B)
    ((e : (a : A) → B)
        (hI.dpow n (HAdd.hAdd (α := A) (β := A) ((e.symm : (a : B) → A) x : A) ((e.symm : (a : B) → A) y : A))) :
      B)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
          ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
      B)
⊢ Eq.{u_2 + 1} (α := B) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) (x + y))) : B)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
          ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
      B)

Tactic:
simp only [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x y : B
hx : x ∈ J
hy : y ∈ J
rw :
  Eq.{u_2 + 1} (α := B)
    ((e : (a : A) → B)
        (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
          hI.dpow k.1 ((e.symm : (a : B) → A) x) * hI.dpow k.2 ((e.symm : (a : B) → A) y)) :
      B)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
          ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
      B)
⊢ Eq.{u_2 + 1} (α := B)
    ((e : (a : A) → B)
        (hI.dpow n (HAdd.hAdd (α := A) (β := A) ((e.symm : (a : B) → A) x : A) ((e.symm : (a : B) → A) y : A))) :
      B)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
          ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
      B)

Tactic:
rw [hI.dpow_add (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))
        (symm_apply_mem_of_equiv_iff.mpr (h ▸ hy))]

Premises used: Iff.mpr, DividedPowers.dpow_add, Ideal.symm_apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x y : B
hx : x ∈ J
hy : y ∈ J
⊢ Eq.{u_2 + 1} (α := B)
    ((e : (a : A) → B)
        (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
          hI.dpow k.1 ((e.symm : (a : B) → A) x) * hI.dpow k.2 ((e.symm : (a : B) → A) y)) :
      B)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
          ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
      B)

Tactic:
simp only [map_sum, map_mul]

Premises used: map_sum, map_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a x : B
hx : x ∈ J
simp :
  (e : (a : A) → B)
      (hI.dpow n (HMul.hMul (α := A) (β := A) ((e.symm : (a : B) → A) a : A) ((e.symm : (a : B) → A) x : A))) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
⊢ (e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) (a * x))) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)

Tactic:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a x : B
hx : x ∈ J
rw :
  (e : (a : A) → B) (HPow.hPow (α := A) ((e.symm : (a : B) → A) a : A) n * hI.dpow n ((e.symm : (a : B) → A) x)) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
⊢ (e : (a : A) → B)
      (hI.dpow n (HMul.hMul (α := A) (β := A) ((e.symm : (a : B) → A) a : A) ((e.symm : (a : B) → A) x : A))) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)

Tactic:
rw [hI.dpow_mul (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))]

Premises used: Iff.mpr, Ideal.symm_apply_mem_of_equiv_iff, DividedPowers.dpow_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a x : B
hx : x ∈ J
rw :
  HMul.hMul (β := B) (HPow.hPow (α := B) ((e : (a : A) → B) ((e.symm : (a : B) → A) a : A) : B) n)
      ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
⊢ (e : (a : A) → B) (HPow.hPow (α := A) ((e.symm : (a : B) → A) a : A) n * hI.dpow n ((e.symm : (a : B) → A) x)) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)

Tactic:
rw [map_mul, map_pow]

Premises used: map_pow, map_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a x : B
hx : x ∈ J
⊢ HMul.hMul (β := B) (HPow.hPow (α := B) ((e : (a : A) → B) ((e.symm : (a : B) → A) a : A) : B) n)
      ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)

Tactic:
simp only [RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hx : x ∈ J
rw :
  HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (↑((m + n).choose m) : A) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B)
rw₁ : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
⊢ HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow m ((e.symm : (a : B) → A) x)) : B)
      ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B)

Tactic:
rw [← map_mul, hI.mul_dpow, map_mul]

Premises used: DividedPowers.mul_dpow, map_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hx : x ∈ J
⊢ HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (↑((m + n).choose m) : A) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B)

Tactic:
simp only [map_natCast]

Premises used: map_natCast
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hx : x ∈ J
rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)

Tactic:
rwa [symm_apply_mem_of_equiv_iff, h]

Premises used: Ideal.symm_apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
simp :
  (e : (a : A) → B) (hI.dpow m (hI.dpow n ((e.symm : (a : B) → A) x))) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
⊢ (e : (a : A) → B)
      (hI.dpow m ((e.symm : (a : B) → A) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B))) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)

Tactic:
simp only [RingEquiv.symm_apply_apply]

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
rw :
  (e : (a : A) → B) ((↑(m.uniformBell n) : A) * hI.dpow (m * n) ((e.symm : (a : B) → A) x)) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
rw₁ : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
⊢ (e : (a : A) → B) (hI.dpow m (hI.dpow n ((e.symm : (a : B) → A) x))) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)

Tactic:
rw [hI.dpow_comp hn]

Premises used: DividedPowers.dpow_comp
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ (e : (a : A) → B) ((↑(m.uniformBell n) : A) * hI.dpow (m * n) ((e.symm : (a : B) → A) x)) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)

Tactic:
simp only [map_mul, map_natCast]

Premises used: map_mul, map_natCast
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)

Tactic:
rwa [symm_apply_mem_of_equiv_iff, h]

Premises used: Ideal.symm_apply_mem_of_equiv_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
b : B
⊢ (ofRingEquiv h hI).dpow n b = (e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) b))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
⊢ (ofRingEquiv h hI).dpow n ((e : (a : A) → B) a) = (e : (a : A) → B) (hI.dpow n a)

Tactic:
simp
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
rw : Ideal.map (R := B) e.symm (Ideal.map e I) = I
⊢ Ideal.map e.symm J = I

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
⊢ Ideal.map (R := B) e.symm (Ideal.map e I) = I

Tactic:
I.map_of_equiv e

Premises used: Set.Mem, setOf, Ideal.map, Ideal.map_of_equiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
⊢ Ideal.map (R := B) e.symm (Ideal.map e I) = I

Tactic:
exact I.map_of_equiv e

Premises used: Ideal.map_of_equiv
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
h_eq : ∀ (n : ℕ) {a : A}, a ∈ I → dpow (I := I) (ofRingEquiv (e := e.symm) ⋯ (ofRingEquiv h hI)) n a = hI.dpow n a
⊢ ofRingEquiv (e := e.symm) ⋯ (ofRingEquiv h hI) = hI

Tactic:
ext n a
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
h_1 : a ∈ I
⊢ dpow (I := I) (ofRingEquiv (e := e.symm) ⋯ (ofRingEquiv h hI)) n a = hI.dpow n a

Tactic:
simp [ofRingEquiv]

Premises used: DividedPowers.ofRingEquiv
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hJ : DividedPowers J
h_eq : ∀ (n : ℕ) {b : B}, b ∈ J → (ofRingEquiv h (ofRingEquiv (e := e.symm) ⋯ hJ)).dpow n b = hJ.dpow n b
⊢ ofRingEquiv h (ofRingEquiv (e := e.symm) ⋯ hJ) = hJ

Tactic:
ext n b
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hJ : DividedPowers J
n : ℕ
b : B
h_1 : b ∈ J
⊢ (ofRingEquiv h (ofRingEquiv (e := e.symm) ⋯ hJ)).dpow n b = hJ.dpow n b

Tactic:
simp [ofRingEquiv]

Premises used: DividedPowers.ofRingEquiv
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
b : B
⊢ dpow (I := J) ((equiv h : (a : DividedPowers I) → DividedPowers J) hI) n b =
    (e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) b))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
⊢ Eq.{u_2 + 1} (α := B)
    (dpow (I := J) ((equiv h : (a : DividedPowers I) → DividedPowers J) hI) n ((e : (a : A) → B) a) : B)
    ((e : (a : A) → B) (hI.dpow n a) : B)

Tactic:
ofRingEquiv_dpow_apply h hI

Premises used: DividedPowers.ofRingEquiv_dpow_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
f : A →+* B
⊢ hI.IsDPMorphism hJ f ↔
    map f I ≤ J ∧ ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
⟨fun h ↦ ⟨h.ideal_comp, h.dpow_comp⟩, fun ⟨h1, h2⟩ ↦ IsDPMorphism.mk h1 h2⟩

Premises used: DividedPowers.IsDPMorphism.ideal_comp, DividedPowers.IsDPMorphism, DividedPowers.IsDPMorphism.dpow_comp, DividedPowers.IsDPMorphism.mk, And.intro, Iff.intro, _private.0.DividedPowers.isDPMorphism_def.match_1
-- 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
f : A →+* B
rw :
  map f I ≤ J →
    ((∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)) ↔
      ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a))
⊢ hI.IsDPMorphism hJ f ↔
    map f I ≤ J ∧ ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
rw [isDPMorphism_def, and_congr_right_iff]

Premises used: and_congr_right_iff, DividedPowers.isDPMorphism_def
-- 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
f : A →+* B
⊢ map f I ≤ J →
    ((∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)) ↔
      ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a))

Tactic:
fun hIJ ↦ ⟨fun H n _ ↦ H, fun H n ↦ ?_⟩

Premises used: Iff.intro
-- 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
f : A →+* B
refine :
  ∀ (hIJ : map f I ≤ J)
    (H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)) (n : ℕ),
    ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
⊢ map f I ≤ J →
    ((∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)) ↔
      ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a))

Tactic:
refine fun hIJ ↦ ⟨fun H n _ ↦ H, fun H n ↦ ?_⟩
-- 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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
n : ℕ
pos : ∀ (hn : n = 0), ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
neg : ∀ (hn : ¬n = 0), ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
⊢ ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
by_cases hn : n = 0
-- 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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
n : ℕ
hn : n = 0
a : A
ha : a ∈ I
pos : hJ.dpow 0 ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow 0 a)
pos₁ : hJ.dpow 0 ((f : (a : A) → B) a) = (f : (a : A) → B) 1
pos₂ : Eq.{u_2 + 1} (α := B) (1 : B) ((f : (a : A) → B) 1 : B)
pos₃ pos₄ : Eq.{u_2 + 1} (α := B) 1 1
⊢ hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
rw [hn, hI.dpow_zero ha, hJ.dpow_zero (hIJ (mem_map_of_mem f ha)), map_one]

Premises used: Ideal.mem_map_of_mem, DividedPowers.dpow_zero, map_one
-- 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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
n : ℕ
hn : ¬n = 0
⊢ ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
H n hn
-- 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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
n : ℕ
hn : ¬n = 0
⊢ ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
exact H n hn
-- 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
f : A →+* B
hf : hI.IsDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ (f : (a : A) → B) (hI.dpow n a) = hJ.dpow n ((f : (a : A) → B) a)

Tactic:
(hf.2 a ha).symm

Premises used: DividedPowers.IsDPMorphism.dpow_comp, Eq.symm