awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Ring α
a b : α
u : αˣ
rw : b = b * ((↑u : α) * (↑u⁻¹ : α))
rw₁ : b = b * 1
rw₂ rw₃ : b = b
⊢ b = b * (↑u : α) * (↑u⁻¹ : α)

Tactic:
rw [mul_assoc, Units.mul_inv, mul_one]

Premises used: mul_assoc, Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
β : Type v
inst : Ring α
F : Type u_1
inst_1 : Ring β
inst_2 : FunLike F α β
inst_3 : RingHomClass F α β
f : F
u : αˣ
⊢ Eq.{v + 1} (α := β) (↑(((map (↑f : α →* β) : MonoidHom.{u, v} αˣ βˣ) : (a : αˣ) → βˣ) (-u)) : β)
    (↑(-((map (↑f : α →* β) : MonoidHom.{u, v} αˣ βˣ) : (a : αˣ) → βˣ) u) : β)

Tactic:
simp only [coe_map, Units.val_neg, MonoidHom.coe_coe, map_neg]

Premises used: Units.coe_map, MonoidHom.coe_coe, map_neg, Units.val_neg
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
β : Type v
inst : Ring α
F : Type u_1
inst_1 : Ring β
inst_2 : FunLike F α β
inst_3 : RingHomClass F α β
f : F
⊢ Eq.{v + 1} (α := βˣ) (((map (↑f : α →* β) : MonoidHom.{u, v} αˣ βˣ) : (a : αˣ) → βˣ) (-1)) (-1)

Tactic:
simp only [Units.map_neg, map_one]

Premises used: Units.map_neg, map_one
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
a : α
⊢ IsUnit (-a) ↔ IsUnit a

Tactic:
⟨fun h => neg_neg a ▸ h.neg, IsUnit.neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, IsUnit.neg
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Monoid α
inst_1 : HasDistribNeg α
⊢ IsUnit.{u} (M := α) (-1)

Tactic:
isUnit_one.neg

Premises used: isUnit_one, IsUnit.neg
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : Ring α
x y : α
⊢ IsUnit (x - y) ↔ IsUnit (y - x)

Tactic:
(IsUnit.neg_iff _).symm.trans <| neg_sub x y ▸ Iff.rfl

Premises used: IsUnit.neg_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
simp :
  a * (↑u₁⁻¹ : α) + b * (↑u₂⁻¹ : α) =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₁ : α) * b * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α))
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * (↑u₂ : α) + (↑u₁ : α) * b) /ₚ (u₁ * u₂)

Tactic:
simp only [divp, add_mul, mul_inv_rev, val_mul]

Premises used: add_mul, divp, mul_inv_rev, Units.val_mul
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
⊢ a * (↑u₁⁻¹ : α) + b * (↑u₂⁻¹ : α) =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₁ : α) * b * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α))

Tactic:
rw [mul_comm (↑u₁ * b), mul_comm b]

Premises used: HMul.hMul, mul_comm
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
rw₁ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₂ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₃ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
rw₄ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
rw₅ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * 1 * b
rw₆ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * 1 * b
rw₇ rw₈ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)

Tactic:
rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]

Premises used: Units.val, mul_assoc, Units.inv_mul, Units.mul_inv, Inv.inv, mul_one
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
inst : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ - b /ₚ u₂ = (a * (↑u₂ : α) - (↑u₁ : α) * b) /ₚ (u₁ * u₂)

Tactic:
simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]

Premises used: sub_eq_add_neg, Units.divp_add_divp, Units.neg_divp, mul_neg
-- Module: Mathlib.Algebra.Ring.Units
Goal:
R : Type x
inst : Semiring R
a : Rˣ
b : R
rw : (↑a : R) + b = (↑a : R) * 1 + (↑a : R) * ((↑a⁻¹ : R) * b)
rw₁ : (↑a : R) + b = (↑a : R) + (↑a : R) * ((↑a⁻¹ : R) * b)
rw₂ : (↑a : R) + b = (↑a : R) + (↑a : R) * (↑a⁻¹ : R) * b
rw₃ : (↑a : R) + b = (↑a : R) + 1 * b
rw₄ rw₅ : (↑a : R) + b = (↑a : R) + b
⊢ (↑a : R) + b = (↑a : R) * (1 + (↑a⁻¹ : R) * b)

Tactic:
rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]

Premises used: mul_assoc, Units.mul_inv, mul_add, mul_one, one_mul
-- Module: Mathlib.Algebra.Ring.Units
Goal:
α : Type u
β : Type v
inst : Semiring α
inst_1 : Semiring β
f : α →+* β
a : α
⊢ IsUnit a → IsUnit.{v} (M := β) ((f : (a : α) → β) a : β)

Tactic:
IsUnit.map f

Premises used: IsUnit.map
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a b c : WithZero α
zero : 0 * (b + c) = 0 * b + 0 * c
coe : ∀ (a : α), (↑a : WithZero α) * (b + c) = (↑a : WithZero α) * b + (↑a : WithZero α) * c
⊢ a * (b + c) = a * b + a * c

Tactic:
cases a
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
b c : WithZero α
⊢ 0 * (b + c) = 0 * b + 0 * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
b c : WithZero α
a : α
coe : (↑a : WithZero α) * (0 + c) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * c
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithZero α) * ((↑a_1 : WithZero α) + c) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * c
⊢ (↑a : WithZero α) * (b + c) = (↑a : WithZero α) * b + (↑a : WithZero α) * c

Tactic:
cases b
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
c : WithZero α
a : α
coe : (↑a : WithZero α) * HAdd.hAdd (α := WithZero α) 0 0 = (↑a : WithZero α) * 0 + (↑a : WithZero α) * 0
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithZero α) * (0 + (↑a_1 : WithZero α)) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * (↑a_1 : WithZero α)
⊢ (↑a : WithZero α) * (0 + c) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * c

Tactic:
cases c
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
c : WithZero α
a a_1 : α
coe : (↑a : WithZero α) * ((↑a_1 : WithZero α) + 0) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * 0
coe₁ :
  ∀ (a_2 : α),
    (↑a : WithZero α) * ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) =
      (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * (↑a_2 : WithZero α)
⊢ (↑a : WithZero α) * ((↑a_1 : WithZero α) + c) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * c

Tactic:
cases c
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a : α
⊢ (↑a : WithZero α) * HAdd.hAdd (α := WithZero α) 0 0 = (↑a : WithZero α) * 0 + (↑a : WithZero α) * 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a : α
⊢ (↑a : WithZero α) * HAdd.hAdd (α := WithZero α) 0 0 = (↑a : WithZero α) * 0 + (↑a : WithZero α) * 0

Tactic:
try rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a a_1 : α
⊢ (↑a : WithZero α) * (0 + (↑a_1 : WithZero α)) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * (↑a_1 : WithZero α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a a_1 : α
⊢ (↑a : WithZero α) * (0 + (↑a_1 : WithZero α)) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * (↑a_1 : WithZero α)

Tactic:
try rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a a_1 : α
⊢ (↑a : WithZero α) * ((↑a_1 : WithZero α) + 0) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a a_1 : α
⊢ (↑a : WithZero α) * ((↑a_1 : WithZero α) + 0) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * 0

Tactic:
try rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a a_1 a_2 : α
⊢ (↑a : WithZero α) * ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) =
    (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * (↑a_2 : WithZero α)

Tactic:
congr_arg some (left_distrib _ _ _)

Premises used: Option.some, Option.merge, congr_arg, WithZero, Option.map₂, left_distrib
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a a_1 a_2 : α
⊢ (↑a : WithZero α) * ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) =
    (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * (↑a_2 : WithZero α)

Tactic:
exact congr_arg some (left_distrib _ _ _)

Premises used: Option.some, congr_arg, left_distrib
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a b c : WithZero α
zero : (a + b) * 0 = a * 0 + b * 0
coe : ∀ (a_1 : α), (a + b) * (↑a_1 : WithZero α) = a * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
⊢ (a + b) * c = a * c + b * c

Tactic:
cases c
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a b : WithZero α
⊢ (a + b) * 0 = a * 0 + b * 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a b : WithZero α
a_1 : α
coe : (0 + b) * (↑a_1 : WithZero α) = 0 * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
coe₁ :
  ∀ (a : α),
    ((↑a : WithZero α) + b) * (↑a_1 : WithZero α) = (↑a : WithZero α) * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
⊢ (a + b) * (↑a_1 : WithZero α) = a * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
b : WithZero α
a : α
coe : HAdd.hAdd (α := WithZero α) 0 0 * (↑a : WithZero α) = 0 * (↑a : WithZero α) + 0 * (↑a : WithZero α)
coe₁ :
  ∀ (a_1 : α),
    (0 + (↑a_1 : WithZero α)) * (↑a : WithZero α) = 0 * (↑a : WithZero α) + (↑a_1 : WithZero α) * (↑a : WithZero α)
⊢ (0 + b) * (↑a : WithZero α) = 0 * (↑a : WithZero α) + b * (↑a : WithZero α)

Tactic:
cases b
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
b : WithZero α
a a_1 : α
coe : ((↑a_1 : WithZero α) + 0) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + 0 * (↑a : WithZero α)
coe₁ :
  ∀ (a_2 : α),
    ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) * (↑a : WithZero α) =
      (↑a_1 : WithZero α) * (↑a : WithZero α) + (↑a_2 : WithZero α) * (↑a : WithZero α)
⊢ ((↑a_1 : WithZero α) + b) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + b * (↑a : WithZero α)

Tactic:
cases b
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a : α
⊢ HAdd.hAdd (α := WithZero α) 0 0 * (↑a : WithZero α) = 0 * (↑a : WithZero α) + 0 * (↑a : WithZero α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a : α
⊢ HAdd.hAdd (α := WithZero α) 0 0 * (↑a : WithZero α) = 0 * (↑a : WithZero α) + 0 * (↑a : WithZero α)

Tactic:
try rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a a_1 : α
⊢ (0 + (↑a_1 : WithZero α)) * (↑a : WithZero α) = 0 * (↑a : WithZero α) + (↑a_1 : WithZero α) * (↑a : WithZero α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a a_1 : α
⊢ (0 + (↑a_1 : WithZero α)) * (↑a : WithZero α) = 0 * (↑a : WithZero α) + (↑a_1 : WithZero α) * (↑a : WithZero α)

Tactic:
try rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a a_1 : α
⊢ ((↑a_1 : WithZero α) + 0) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + 0 * (↑a : WithZero α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a a_1 : α
⊢ ((↑a_1 : WithZero α) + 0) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + 0 * (↑a : WithZero α)

Tactic:
try rfl
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a a_1 a_2 : α
⊢ ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) * (↑a : WithZero α) =
    (↑a_1 : WithZero α) * (↑a : WithZero α) + (↑a_2 : WithZero α) * (↑a : WithZero α)

Tactic:
congr_arg some (right_distrib _ _ _)

Premises used: Option.some, Option.merge, congr_arg, WithZero, right_distrib, Option.map₂
-- Module: Mathlib.Algebra.Ring.WithZero
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a a_1 a_2 : α
⊢ ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) * (↑a : WithZero α) =
    (↑a_1 : WithZero α) * (↑a : WithZero α) + (↑a_2 : WithZero α) * (↑a : WithZero α)

Tactic:
exact congr_arg some (right_distrib _ _ _)

Premises used: Option.some, congr_arg, right_distrib
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
c : RingCon A
⊢ Function.Surjective (α := A) (β := c.Quotient) (⇑(mkₐ S c) : (a : A) → c.Quotient)

Tactic:
mk'_surjective c

Premises used: RingCon.mk'_surjective
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
c : RingCon A
s : S
⊢ Eq.{uA + 1} (α := c.Quotient) ((↑((algebraMap S A : (a : S) → A) s) : c.Quotient) : c.Quotient)
    ((algebraMap S c.Quotient : (a : S) → c.Quotient) s : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, rfl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
rw : Rel r (b + a) (c + a)
⊢ Rel r (a + b) (a + c)

Tactic:
rw [add_comm a b, add_comm a c]

Premises used: add_comm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)

Tactic:
Rel.add_left h

Premises used: RingQuot.Rel.add_left
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)

Tactic:
exact Rel.add_left h

Premises used: RingQuot.Rel.add_left
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Ring R
r : R → R → Prop
a b : R
h : Rel r a b
⊢ Rel r (-a) (-b)

Tactic:
simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, Rel.mul_right h]

Premises used: neg_eq_neg_one_mul, RingQuot.Rel.mul_right
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Ring R
r : R → R → Prop
a b c : R
h : Rel r a b
⊢ Rel r (a - c) (b - c)

Tactic:
simp only [sub_eq_add_neg, h.add_left]

Premises used: sub_eq_add_neg, RingQuot.Rel.add_left
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Ring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a - b) (a - c)

Tactic:
simp only [sub_eq_add_neg, h.neg.add_right]

Premises used: RingQuot.Rel.add_right, sub_eq_add_neg, RingQuot.Rel.neg
-- Module: Mathlib.Algebra.RingQuot
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
r : A → A → Prop
k : S
a b : A
h : Rel r a b
⊢ Rel r (k • a) (k • b)

Tactic:
simp only [Algebra.smul_def, Rel.mul_right h]

Premises used: RingQuot.Rel.mul_right, Algebra.smul_def
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x * c) (y * d)

Tactic:
(Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_

Premises used: Relation.EqvGen.trans, RingQuot.Rel.mul_left, Relation.EqvGen.rel
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : Relation.EqvGen (Rel r) (y * c) (y * d)
⊢ Relation.EqvGen (Rel r) (x * c) (y * d)

Tactic:
refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_

Premises used: Relation.EqvGen.trans, RingQuot.Rel.mul_left, Relation.EqvGen.rel
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
hcd : Rel r x_1 y_1
⊢ Relation.EqvGen (Rel r) (y * x_1) (y * y_1)

Tactic:
Relation.EqvGen.rel _ _ hcd.mul_right

Premises used: Relation.EqvGen.rel, RingQuot.Rel.mul_right
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
hcd : Rel r x_1 y_1
⊢ Relation.EqvGen (Rel r) (y * x_1) (y * y_1)

Tactic:
exact Relation.EqvGen.rel _ _ hcd.mul_right

Premises used: Relation.EqvGen.rel, RingQuot.Rel.mul_right
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 : R
⊢ Relation.EqvGen (Rel r) (y * x_1) (y * x_1)

Tactic:
Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 : R
⊢ Relation.EqvGen (Rel r) (y * x_1) (y * x_1)

Tactic:
exact Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h : Relation.EqvGen (Rel r) (y * x_1) (y * y_1)
⊢ Relation.EqvGen (Rel r) (y * y_1) (y * x_1)

Tactic:
h.symm _ _

Premises used: Relation.EqvGen.symm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 y_1 : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h : Relation.EqvGen (Rel r) (y * x_1) (y * y_1)
⊢ Relation.EqvGen (Rel r) (y * y_1) (y * x_1)

Tactic:
exact h.symm _ _

Premises used: Relation.EqvGen.symm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 y_1 z : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h_2 : Relation.EqvGen (Rel r) y_1 z
h : Relation.EqvGen (Rel r) (y * x_1) (y * y_1)
h' : Relation.EqvGen (Rel r) (y * y_1) (y * z)
⊢ Relation.EqvGen (Rel r) (y * x_1) (y * z)

Tactic:
h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d x_1 y_1 z : R
h_1 : Relation.EqvGen (Rel r) x_1 y_1
h_2 : Relation.EqvGen (Rel r) y_1 z
h : Relation.EqvGen (Rel r) (y * x_1) (y * y_1)
h' : Relation.EqvGen (Rel r) (y * y_1) (y * z)
⊢ Relation.EqvGen (Rel r) (y * x_1) (y * z)

Tactic:
exact h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y * x) (y * y_1)
rel₁ : ∀ (x : R), Relation.EqvGen (Rel r) (y * x) (y * x)
rel₂ :
  ∀ (x y_1 : R),
    Relation.EqvGen (Rel r) x y_1 →
      ∀ (h : Relation.EqvGen (Rel r) (y * x) (y * y_1)), Relation.EqvGen (Rel r) (y * y_1) (y * x)
rel₃ :
  ∀ (x y_1 z : R),
    Relation.EqvGen (Rel r) x y_1 →
      Relation.EqvGen (Rel r) y_1 z →
        ∀ (h : Relation.EqvGen (Rel r) (y * x) (y * y_1)) (h' : Relation.EqvGen (Rel r) (y * y_1) (y * z)),
          Relation.EqvGen (Rel r) (y * x) (y * z)
⊢ Relation.EqvGen (Rel r) (y * c) (y * d)

Tactic:
induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'

Premises used: Relation.EqvGen.refl, symm, refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d x_1 y : R
hcd : Rel r x_1 y
⊢ Relation.EqvGen (Rel r) (x * x_1) (x * y)

Tactic:
Relation.EqvGen.rel _ _ hcd.mul_right

Premises used: Relation.EqvGen.rel, RingQuot.Rel.mul_right
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d x_1 y : R
hcd : Rel r x_1 y
⊢ Relation.EqvGen (Rel r) (x * x_1) (x * y)

Tactic:
exact Relation.EqvGen.rel _ _ hcd.mul_right

Premises used: Relation.EqvGen.rel, RingQuot.Rel.mul_right
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d x_1 : R
⊢ Relation.EqvGen (Rel r) (x * x_1) (x * x_1)

Tactic:
Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d x_1 : R
⊢ Relation.EqvGen (Rel r) (x * x_1) (x * x_1)

Tactic:
exact Relation.EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d x_1 y : R
h_1 : Relation.EqvGen (Rel r) x_1 y
h : Relation.EqvGen (Rel r) (x * x_1) (x * y)
⊢ Relation.EqvGen (Rel r) (x * y) (x * x_1)

Tactic:
h.symm _ _

Premises used: Relation.EqvGen.symm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d x_1 y : R
h_1 : Relation.EqvGen (Rel r) x_1 y
h : Relation.EqvGen (Rel r) (x * x_1) (x * y)
⊢ Relation.EqvGen (Rel r) (x * y) (x * x_1)

Tactic:
exact h.symm _ _

Premises used: Relation.EqvGen.symm
-- Module: Mathlib.Algebra.RingQuot
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d x_1 y z : R
h_1 : Relation.EqvGen (Rel r) x_1 y
h_2 : Relation.EqvGen (Rel r) y z
h : Relation.EqvGen (Rel r) (x * x_1) (x * y)
h' : Relation.EqvGen (Rel r) (x * y) (x * z)
⊢ Relation.EqvGen (Rel r) (x * x_1) (x * z)

Tactic:
h.trans _ _ _ h'

Premises used: Relation.EqvGen.trans