awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : MulZeroClass α
P : Prop
inst_1 : Decidable P
a b : α
⊢ (a * if P then b else 0) = if P then a * b else 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : MulZeroClass α
P Q : Prop
inst_1 : Decidable P
inst_2 : Decidable Q
a b : α
⊢ ((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0

Tactic:
simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]

Premises used: MulZeroClass.zero_mul, mul_ite, and_comm, MulZeroClass.mul_zero, ite_mul, ite_and
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u_1
inst : MulZeroOneClass α
P : Prop
inst_1 : Decidable P
a : α
⊢ (a * if P then 1 else 0) = if P then a else 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u_1
inst : MulZeroOneClass α
P : Prop
inst_1 : Decidable P
a : α
⊢ (if P then 1 else 0) * a = if P then a else 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : CommSemiring α
a b : α
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b

Tactic:
simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]

Premises used: add_mul, add_assoc, two_mul, mul_comm, mul_add
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : CommSemiring α
a b : α
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2

Tactic:
simp only [sq, add_mul_self_eq]

Premises used: sq, add_mul_self_eq
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : CommSemiring α
a b : α
rw :
  HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
rw₁ :
  HPow.hPow (β := ℕ) a 2 + (2 * a * b + HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
rw₂ :
  HPow.hPow (β := ℕ) a 2 + (HPow.hPow (β := ℕ) b 2 + 2 * a * b) =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
rw₃ rw₄ :
  HPow.hPow (β := ℕ) a 2 + (HPow.hPow (β := ℕ) b 2 + 2 * a * b) =
    HPow.hPow (β := ℕ) a 2 + (HPow.hPow (β := ℕ) b 2 + 2 * a * b)
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b

Tactic:
rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]

Premises used: add_sq, add_assoc, add_comm, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : HasDistribNeg α
a b : α
⊢ -a * b = -(a * b)

Tactic:
HasDistribNeg.neg_mul _ _

Premises used: HasDistribNeg.neg_mul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : HasDistribNeg α
a b : α
⊢ a * -b = -(a * b)

Tactic:
HasDistribNeg.mul_neg _ _

Premises used: HasDistribNeg.mul_neg
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : HasDistribNeg α
a b : α
⊢ -a * -b = a * b

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : HasDistribNeg α
a b : α
⊢ -(a * b) = -a * b

Tactic:
(neg_mul _ _).symm

Premises used: neg_mul, Eq.symm
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : HasDistribNeg α
a b : α
⊢ -(a * b) = a * -b

Tactic:
(mul_neg _ _).symm

Premises used: Eq.symm, mul_neg
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : HasDistribNeg α
a b : α
⊢ -a * b = a * -b

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : HasDistribNeg α
a : α
⊢ -a = -1 * a

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : HasDistribNeg α
a : α
⊢ a * -1 = -a

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : HasDistribNeg α
a : α
⊢ -1 * a = -a

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Defs
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
rw₃ rw₄ : Eq.{u + 1} (α := α) 0 0
⊢ Eq.{u + 1} (α := α) (-0) 0

Tactic:
rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, neg_mul, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
rw : (-a + a) * b = 0
rw₁ : 0 * b = 0
rw₂ rw₃ : Eq.{u + 1} (α := α) 0 0
⊢ -a * b + a * b = 0

Tactic:
rw [← right_distrib, neg_add_cancel, zero_mul]

Premises used: NonUnitalNonAssocRing.zero_mul, neg_add_cancel, right_distrib
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
R : Type v
inst : NonUnitalNonAssocRing α
a b : α
rw : a * (-b + b) = 0
rw₁ : a * 0 = 0
rw₂ rw₃ : Eq.{u + 1} (α := α) 0 0
⊢ a * -b + a * b = 0

Tactic:
rw [← left_distrib, neg_add_cancel, mul_zero]

Premises used: NonUnitalNonAssocRing.mul_zero, neg_add_cancel, left_distrib
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b - c) = a * b - a * c

Tactic:
simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)

Premises used: sub_eq_add_neg, neg_mul_eq_mul_neg, mul_add, Neg.neg
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonUnitalNonAssocRing α
a b c : α
⊢ (a - b) * c = a * c - b * c

Tactic:
simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c

Premises used: add_mul, sub_eq_add_neg, neg_mul_eq_neg_mul, Neg.neg
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : a * b - 1 * b = a * b - b
rw₁ rw₂ : a * b - b = a * b - b
⊢ (a - 1) * b = a * b - b

Tactic:
rw [sub_mul, one_mul]

Premises used: sub_mul, one_mul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : a * b - a * 1 = a * b - a
rw₁ rw₂ : a * b - a = a * b - a
⊢ a * (b - 1) = a * b - a

Tactic:
rw [mul_sub, mul_one]

Premises used: mul_sub, mul_one
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : 1 * b - a * b = b - a * b
rw₁ rw₂ : b - a * b = b - a * b
⊢ (1 - a) * b = b - a * b

Tactic:
rw [sub_mul, one_mul]

Premises used: sub_mul, one_mul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocRing α
a b : α
rw : a * 1 - a * b = a - a * b
rw₁ rw₂ : a - a * b = a - a * b
⊢ a * (1 - b) = a - a * b

Tactic:
rw [mul_sub, mul_one]

Premises used: mul_sub, mul_one
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocRing α
a b c : α
rw : (a - a * b) * c = a * c - a * b * c
rw₁ rw₂ : a * c - a * b * c = a * c - a * b * c
⊢ a * (1 - b) * c = a * c - a * b * c

Tactic:
rw [mul_one_sub, sub_mul]

Premises used: mul_one_sub, sub_mul
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 : β)
rw : f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)
⊢ a ∣ b

Tactic:
rw [← f.left_inv a, ← f.left_inv b]

Premises used: MulEquiv.toEquiv, Equiv.left_inv
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 : β)
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)

Tactic:
map_dvd f.symm h

Premises used: map_dvd, MulEquiv.symm
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 : β)
⊢ f.invFun (f.toFun a) ∣ f.invFun (f.toFun b)

Tactic:
exact map_dvd f.symm h

Premises used: map_dvd, MulEquiv.symm
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 : β
⊢ ∃ (c : α), (f : (a : α) → β) c = b

Tactic:
EquivLike.surjective f b

Premises used: EquivLike.surjective
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 : β
obtain :
  ∀ (c : α),
    Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β) ↔
      a ∣ (MulEquiv.symm (↑f : α ≃* β) : (a : β) → α) ((f : (a : α) → β) c : β)
⊢ (f : (a : α) → β) a ∣ b ↔ a ∣ (MulEquiv.symm (↑f : α ≃* β) : (a : β) → α) b

Tactic:
obtain ⟨c, rfl⟩ : ∃ c, f c = b := EquivLike.surjective f b

Premises used: EquivLike.surjective, rfl
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 c : α
⊢ Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) c : β) ↔
    a ∣ (MulEquiv.symm (↑f : α ≃* β) : (a : β) → α) ((f : (a : α) → β) c : β)

Tactic:
simp [map_dvd_iff]

Premises used: map_dvd_iff
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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
⊢ (f : (a : α) → β) a ∣ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) c : β)

Tactic:
rw [← map_dvd_iff f, map_mul] at h

Premises used: map_dvd_iff, map_mul
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 : β)
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₂
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h

Premises used: DecompositionMonoid.primal
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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₂

Tactic:
⟨symm f a₁, symm f a₂, ?_⟩

Premises used: Exists.intro, MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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₂
refine :
  (symm (↑f : α ≃* β) : (a : β) → α) a₁ ∣ b ∧
    (symm (↑f : α ≃* β) : (a : β) → α) a₂ ∣ c ∧
      a =
        HMul.hMul (α := α) (β := α) ((symm (↑f : α ≃* β) : (a : β) → α) a₁ : α)
          ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α)
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
refine ⟨symm f a₁, symm f a₂, ?_⟩
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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₂
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₂
⊢ (symm (↑f : α ≃* β) : (a : β) → α) a₁ ∣ b ∧
    (symm (↑f : α ≃* β) : (a : β) → α) a₂ ∣ c ∧
      a =
        HMul.hMul (α := α) (β := α) ((symm (↑f : α ≃* β) : (a : β) → α) a₁ : α)
          ((symm (↑f : α ≃* β) : (a : β) → α) a₂ : α)

Tactic:
simp_rw [← map_dvd_iff f, ← map_mul, eq_symm_apply]

Premises used: MulEquiv.eq_symm_apply, map_dvd_iff, map_mul
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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₂
erw :
  a₁ ∣ (f : (a : α) → β) b ∧
    Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) ((symm (↑f : α ≃* β) : (a : β) → α) 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₂

Tactic:
erw [(f : α ≃* β).apply_symm_apply]

Premises used: MulEquivClass.toMulEquiv, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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₂
erw : 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₂

Tactic:
erw [(f : α ≃* β).apply_symm_apply]

Premises used: MulEquivClass.toMulEquiv, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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₂
iterate : 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₂

Tactic:
iterate 2 erw [(f : α ≃* β).apply_symm_apply]

Premises used: MulEquivClass.toMulEquiv, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 ∧ a₂ ∣ (f : (a : α) → β) c ∧ ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂

Tactic:
h
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 ∧ a₂ ∣ (f : (a : α) → β) c ∧ ((↑f : α ≃* β) : (a : α) → β) a = a₁ * a₂

Tactic:
exact h
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
G : Type u_4
inst_4 : LeftCancelSemigroup G
g x : G
⊢ (fun (x : { a : G // g ∣ a }) ↦
        (match (motive := { a : G // g ∣ a } → G) x with
          | ⟨val, h⟩ => Exists.choose (p := fun (c : G) ↦ val = g * c) h :
          G))
      ((fun (a : G) ↦ (Subtype.mk (p := fun (a : G) ↦ g ∣ a) (g * a) ⋯ : { a : G // g ∣ a })) x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Semigroup α
inst_1 : Semigroup β
F : Type u_3
inst_2 : EquivLike F α β
inst_3 : MulEquivClass F α β
G : Type u_4
inst_4 : LeftCancelSemigroup G
g w : G
⊢ Eq (α := { a : G // g ∣ a })
    ((fun (a : G) ↦ (Subtype.mk (p := fun (a : G) ↦ g ∣ a) (g * a) ⋯ : { a : G // g ∣ a }))
      ((fun (x : { a : G // g ∣ a }) ↦
          (match (motive := { a : G // g ∣ a } → G) x with
            | ⟨val, h⟩ => Exists.choose (p := fun (c : G) ↦ val = g * c) h :
            G))
        (Subtype.mk (p := fun (a : G) ↦ g ∣ a) (g * w) ⋯)))
    (Subtype.mk (p := fun (a : G) ↦ g ∣ a) (g * w) ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
G : Type u_4
inst : LeftCancelSemigroup G
g a : G
⊢ (↑((Equiv.dvd g : (a : G) → { a : G // g ∣ a }) a) : G) = g * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Add α
inst_1 : Semigroup α
inst_2 : LeftDistribClass α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
d : α
hd : b = a * d
e : α
he : c = a * e
⊢ a * (d + e) = b + c

Tactic:
simp [left_distrib, hd, he]

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Semiring α
a b c : α
m n : ℕ
ha : c ^ m ∣ a
hb : c ^ n ∣ b
⊢ c ^ min m n ∣ a + b

Tactic:
((pow_dvd_pow c (m.min_le_left n)).trans ha).add ((pow_dvd_pow c (m.min_le_right n)).trans hb)

Premises used: Nat.min_le_right, pow_dvd_pow, Dvd.dvd.add, Nat.min_le_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalCommSemiring α
d x y : α
hdx : d ∣ x
hdy : d ∣ y
a b : α
⊢ d ∣ a * x + b * y

Tactic:
dvd_add (hdx.mul_left a) (hdy.mul_left b)

Premises used: Dvd.dvd.mul_left, dvd_add
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
inst_1 : HasDistribNeg α
a b : α
⊢ (∃ (b_1 : α), -b = HMul.hMul (β := α) a ((Equiv.symm (Equiv.neg α) : (a : α) → α) b_1 : α)) ↔ a ∣ b

Tactic:
simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_inj, Dvd.dvd]

Premises used: Dvd.dvd, Equiv.neg_apply, neg_inj, Equiv.neg_symm, mul_neg
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Semigroup α
inst_1 : HasDistribNeg α
a b : α
⊢ (∃ (b_1 : α), b = HMul.hMul (β := α) (-a) ((Equiv.symm (Equiv.neg α) : (a : α) → α) b_1 : α)) ↔ a ∣ b

Tactic:
simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_mul, neg_neg, Dvd.dvd]

Premises used: Dvd.dvd, neg_neg, Equiv.neg_apply, Equiv.neg_symm, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
⊢ a ∣ b - c

Tactic:
simpa only [← sub_eq_add_neg] using h₁.add h₂.neg_right

Premises used: sub_eq_add_neg, Dvd.dvd.add, Dvd.dvd.neg_right
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ c
H : a ∣ b + c
⊢ a ∣ b

Tactic:
simpa only [add_sub_cancel_right] using dvd_sub H h

Premises used: dvd_sub, add_sub_cancel_right
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
rw : a ∣ c + b ↔ a ∣ c
⊢ a ∣ b + c ↔ a ∣ c

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c

Tactic:
dvd_add_left h

Premises used: dvd_add_left
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ c + b ↔ a ∣ c

Tactic:
exact dvd_add_left h

Premises used: dvd_add_left
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b

Tactic:
simpa only [← sub_eq_add_neg] using dvd_add_left (dvd_neg.2 h)

Premises used: Iff.mpr, sub_eq_add_neg, dvd_neg, dvd_add_left
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b
rw : a ∣ b + -c ↔ a ∣ c
rw₁ : a ∣ -c ↔ a ∣ c
rw₂ rw₃ : a ∣ c ↔ a ∣ c
⊢ a ∣ b - c ↔ a ∣ c

Tactic:
rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]

Premises used: dvd_add_right, sub_eq_add_neg, dvd_neg
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
h : a ∣ b - c
rw : a ∣ b - c + c ↔ a ∣ c
rw₁ rw₂ : a ∣ c ↔ a ∣ c
⊢ a ∣ b ↔ a ∣ c

Tactic:
rw [← sub_add_cancel b c, dvd_add_right h]

Premises used: dvd_add_right, sub_add_cancel
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalRing α
a b c : α
rw : a ∣ -(b - c) ↔ a ∣ c - b
rw₁ rw₂ : a ∣ c - b ↔ a ∣ c - b
⊢ a ∣ b - c ↔ a ∣ c - b

Tactic:
rw [← dvd_neg, neg_sub]

Premises used: neg_sub, dvd_neg
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ a ∣ a + b ↔ a ∣ b

Tactic:
dvd_add_right (dvd_refl a)

Premises used: dvd_add_right, dvd_refl
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ a ∣ b + a ↔ a ∣ b

Tactic:
dvd_add_left (dvd_refl a)

Premises used: dvd_add_left, dvd_refl
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ a ∣ a - b ↔ a ∣ b

Tactic:
dvd_sub_right dvd_rfl

Premises used: dvd_sub_right, dvd_rfl
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ a ∣ b - a ↔ a ∣ b

Tactic:
dvd_sub_left dvd_rfl

Premises used: dvd_sub_left, dvd_rfl
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
⊢ k ∣ a * (x - y) + (a - b) * y

Tactic:
dvd_add (hxy.mul_left a) (hab.mul_right y)

Premises used: Dvd.dvd.mul_right, Dvd.dvd.mul_left, dvd_add
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
h : a * x - b * y = a * (x - y) + (a - b) * y
⊢ k ∣ a * x - b * y

Tactic:
convert! dvd_add (hxy.mul_left a) (hab.mul_right y) using 1

Premises used: Dvd.dvd.mul_right, Dvd.dvd.mul_left, dvd_add
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
Goal:
α : Type u_1
inst : NonUnitalCommRing α
k a b x y : α
hab : k ∣ a - b
hxy : k ∣ x - y
h : a * x - b * y = a * x - a * y + (a * y - b * y)
⊢ a * x - b * y = a * (x - y) + (a - b) * y

Tactic:
rw [mul_sub_left_distrib, mul_sub_right_distrib]

Premises used: mul_sub_left_distrib, mul_sub_right_distrib
-- Module: Mathlib.Algebra.Ring.Divisibility.Basic
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 - a * y + (a * y - b * y)

Tactic:
simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]

Premises used: add_assoc, sub_eq_add_neg, neg_add_cancel_left