awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a b : R
inst_1 : NoZeroDivisors R
h : Commute a b
rw : HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₃ : a = -b ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₄ : a = -b ∨ a = b ↔ a = b ∨ a = -b
rw₅ rw₆ : a = b ∨ a = -b ↔ a = b ∨ a = -b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b

Tactic:
rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]

Premises used: sub_eq_zero, add_eq_zero_iff_eq_neg, Commute.sq_sub_sq, mul_eq_zero, or_comm
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = -1
rw : HPow.hPow (α := R) (-1) n * -1 = 1
rw₁ : HMul.hMul (α := R) (-1) (-1) = 1
rw₂ : Eq.{u + 1} (α := R) (- -1) 1
rw₃ rw₄ : Eq.{u + 1} (α := R) 1 1
⊢ HPow.hPow (α := R) (-1) (n + 1) = 1

Tactic:
rw [pow_succ, h, neg_one_mul, neg_neg]

Premises used: pow_succ, neg_one_mul, neg_neg
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
n : ℕ
h : HPow.hPow (α := R) (-1) n = 1
rw : HPow.hPow (α := R) (-1) n * -1 = -1
rw₁ : HMul.hMul (α := R) 1 (-1) = -1
rw₂ rw₃ : Eq.{u + 1} (α := R) (-1) (-1)
⊢ HPow.hPow (α := R) (-1) (n + 1) = -1

Tactic:
rw [pow_succ, h, one_mul]

Premises used: pow_succ, one_mul
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
a : R
n : ℕ
⊢ (-a) ^ n = HPow.hPow (α := R) (-1) n * a ^ n

Tactic:
neg_one_mul a ▸ (Commute.neg_one_left a).mul_pow n

Premises used: neg_one_mul, Eq.rec, Commute.mul_pow, Commute.neg_one_left
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
a : R
n : ℕ
⊢ (-a) ^ n = a ^ n * HPow.hPow (α := R) (-1) n

Tactic:
mul_neg_one a ▸ (Commute.neg_one_right a).mul_pow n

Premises used: Eq.rec, Commute.mul_pow, Commute.neg_one_right, mul_neg_one
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
a : R
⊢ HPow.hPow (β := ℕ) (-a) 2 = HPow.hPow (β := ℕ) a 2

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Monoid R
inst_1 : HasDistribNeg R
⊢ HPow.hPow (α := R) (β := ℕ) (-1) 2 = 1

Tactic:
simp [neg_sq, one_pow]

Premises used: one_pow, neg_sq
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
inl : ∀ (h : HPow.hPow (α := R) (-1) n = 1), HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0
inr : ∀ (h : HPow.hPow (α := R) (-1) n = -1), HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0
⊢ HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0

Tactic:
rcases neg_one_pow_eq_or R n with h | h

Premises used: neg_one_pow_eq_or
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
h : HPow.hPow (α := R) (-1) n = 1
⊢ HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
h : HPow.hPow (α := R) (-1) n = -1
⊢ HPow.hPow (α := R) (-1) n * a = 0 ↔ a = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
inl : ∀ (h : HPow.hPow (α := R) (-1) n = 1), a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0
inr : ∀ (h : HPow.hPow (α := R) (-1) n = -1), a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0
⊢ a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0

Tactic:
obtain h | h := neg_one_pow_eq_or R n

Premises used: neg_one_pow_eq_or
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
h : HPow.hPow (α := R) (-1) n = 1
⊢ a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
n : ℕ
h : HPow.hPow (α := R) (-1) n = -1
⊢ a * HPow.hPow (α := R) (-1) n = 0 ↔ a = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
n : ℕ
rw :
  HPow.hPow (α := R) (-1) (n % 2) * HPow.hPow (α := R) (β := ℕ) (-1) 2 ^ (n / 2) =
    HPow.hPow (α := R) (-1) ((n % 2 + 2 * (n / 2)) % 2)
⊢ HPow.hPow (α := R) (-1) n = HPow.hPow (α := R) (-1) (n % 2)

Tactic:
rw [← Nat.mod_add_div n 2, pow_add, pow_mul]

Premises used: pow_add, pow_mul, Nat.mod_add_div, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ HPow.hPow (α := R) (-1) (n % 2) * HPow.hPow (α := R) (β := ℕ) (-1) 2 ^ (n / 2) =
    HPow.hPow (α := R) (-1) ((n % 2 + 2 * (n / 2)) % 2)

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
inst_1 : NoZeroDivisors R
rw : HPow.hPow (β := ℕ) a 2 = 1 ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (α := R) (β := ℕ) 1 2
rw₁ rw₂ : HPow.hPow (β := ℕ) a 2 = 1 ↔ HPow.hPow (β := ℕ) a 2 = 1
⊢ HPow.hPow (β := ℕ) a 2 = 1 ↔ a = 1 ∨ a = -1

Tactic:
rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]

Premises used: one_pow, Commute.sq_eq_sq_iff_eq_or_eq_neg, Commute.one_right
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a : R
inst_1 : NoZeroDivisors R
⊢ HPow.hPow (β := ℕ) a 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1

Tactic:
sq_eq_one_iff.not.trans not_or

Premises used: sq_eq_one_iff, Iff.not, not_or, Iff.trans
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocCommRing R
a b : R
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
(Commute.all a b).mul_self_sub_mul_self_eq

Premises used: Commute.mul_self_sub_mul_self_eq, Commute.all
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonAssocRing R
a : R
rw : a * a - 1 = a * a - HMul.hMul (α := R) 1 1
rw₁ rw₂ : a * a - 1 = a * a - 1
⊢ a * a - 1 = (a + 1) * (a - 1)

Tactic:
rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]

Premises used: Commute.mul_self_sub_mul_self_eq, mul_one, Commute.one_right
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocCommRing R
inst_1 : NoZeroDivisors R
a b : R
⊢ a * a = b * b ↔ a = b ∨ a = -b

Tactic:
(Commute.all a b).mul_self_eq_mul_self_iff

Premises used: Commute.mul_self_eq_mul_self_iff, Commute.all
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
a : R
rw : a * a = 1 ↔ a * a = HMul.hMul (α := R) 1 1
rw₁ rw₂ : a * a = 1 ↔ a * a = 1
⊢ a * a = 1 ↔ a = 1 ∨ a = -1

Tactic:
rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]

Premises used: Commute.mul_self_eq_mul_self_iff, mul_one, Commute.one_right
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
a b : R
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)

Tactic:
(Commute.all a b).sq_sub_sq

Premises used: Commute.sq_sub_sq, Commute.all
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₁ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) (-b) 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₂ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₃ :
  HPow.hPow (β := ℕ) a 2 + -(2 * a * b) + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₄ rw₅ :
  HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2

Tactic:
rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]

Premises used: add_sq, sub_eq_add_neg, neg_sq, mul_neg
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -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₂ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * -b =
    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 [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, neg_sq, add_sq', mul_neg
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b = HPow.hPow (β := ℕ) (b - a) 2
rw₁ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * b * a = HPow.hPow (β := ℕ) (b - a) 2
rw₂ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 - 2 * b * a = HPow.hPow (β := ℕ) (b - a) 2
rw₃ rw₄ :
  HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 - 2 * b * a =
    HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 - 2 * b * a
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) (b - a) 2

Tactic:
rw [sub_sq', mul_right_comm, add_comm, sub_sq']

Premises used: add_comm, mul_right_comm, sub_sq'
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b

Tactic:
(Commute.all a b).sq_eq_sq_iff_eq_or_eq_neg

Premises used: Commute.sq_eq_sq_iff_eq_or_eq_neg, Commute.all
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 → a = b ∨ a = -b

Tactic:
sq_eq_sq_iff_eq_or_eq_neg.1

Premises used: Iff.mp, sq_eq_sq_iff_eq_or_eq_neg
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : Rˣ
simp_rw :
  (↑(HPow.hPow (β := ℕ) a 2) : R) = (↑(HPow.hPow (β := ℕ) b 2) : R) ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
simp_rw₁ : HPow.hPow (β := ℕ) (↑a : R) 2 = HPow.hPow (β := ℕ) (↑b : R) 2 ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
simp_rw₂ : (↑a : R) = (↑b : R) ∨ (↑a : R) = -(↑b : R) ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b

Tactic:
simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]

Premises used: Units.ext_iff, Units.val_neg, sq_eq_sq_iff_eq_or_eq_neg, Units.val_pow_eq_pow_val
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : Rˣ
h : HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2
⊢ a = b ∨ a = -b

Tactic:
Units.sq_eq_sq_iff_eq_or_eq_neg.1 h

Premises used: Units.sq_eq_sq_iff_eq_or_eq_neg, Iff.mp
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
rw : u * u = 1 ↔ u = 1 ∨ u = -1
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1

Tactic:
rw [inv_eq_iff_mul_eq_one]

Premises used: inv_eq_iff_mul_eq_one
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
simp : (↑(u * u) : R) = (↑1 : R) ↔ (↑u : R) = (↑1 : R) ∨ (↑u : R) = (↑(-1) : R)
⊢ u * u = 1 ↔ u = 1 ∨ u = -1

Tactic:
simp only [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
push_cast : (↑u : R) * (↑u : R) = 1 ↔ (↑u : R) = 1 ∨ (↑u : R) = -1
⊢ (↑(u * u) : R) = (↑1 : R) ↔ (↑u : R) = (↑1 : R) ∨ (↑u : R) = (↑(-1) : R)

Tactic:
push_cast
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
⊢ (↑u : R) * (↑u : R) = 1 ↔ (↑u : R) = 1 ∨ (↑u : R) = -1

Tactic:
mul_self_eq_one_iff

Premises used: mul_self_eq_one_iff
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
⊢ (↑u : R) * (↑u : R) = 1 ↔ (↑u : R) = 1 ∨ (↑u : R) = -1

Tactic:
exact mul_self_eq_one_iff

Premises used: mul_self_eq_one_iff
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
x y : R
⊢ ⁅x, y⁆ = x * y - y * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
x y : R
⊢ Commute x y ↔ ⁅x, y⁆ = 0

Tactic:
sub_eq_zero.symm

Premises used: sub_eq_zero, SemiconjBy, Commute, Iff.symm
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
x y : R
h : Commute x y
⊢ ⁅x, y⁆ = 0

Tactic:
sub_eq_zero_of_eq h

Premises used: sub_eq_zero_of_eq
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x : R₁
⊢ Eq.{u_3 + 1} (α := R₃) ((σ₂₃ : (a : R₂) → R₃) ((σ₁₂ : (a : R₁) → R₂) x : R₂) : R₃) ((σ₁₃ : (a : R₁) → R₃) x : R₃)

Tactic:
RingHom.congr_fun comp_eq x

Premises used: RingHom.congr_fun, RingHomCompTriple.comp_eq
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_2 : RingHomInvPair σ σ'
x : R₁
rw : (RingHom.id R₁ : (a : R₁) → R₁) x = x
⊢ (σ' : (a : R₂) → R₁) ((σ : (a : R₁) → R₂) x : R₂) = x

Tactic:
rw [← RingHom.comp_apply, comp_eq]

Premises used: RingHomInvPair.comp_eq, RingHom.comp_apply
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_2 : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁ : (a : R₁) → R₁) x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_2 : RingHomInvPair σ σ'
x : R₂
rw : (RingHom.id R₂ : (a : R₂) → R₂) x = x
⊢ (σ : (a : R₁) → R₂) ((σ' : (a : R₂) → R₁) x : R₁) = x

Tactic:
rw [← RingHom.comp_apply, comp_eq₂]

Premises used: RingHomInvPair.comp_eq₂, RingHom.comp_apply
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_2 : RingHomInvPair σ σ'
x : R₂
⊢ (RingHom.id R₂ : (a : R₂) → R₂) x = x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_3 : RingHomInvPair σ σ'
⊢ RingHomInvPair (RingHom.id R₁) (RingHom.id R₁)

Tactic:
⟨rfl, rfl⟩

Premises used: RingHomInvPair.mk, rfl
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_3 : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst_4 : RingHomInvPair σ₁₂ σ₂₁
⊢ σ₂₁.comp σ₁₂ = RingHom.id R₁

Tactic:
simp only [comp_eq]

Premises used: RingHomInvPair.comp_eq
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_3 : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst_4 : RingHomInvPair σ₁₂ σ₂₁
⊢ σ₁₂.comp σ₂₁ = RingHom.id R₂

Tactic:
simp only [comp_eq₂]

Premises used: RingHomInvPair.comp_eq₂
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
e : R₁ ≃+* R₂
⊢ RingHomInvPair (↑e : R₁ →+* R₂) (↑e.symm : R₂ →+* R₁)

Tactic:
⟨e.symm_toRingHom_comp_toRingHom, e.symm.symm_toRingHom_comp_toRingHom⟩

Premises used: RingEquiv.symm_toRingHom_comp_toRingHom, RingEquiv.symm, RingHomInvPair.mk
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
e : R₁ ≃+* R₂
⊢ RingHomInvPair (↑e.symm : R₂ →+* R₁) (↑e : R₁ →+* R₂)

Tactic:
of_ringEquiv e.symm

Premises used: RingHomInvPair.of_ringEquiv, Equiv.symm, RingEquiv.symm
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
⊢ RingHomInvPair σ₂₁ σ₁₂

Tactic:
⟨RingHomInvPair.comp_eq₂, RingHomInvPair.comp_eq⟩

Premises used: RingHomInvPair.comp_eq₂, RingHomInvPair.comp_eq, RingHomInvPair.mk
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ σ₁₂.comp (RingHom.id R₁) = σ₁₂

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ RingHom.comp (RingHom.id R₂) σ₁₂ = σ₁₂

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ : R₁ →+* R₂
t : RingHomSurjective σ
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R₁) (β := R₂) (⇑σ : (a : R₁) → R₂)

Tactic:
t.is_surjective

Premises used: RingHomSurjective.is_surjective
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
σ₁ : R₁ →+* R₂
σ₂ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁ σ₂
⊢ RingHomSurjective σ₁

Tactic:
⟨fun x => ⟨σ₂ x, RingHomInvPair.comp_apply_eq₂⟩⟩

Premises used: RingHomInvPair.comp_apply_eq₂, RingHomSurjective.mk, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ RingHomSurjective (RingHom.id R₁)

Tactic:
⟨is_surjective⟩

Premises used: RingHomSurjective.mk, RingHomSurjective.is_surjective
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : RingHomSurjective σ₁₂
inst_5 : RingHomSurjective σ₂₃
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := R₂) (⇑σ₂₃ : (a : R₂) → R₃) (⇑σ₁₂ : (a : R₁) → R₂))

Tactic:
have := σ₂₃.surjective.comp σ₁₂.surjective
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : RingHomSurjective σ₁₂
inst_5 : RingHomSurjective σ₂₃
this :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := R₂) (⇑σ₂₃ : (a : R₂) → R₃) (⇑σ₁₂ : (a : R₁) → R₂))
rwa :
  ∀ (this : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑(σ₂₃.comp σ₁₂) : (a : R₁) → R₃)),
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)),
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)

Tactic:
rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this

Premises used: RingHomCompTriple.comp_eq, RingHom.coe_comp
-- Module: Mathlib.Algebra.Ring.CompTypeclasses
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ_1 : R₁ →+* R₂
σ' : R₂ →+* R₁
σ : R₁ ≃+* R₂
⊢ RingHomSurjective (↑σ : R₁ →+* R₂)

Tactic:
⟨σ.surjective⟩

Premises used: RingEquiv.surjective, RingHomSurjective.mk
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
R_1 : Type v
R : Type u_1
inst : Distrib R
⊢ LeftDistribClass R

Tactic:
⟨Distrib.left_distrib⟩

Premises used: Distrib.left_distrib, LeftDistribClass.mk
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
R_1 : Type v
R : Type u_1
inst : Distrib R
⊢ RightDistribClass R

Tactic:
⟨Distrib.right_distrib⟩

Premises used: RightDistribClass.mk, Distrib.right_distrib
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
R : Type v
inst : Mul R
inst_1 : Add R
inst_2 : LeftDistribClass R
a b c : R
⊢ a * (b + c) = a * b + a * c

Tactic:
LeftDistribClass.left_distrib a b c

Premises used: LeftDistribClass.left_distrib
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
R : Type v
inst : Mul R
inst_1 : Add R
inst_2 : RightDistribClass R
a b c : R
⊢ (a + b) * c = a * c + b * c

Tactic:
RightDistribClass.right_distrib a b c

Premises used: RightDistribClass.right_distrib
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
R : Type v
inst : Mul R
inst_1 : Add R
inst_2 : RightDistribClass R
a b c d : R
⊢ (a + b + c) * d = a * d + b * d + c * d

Tactic:
simp [right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : RightDistribClass α
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 [add_mul, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : LeftDistribClass α
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_add, mul_one]

Premises used: mul_add, mul_one
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : RightDistribClass α
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 [add_mul, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : LeftDistribClass α
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_add, mul_one]

Premises used: mul_add, mul_one
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocSemiring α
n : α
rw rw₁ : n + n = n + n
⊢ 1 * n + 1 * n = n + n

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocSemiring α
n : α
rw rw₁ : n + n = n + n
⊢ n * 1 + n * 1 = n + n

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
zero : 0 = (↑0 : α) * a
zero₁ : 0 = 0 * a
zero₂ zero₃ : Eq.{u + 1} (α := α) 0 0
⊢ HSMul.hSMul (α := ℕ) 0 a = (↑0 : α) * a

Tactic:
rw [zero_nsmul, Nat.cast_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, zero_nsmul, Nat.cast_zero
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = (↑n : α) * a
succ : n • a + a = (↑(n + 1) : α) * a
succ₁ : (↑n : α) * a + a = (↑(n + 1) : α) * a
succ₂ : (↑n : α) * a + a = HAdd.hAdd (α := α) (↑n : α) 1 * a
succ₃ : (↑n : α) * a + a = (↑n : α) * a + 1 * a
succ₄ succ₅ : (↑n : α) * a + a = (↑n : α) * a + a
⊢ (n + 1) • a = (↑(n + 1) : α) * a

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

Premises used: add_mul, Nat.cast_succ, one_mul, succ_nsmul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : NonAssocSemiring α
n : ℕ
a : α
zero : HSMul.hSMul (α := ℕ) 0 a = (↑0 : α) * a
succ : ∀ (n : ℕ) (ih : n • a = (↑n : α) * a), (n + 1) • a = (↑(n + 1) : α) * a
⊢ n • a = (↑n : α) * a

Tactic:
induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

Premises used: add_mul, Nat.cast_succ, MulZeroClass.zero_mul, zero_nsmul, Nat.cast_zero, one_mul, succ_nsmul
-- Module: Mathlib.Algebra.Ring.Defs
Goal:
α : Type u
inst : MulZeroClass α
P : Prop
inst_1 : Decidable P
a b : α
⊢ (if P then a else 0) * b = if P then a * b else 0

Tactic:
simp