awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
p : MvPolynomial.{u_2, u_1} (ℕ × M) R
rw :
  Eq (α := DividedPowerAlgebra S N)
    ((lift' (f := fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2)) ⋯ ⋯ ⋯ ⋯ :
          (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p) :
      DividedPowerAlgebra S N)
    ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
          (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
        p :
      DividedPowerAlgebra S N)
⊢ Eq (α := DividedPowerAlgebra S N)
    ((map S f : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p) :
      DividedPowerAlgebra S N)
    ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
          (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
        p :
      DividedPowerAlgebra S N)
have rw₁ : Eq (α := DividedPowerAlgebra S N)
  ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
        (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
      p :
    DividedPowerAlgebra S N)
  ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
        (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
      p :
    DividedPowerAlgebra S N)
Tactic: rw [map, lift'_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
a : M
⊢ Eq (α := DividedPowerAlgebra S N)
    ((map S f : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N) (dp R n a) : DividedPowerAlgebra S N)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
have rw : Eq (α := DividedPowerAlgebra S N)
  ((lift' (f := fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2)) sorry sorry sorry sorry :
        (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
      (dp R n a) :
    DividedPowerAlgebra S N)
  (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
Tactic: rw [map, lift'_apply_dp]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
a : M
rw :
  Eq (α := DividedPowerAlgebra S N)
    ((lift' (f := fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2)) ⋯ ⋯ ⋯ ⋯ :
          (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        (dp R n a) :
      DividedPowerAlgebra S N)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
⊢ Eq (α := DividedPowerAlgebra S N)
    ((map S f : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N) (dp R n a) : DividedPowerAlgebra S N)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
have rw₁ : Eq (α := DividedPowerAlgebra S N) (dp S (n, a).1 ((f : (a : M) → N) (n, a).2) : DividedPowerAlgebra S N)
  (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
Tactic: rw [map, lift'_apply_dp]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
⊢ Eq (α := M →ₗ[R] DividedPowerAlgebra S N) (AlgHom.toLinearMap (map S f) ∘ₗ embed R M)
    ((↑R :
          {S : Type u_3} →
            {M : Type u_4} →
              {M₂ : Type (max u_3 u_4)} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (embed S N) ∘ₗ
      f)
have h : ∀ (x : M),
  Eq (α := DividedPowerAlgebra S N)
    ((AlgHom.toLinearMap (map S f) ∘ₗ embed R M : (a : M) → DividedPowerAlgebra S N) x : DividedPowerAlgebra S N)
    (((↑R :
                {S : Type u_3} →
                  {M : Type u_4} →
                    {M₂ : Type (max u_3 u_4)} →
                      [inst : Semiring R] →
                        [inst_9 : Semiring S] →
                          [inst_10 : AddCommMonoid M] →
                            [inst_11 : AddCommMonoid M₂] →
                              [inst_12 : Module R M] →
                                [inst_13 : Module R M₂] →
                                  [inst_14 : Module S M] →
                                    [inst_15 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (embed S N) ∘ₗ
            f :
          (a : M) → DividedPowerAlgebra S N)
        x :
      DividedPowerAlgebra S N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Surjective (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R N)
    (⇑(map R f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R N)
have rw : Set.range X ⊆
  (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
        (Subalgebra.map (map R f) ⊤)) :
    Set (MvPolynomial (ℕ × N) R))
Tactic: rw [← AlgHom.range_eq_top, ← Algebra.map_top (map R f), eq_top_iff,
    ← (AlgHom.range_eq_top (mkAlgHom R (Rel R N))).mpr mkAlgHom_surjective,
    ← Algebra.map_top, (Subalgebra.gc_map_comap _).le_iff_le, ← MvPolynomial.adjoin_range_X,
    Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a : MvPolynomial.{u_4, u_1} (ℕ × N) R
⊢ Membership.mem (γ := Set (MvPolynomial.{u_4, u_1} (ℕ × N) R)) (Set.range X) a →
    a ∈
      (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
            (Subalgebra.map (map R f) ⊤)) :
        Set (MvPolynomial (ℕ × N) R))
have simp : (∃ (a_1 : ℕ) (b : N), X (a_1, b) = a) →
  a ∈
    (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
          (Subalgebra.map (map R f) ⊤)) :
      Set (MvPolynomial (ℕ × N) R))
Tactic: simp only [Set.mem_range, Prod.exists]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
m : N
⊢ X (n, m) ∈
    (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
          (Subalgebra.map (map R f) ⊤)) :
      Set (MvPolynomial (ℕ × N) R))
have obtain : ∀ (l : M),
  Membership.mem (α := MvPolynomial.{u_4, u_1} (ℕ × N) R)
    (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
          (Subalgebra.map (map R f) ⊤)) :
      Set (MvPolynomial (ℕ × N) R))
    (X (n, (f : (a : M) → N) l) : MvPolynomial.{u_4, u_1} (ℕ × N) R)
Tactic: obtain ⟨l, rfl⟩ := hf m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
l : M
⊢ Membership.mem (α := MvPolynomial.{u_4, u_1} (ℕ × N) R)
    (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
          (Subalgebra.map (map R f) ⊤)) :
      Set (MvPolynomial (ℕ × N) R))
    (X (n, (f : (a : M) → N) l) : MvPolynomial.{u_4, u_1} (ℕ × N) R)
have simp : ∃ (y : DividedPowerAlgebra R M),
  Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) y :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
Tactic: simp only [Algebra.map_top, Subalgebra.coe_comap, AlgHom.coe_range, Set.mem_preimage,
    Set.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
l : M
⊢ ∃ (y : DividedPowerAlgebra R M),
    Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
      ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) y :
        RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
      ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
        RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
have h : Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
  ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) (dp R n l) :
    RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
  ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
    RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
Tactic: use dp R n l
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
l : M
⊢ Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) (dp R n l) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
have h : Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
  (dp R n ((f : (a : M) → N) l) : DividedPowerAlgebra R N)
  ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
    RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
Tactic: rw [map_apply_dp, dp]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
l : M
h :
  Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    (dp R n ((f : (a : M) → N) l) : DividedPowerAlgebra R N)
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
⊢ Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) (dp R n l) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
have h₁ : Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
  ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
    RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
  ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
    RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
Tactic: rw [map_apply_dp, dp]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ Eq (α := DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra R P) (map R (g ∘ₗ f)) (AlgHom.comp (map R g) (map R f))
have rw : ∀ (n : ℕ) (m : M),
  Eq (α := DividedPowerAlgebra R P)
    ((map R (g ∘ₗ f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R P) (dp R n m) : DividedPowerAlgebra R P)
    ((AlgHom.comp (map R g) (map R f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R P) (dp R n m) :
      DividedPowerAlgebra R P)
Tactic: rw [algHom_ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra R M) (map R LinearMap.id)
    (AlgHom.id R (DividedPowerAlgebra R M))
have rw : ∀ (n : ℕ) (m : M),
  Eq (α := DividedPowerAlgebra R M)
    ((map R LinearMap.id : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R M) (dp R n m) :
      DividedPowerAlgebra R M)
    ((AlgHom.id R (DividedPowerAlgebra R M) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R M) (dp R n m) :
      DividedPowerAlgebra R M)
Tactic: rw [algHom_ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : a ∉ ⊥
⊢ Eq.{u_1 + 1} (α := A) (if a = 0 ∧ n = 0 then 1 else 0) 0
have ha₁ : ¬a = 0
Tactic: simp only [mem_bot] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : ¬a = 0
⊢ Eq.{u_1 + 1} (α := A) (if a = 0 ∧ n = 0 then 1 else 0) 0
have hnc : ¬(a = 0 ∧ n = 0)
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
x : A
ha : Membership.mem (γ := Ideal A) ⊥ x
⊢ Eq.{u_1 + 1} (α := A) (if x = 0 ∧ Eq (α := ℕ) 0 0 then 1 else 0) 1
have rw : Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ Eq (α := ℕ) 0 0 then 1 else 0) 1
Tactic: rw [mem_bot.mp ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
hn : n ≠ 0
h : Membership.mem (γ := Ideal A) ⊥ a
⊢ Membership.mem (γ := Ideal A) ⊥ (if a = 0 ∧ n = 0 then 1 else 0)
have simp : a = 0 → n = 0 → Eq.{u_1 + 1} (α := A) 1 0
Tactic: simp only [mem_bot, ite_eq_right_iff, and_imp]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
⊢ Eq.{u_1 + 1} (α := A) (if x + y = 0 ∧ n = 0 then 1 else 0)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (if x = 0 ∧ k.1 = 0 then 1 else 0) (if y = 0 ∧ k.2 = 0 then 1 else 0))
have rw : Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0)
  (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
    HMul.hMul (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.1 = 0 then 1 else 0)
      (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.2 = 0 then 1 else 0))
Tactic: rw [mem_bot.mp ha, mem_bot.mp hb, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
⊢ Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.1 = 0 then 1 else 0)
        (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.2 = 0 then 1 else 0))
have simp : Eq.{u_1 + 1} (α := A) (if n = 0 then 1 else 0)
  (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
Tactic: simp only [true_and, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
⊢ Eq.{u_1 + 1} (α := A) (if n = 0 then 1 else 0)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
have pos : ∀ (h : n = 0),
  Eq.{u_1 + 1} (α := A) 1 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
pos :
  ∀ (h : n = 0),
    Eq.{u_1 + 1} (α := A) 1 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
⊢ Eq.{u_1 + 1} (α := A) (if n = 0 then 1 else 0)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
have neg : ∀ (h : ¬n = 0),
  Eq.{u_1 + 1} (α := A) 0 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
h : ¬n = 0
⊢ Eq.{u_1 + 1} (α := A) 0 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
have neg : Eq.{u_1 + 1} (α := A) (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) 0
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
h : ¬n = 0
⊢ Eq.{u_1 + 1} (α := A) (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) 0
have neg : ∀ x ∈ @antidiagonal _ instAddMonoid _ n, Eq.{u_1 + 1} (α := A) (if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) 0
Tactic: apply sum_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
⊢ (if x * x_1 = 0 ∧ n = 0 then 1 else 0) = x ^ n * if x_1 = 0 ∧ n = 0 then 1 else 0
have rw : (if x * 0 = 0 ∧ n = 0 then 1 else 0) = x ^ n * if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0
Tactic: rw [mem_bot.mp hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
⊢ (if x * 0 = 0 ∧ n = 0 then 1 else 0) = x ^ n * if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0
have simp : (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
Tactic: simp only [mul_zero, true_and, mul_ite, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
have pos : ∀ (hn : n = 0), (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
pos : ∀ (hn : n = 0), (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
have neg : ∀ (hn : ¬n = 0), (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
hn : n = 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
have pos : 1 = if n = 0 then x ^ n else 0
Tactic: rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
hn : n = 0
pos : 1 = if n = 0 then x ^ n else 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
have pos₁ : 1 = if Eq (α := ℕ) 0 0 then HPow.hPow (β := ℕ) x 0 else 0
Tactic: rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
hn : n = 0
pos : 1 = if n = 0 then x ^ n else 0
pos₁ : 1 = if Eq (α := ℕ) 0 0 then HPow.hPow (β := ℕ) x 0 else 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
have pos₂ : 1 = HPow.hPow (β := ℕ) x 0
Tactic: rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
hn : n = 0
pos : 1 = if n = 0 then x ^ n else 0
pos₁ : 1 = if Eq (α := ℕ) 0 0 then HPow.hPow (β := ℕ) x 0 else 0
pos₂ : 1 = HPow.hPow (β := ℕ) x 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
have pos₃ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
⊢ HMul.hMul (α := A) (if x = 0 ∧ m = 0 then 1 else 0) (if x = 0 ∧ n = 0 then 1 else 0) =
    HMul.hMul (α := A) (↑((m + n).choose m) : A) (if x = 0 ∧ m + n = 0 then 1 else 0)
have rw : HMul.hMul (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ m = 0 then 1 else 0)
    (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) =
  HMul.hMul (α := A) (↑((m + n).choose m) : A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ m + n = 0 then 1 else 0)
Tactic: rw [mem_bot.mp hx]