awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : MulZeroClass α
inst_1 : HasDistribNeg α
rw : -HMul.hMul (α := α) 0 0 = HMul.hMul (α := α) 0 0
⊢ Eq.{u + 1} (α := α) (-0) 0
have rw₁ : HMul.hMul (α := α) (-0) 0 = HMul.hMul (α := α) 0 0
Tactic: rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : MulZeroClass α
inst_1 : HasDistribNeg α
rw : -HMul.hMul (α := α) 0 0 = HMul.hMul (α := α) 0 0
rw₁ : HMul.hMul (α := α) (-0) 0 = HMul.hMul (α := α) 0 0
⊢ Eq.{u + 1} (α := α) (-0) 0
have rw₂ : 0 = HMul.hMul (α := α) 0 0
Tactic: rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : MulZeroClass α
inst_1 : HasDistribNeg α
rw : -HMul.hMul (α := α) 0 0 = HMul.hMul (α := α) 0 0
rw₁ : HMul.hMul (α := α) (-0) 0 = HMul.hMul (α := α) 0 0
rw₂ : 0 = HMul.hMul (α := α) 0 0
⊢ Eq.{u + 1} (α := α) (-0) 0
have rw₃ : Eq.{u + 1} (α := α) 0 0
Tactic: rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
⊢ -a * b + a * b = 0
have rw : (-a + a) * b = 0
Tactic: rw [← right_distrib, neg_add_cancel, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
rw : (-a + a) * b = 0
⊢ -a * b + a * b = 0
have rw₁ : 0 * b = 0
Tactic: rw [← right_distrib, neg_add_cancel, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
rw : (-a + a) * b = 0
rw₁ : 0 * b = 0
⊢ -a * b + a * b = 0
have rw₂ : Eq.{u + 1} (α := α) 0 0
Tactic: rw [← right_distrib, neg_add_cancel, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
⊢ a * -b + a * b = 0
have rw : a * (-b + b) = 0
Tactic: rw [← left_distrib, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
rw : a * (-b + b) = 0
⊢ a * -b + a * b = 0
have rw₁ : a * 0 = 0
Tactic: rw [← left_distrib, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
rw : a * (-b + b) = 0
rw₁ : a * 0 = 0
⊢ a * -b + a * b = 0
have rw₂ : Eq.{u + 1} (α := α) 0 0
Tactic: rw [← left_distrib, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
⊢ (a - 1) * b = a * b - b
have rw : a * b - 1 * b = a * b - b
Tactic: rw [sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : a * b - 1 * b = a * b - b
⊢ (a - 1) * b = a * b - b
have rw₁ : a * b - b = a * b - b
Tactic: rw [sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
⊢ a * (b - 1) = a * b - a
have rw : a * b - a * 1 = a * b - a
Tactic: rw [mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : a * b - a * 1 = a * b - a
⊢ a * (b - 1) = a * b - a
have rw₁ : a * b - a = a * b - a
Tactic: rw [mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
⊢ (1 - a) * b = b - a * b
have rw : 1 * b - a * b = b - a * b
Tactic: rw [sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : 1 * b - a * b = b - a * b
⊢ (1 - a) * b = b - a * b
have rw₁ : b - a * b = b - a * b
Tactic: rw [sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
⊢ a * (1 - b) = a - a * b
have rw : a * 1 - a * b = a - a * b
Tactic: rw [mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : a * 1 - a * b = a - a * b
⊢ a * (1 - b) = a - a * b
have rw₁ : a - a * b = a - a * b
Tactic: rw [mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b c : α
⊢ a * (1 - b) * c = a * c - a * b * c
have rw : (a - a * b) * c = a * c - a * b * c
Tactic: rw [mul_one_sub, sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocRing α
a b c : α
rw : (a - a * b) * c = a * c - a * b * c
⊢ a * (1 - b) * c = a * c - a * b * c
have rw₁ : a * c - a * b * c = a * c - a * b * c
Tactic: rw [mul_one_sub, sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f_1 : F
a b : α
f : α ≃* β := (↑f_1 : α ≃* β)
h : Dvd.dvd.{u_2} (α := β) ((f_1 : (a : α) → β) a : β) ((f_1 : (a : α) → β) b : β)
⊢ a ∣ b
have rw : f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)
Tactic: rw [← f.left_inv a, ← f.left_inv b]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
a : α
b : β
⊢ (f : (a : α) → β) a ∣ b ↔ a ∣ (MulEquiv.symm (↑f : α ≃* β) : (a : β) → α) b
have obtain : ∀ (c : α),
  Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β) ↔
    a ∣ (MulEquiv.symm (↑f : α ≃* β) : (a : β) → α) ((f : (a : α) → β) c : β)
Tactic: obtain ⟨c, rfl⟩ : ∃ c, f c = b := EquivLike.surjective f b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
inst_4 : DecompositionMonoid β
a b c : α
h : a ∣ b * c
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
have h₁ : (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)
Tactic: rw [← map_dvd_iff f, map_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
inst_4 : DecompositionMonoid β
a b c : α
h : (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
have obtain : ∀ (a₁ a₂ : β) (h : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ (f : (a : α) → β) a = a₁ * a₂),
  ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Tactic: obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
inst_4 : DecompositionMonoid β
a b c : α
h_1 : (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)
a₁ a₂ : β
h : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ (f : (a : α) → β) a = a₁ * a₂
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
have refine : (symm (↑f : α ≃* β) : (a : β) → α) a₁ ∣ b ∧
  (symm (↑f : α ≃* β) : (a : β) → α) a₂ ∣ c ∧
    a =
      HMul.hMul (α := α) (β := α) ((symm (↑f : α ≃* β) : (a : β) → α) a₁ : α)
        ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α)
Tactic: refine ⟨symm f a₁, symm f a₂, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
inst_4 : DecompositionMonoid β
a b c : α
h_1 : (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)
a₁ a₂ : β
h : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ (f : (a : α) → β) a = a₁ * a₂
⊢ (symm (↑f : α ≃* β) : (a : β) → α) a₁ ∣ b ∧
    (symm (↑f : α ≃* β) : (a : β) → α) a₂ ∣ c ∧
      a =
        HMul.hMul (α := α) (β := α) ((symm (↑f : α ≃* β) : (a : β) → α) a₁ : α)
          ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α)
have simp_rw : Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₁ : α) : β) ((f : (a : α) → β) b : β) ∧
  Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α) : β) ((f : (a : α) → β) c : β) ∧
    ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂
Tactic: simp_rw [← map_dvd_iff f, ← map_mul, eq_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
inst_4 : DecompositionMonoid β
a b c : α
h_1 : (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)
a₁ a₂ : β
h : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ (f : (a : α) → β) a = a₁ * a₂
⊢ Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₁ : α) : β) ((f : (a : α) → β) b : β) ∧
    Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α) : β)
        ((f : (a : α) → β) c : β) ∧
      ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂
have erw : a₁ ∣ (f : (a : α) → β) b ∧
  Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α) : β) ((f : (a : α) → β) c : β) ∧
    ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂
Tactic: erw [(f : α ≃* β).apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
inst_4 : DecompositionMonoid β
a b c : α
h_1 : (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)
a₁ a₂ : β
h : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ (f : (a : α) → β) a = a₁ * a₂
⊢ a₁ ∣ (f : (a : α) → β) b ∧
    Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α) : β)
        ((f : (a : α) → β) c : β) ∧
      ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂
have erw : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂
Tactic: erw [(f : α ≃* β).apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
f : F
inst_4 : DecompositionMonoid β
a b c : α
h_1 : (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)
a₁ a₂ : β
h : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ (f : (a : α) → β) a = a₁ * a₂
⊢ Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₁ : α) : β) ((f : (a : α) → β) b : β) ∧
    Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α) : β)
        ((f : (a : α) → β) c : β) ∧
      ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂
have iterate : a₁ ∣ (f : (a : α) → β) b ∧ a₂ ∣ (f : (a : α) → β) c ∧ ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂
Tactic: iterate 2 erw [(f : α ≃* β).apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + c ↔ a ∣ c
have rw : a ∣ c + b ↔ a ∣ c
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b - c ↔ a ∣ c
have rw : a ∣ b + -c ↔ a ∣ c
Tactic: rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
rw : a ∣ b + -c ↔ a ∣ c
⊢ a ∣ b - c ↔ a ∣ c
have rw₁ : a ∣ -c ↔ a ∣ c
Tactic: rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
rw : a ∣ b + -c ↔ a ∣ c
rw₁ : a ∣ -c ↔ a ∣ c
⊢ a ∣ b - c ↔ a ∣ c
have rw₂ : a ∣ c ↔ a ∣ c
Tactic: rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b ↔ a ∣ c
have rw : a ∣ b - c + c ↔ a ∣ c
Tactic: rw [← sub_add_cancel b c, dvd_add_right h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b - c
rw : a ∣ b - c + c ↔ a ∣ c
⊢ a ∣ b ↔ a ∣ c
have rw₁ : a ∣ c ↔ a ∣ c
Tactic: rw [← sub_add_cancel b c, dvd_add_right h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
⊢ a ∣ b - c ↔ a ∣ c - b
have rw : a ∣ -(b - c) ↔ a ∣ c - b
Tactic: rw [← dvd_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
rw : a ∣ -(b - c) ↔ a ∣ c - b
⊢ a ∣ b - c ↔ a ∣ c - b
have rw₁ : a ∣ c - b ↔ a ∣ c - b
Tactic: rw [← dvd_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * x - b * y
have h : a * x - b * y = a * (x - y) + (a - b) * y
Tactic: convert! dvd_add (hxy.mul_left a) (hab.mul_right y) using 1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Basic (goal)
Goal:
α : Type u_1
inst : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ a * x - b * y = a * (x - y) + (a - b) * y
have h : a * x - b * y = a * x - a * y + (a * y - b * y)
Tactic: rw [mul_sub_left_distrib, mul_sub_right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : SMul M R
inst_1 : Semigroup R
inst_2 : SMulCommClass M R R
x y : R
m : M
h : x ∣ y
k : R
hk : y = x * k
⊢ m • y = x * m • k
have rw : m • y = m • (x * k)
Tactic: rw [mul_smul_comm, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : SMul M R
inst_1 : Semigroup R
inst_2 : SMulCommClass M R R
x y : R
m : M
h : x ∣ y
k : R
hk : y = x * k
rw : m • y = m • (x * k)
⊢ m • y = x * m • k
have rw₁ : m • y = m • y
Tactic: rw [mul_smul_comm, ← hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
⊢ x ^ m ∣ (x + y) ^ p
have rw : x ^ m ∣ ∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ p, p.choose m.1 • (x ^ m.1 * y ^ m.2)
Tactic: rw [h_comm.add_pow']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
⊢ x ^ m ∣ ∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ p, p.choose m.1 • (x ^ m.1 * y ^ m.2)
have refine : ∀ (x_1 : ℕ × ℕ) (i j : ℕ) (hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ p),
  x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)
Tactic: refine Finset.dvd_sum fun ⟨i, j⟩ hij ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (hypothesis)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x_1 : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ p
⊢ x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)
have hij₁ : i + j = p
Tactic: replace hij : i + j = p := by simpa using hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x_1 : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)
have h : x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
Tactic: apply dvd_nsmul_of_dvd
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x_1 : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
have h : ∀ (hi : m ≤ i), x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
Tactic: rcases le_or_gt m i with (hi : m ≤ i) | (hi : i + 1 ≤ m)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x_1 : ℕ × ℕ
i j : ℕ
hij : i + j = p
h : ∀ (hi : m ≤ i), x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
have h₁ : ∀ (hi : i + 1 ≤ m), x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
Tactic: rcases le_or_gt m i with (hi : m ≤ i) | (hi : i + 1 ≤ m)
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ x ^ m ∣ y ^ p
have rw : x ^ m ∣ (y - x + x) ^ p
Tactic: rw [← sub_add_cancel y x]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ x ^ m ∣ (y - x + x) ^ p
have apply : (y - x) ^ n = 0
Tactic: apply (h_comm.symm.sub_left rfl).pow_dvd_add_pow_of_pow_eq_zero_left hp _
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (y - x) ^ n = 0
have rw : (-(x - y)) ^ n = 0
Tactic: rw [← neg_sub x y, neg_pow, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
rw : (-(x - y)) ^ n = 0
⊢ (y - x) ^ n = 0
have rw₁ : HPow.hPow (α := R) (-1) n * (x - y) ^ n = 0
Tactic: rw [← neg_sub x y, neg_pow, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
rw : (-(x - y)) ^ n = 0
rw₁ : HPow.hPow (α := R) (-1) n * (x - y) ^ n = 0
⊢ (y - x) ^ n = 0
have rw₂ : HPow.hPow (α := R) (-1) n * 0 = 0
Tactic: rw [← neg_sub x y, neg_pow, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
rw : (-(x - y)) ^ n = 0
rw₁ : HPow.hPow (α := R) (-1) n * (x - y) ^ n = 0
rw₂ : HPow.hPow (α := R) (-1) n * 0 = 0
⊢ (y - x) ^ n = 0
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← neg_sub x y, neg_pow, h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ y ^ p
have rw : x ^ m ∣ (-y) ^ p * HPow.hPow (α := R) (-1) p
Tactic: rw [← neg_neg y, neg_pow']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p * HPow.hPow (α := R) (-1) p
have h₁ : x ^ m ∣ (-y) ^ p
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p
have h₁ : (x - -y) ^ n = 0
Tactic: apply h_comm.neg_right.pow_dvd_pow_of_sub_pow_eq_zero hp
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (x - y) ^ p
have rw : y ^ m ∣ (y - x) ^ p * HPow.hPow (α := R) (-1) p
Tactic: rw [← neg_sub y x, neg_pow']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (y - x) ^ p * HPow.hPow (α := R) (-1) p
have h : y ^ m ∣ (y - x) ^ p
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
p a b c d x y : R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ (a * d - b * c) * x
have obtain : ∀ (k1 : R) (hk1 : a * x + b * y = p * k1), p ∣ (a * d - b * c) * x
Tactic: obtain ⟨k1, hk1⟩ := h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
p a b c d x y : R
h2 : p ∣ c * x + d * y
k1 : R
hk1 : a * x + b * y = p * k1
⊢ p ∣ (a * d - b * c) * x
have obtain : ∀ (k2 : R) (hk2 : c * x + d * y = p * k2), p ∣ (a * d - b * c) * x
Tactic: obtain ⟨k2, hk2⟩ := h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ p ∣ (a * d - b * c) * x
have refine : (a * d - b * c) * x = p * (d * k1 - b * k2)
Tactic: refine ⟨d * k1 - b * k2, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : CommRing R
p a b c d x y : R
inst_1 : GCDMonoid R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ (a * d - b * c) * @gcd _ CommSemiring.toCommMonoidWithZero _ x y
have rw : p ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ ((a * d - b * c) * x) ((a * d - b * c) * y)
Tactic: rw [← (gcd_mul_left' (a * d - b * c) x y).dvd_iff_dvd_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
x y : R
⊢ Associated |x| y ↔ Associated x y
have inl : ∀ (h : |x| = x), Associated |x| y ↔ Associated x y
Tactic: obtain h | h := abs_choice x
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
x y : R
inl : ∀ (h : |x| = x), Associated |x| y ↔ Associated x y
⊢ Associated |x| y ↔ Associated x y
have inr : ∀ (h : |x| = -x), Associated |x| y ↔ Associated x y
Tactic: obtain h | h := abs_choice x
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
x y : R
⊢ Associated x |y| ↔ Associated x y
have rw : Associated |y| x ↔ Associated x y
Tactic: rw [Associated.comm, associated_abs_left_iff, Associated.comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
x y : R
rw : Associated |y| x ↔ Associated x y
⊢ Associated x |y| ↔ Associated x y
have rw₁ : Associated y x ↔ Associated x y
Tactic: rw [Associated.comm, associated_abs_left_iff, Associated.comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Divisibility.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
x y : R
rw : Associated |y| x ↔ Associated x y
rw₁ : Associated y x ↔ Associated x y
⊢ Associated x |y| ↔ Associated x y
have rw₂ : Associated x y ↔ Associated x y
Tactic: rw [Associated.comm, associated_abs_left_iff, Associated.comm]