awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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)
rw₁ rw₂ : m • y = m • y
⊢ m • y = x * m • k

Tactic:
rw [mul_smul_comm, ← hk]

Premises used: mul_smul_comm
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
n : ℕ
h : x ∣ y
⊢ x ∣ n • y

Tactic:
dvd_smul_of_dvd n h

Premises used: dvd_smul_of_dvd
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
Goal:
R : Type u_1
inst : NonUnitalRing R
x y : R
z : ℤ
h : x ∣ y
⊢ x ∣ z • y

Tactic:
dvd_smul_of_dvd z h

Premises used: dvd_smul_of_dvd
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
rw : x ^ m ∣ ∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ p, p.choose m.1 • (x ^ m.1 * y ^ m.2)
⊢ x ^ m ∣ (x + y) ^ p

Tactic:
rw [h_comm.add_pow']

Premises used: Commute.add_pow'
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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)

Tactic:
Finset.dvd_sum fun ⟨i, j⟩ hij ↦ ?_

Premises used: Dvd.dvd, Nat.choose, HMul.hMul, Prod.fst, _private.0.Commute.pow_dvd_add_pow_of_pow_eq_zero_right.match_1, Finset.dvd_sum, HPow.hPow, HSMul.hSMul, Prod.snd
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
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)
⊢ x ^ m ∣ ∑ m ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ p, p.choose m.1 • (x ^ m.1 * y ^ m.2)

Tactic:
refine Finset.dvd_sum fun ⟨i, j⟩ hij ↦ ?_

Premises used: Finset.dvd_sum
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
⊢ i + j = p

Tactic:
simpa using hij
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
⊢ i + j = p

Tactic:
replace hij : i + j = p := by simpa using hij
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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 : x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
⊢ x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)

Tactic:
apply dvd_nsmul_of_dvd

Premises used: dvd_nsmul_of_dvd
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
h₁ : ∀ (hi : i + 1 ≤ m), x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
⊢ 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)

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
hi : m ≤ i
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
dvd_mul_of_dvd_left (pow_dvd_pow x hi) _

Premises used: dvd_mul_of_dvd_left, pow_dvd_pow
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
hi : m ≤ i
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
exact dvd_mul_of_dvd_left (pow_dvd_pow x hi) _

Premises used: dvd_mul_of_dvd_left, pow_dvd_pow
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
hi : i + 1 ≤ m
⊢ n ≤ j

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
hi : i + 1 ≤ m
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
simp [pow_eq_zero_of_le (by lia : n ≤ j) hy]

Premises used: pow_eq_zero_of_le
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (x + y) ^ p

Tactic:
add_comm x y ▸ h_comm.symm.pow_dvd_add_pow_of_pow_eq_zero_right hp hx

Premises used: Eq.rec, add_comm, Commute.symm, Eq.symm, Commute.pow_dvd_add_pow_of_pow_eq_zero_right
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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 ^ m ∣ (y - x + x) ^ p
⊢ x ^ m ∣ y ^ p

Tactic:
rw [← sub_add_cancel y x]

Premises used: sub_add_cancel
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
apply : (y - x) ^ n = 0
⊢ x ^ m ∣ (y - x + x) ^ p

Tactic:
apply (h_comm.symm.sub_left rfl).pow_dvd_add_pow_of_pow_eq_zero_left hp _

Premises used: Commute.pow_dvd_add_pow_of_pow_eq_zero_left, Commute.symm, rfl, Commute.sub_left
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (y - x) ^ n = 0

Tactic:
rw [← neg_sub x y, neg_pow, h, mul_zero]

Premises used: neg_sub, MulZeroClass.mul_zero, neg_pow
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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 ^ m ∣ (-y) ^ p * HPow.hPow (α := R) (-1) p
⊢ x ^ m ∣ y ^ p

Tactic:
rw [← neg_neg y, neg_pow']

Premises used: neg_neg, neg_pow'
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
h₁ : x ^ m ∣ (-y) ^ p
⊢ x ^ m ∣ (-y) ^ p * HPow.hPow (α := R) (-1) p

Tactic:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
h₁ : (x - -y) ^ n = 0
⊢ x ^ m ∣ (-y) ^ p

Tactic:
apply h_comm.neg_right.pow_dvd_pow_of_sub_pow_eq_zero hp

Premises used: Commute.pow_dvd_pow_of_sub_pow_eq_zero, Commute.neg_right
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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 - -y) ^ n = 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
⊢ (x - (x - y)) ^ n = 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
rw : y ^ m ∣ (y - x) ^ p * HPow.hPow (α := R) (-1) p
⊢ y ^ m ∣ (x - y) ^ p

Tactic:
rw [← neg_sub y x, neg_pow']

Premises used: neg_sub, neg_pow'
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
h : y ^ m ∣ (y - x) ^ p
⊢ y ^ m ∣ (y - x) ^ p * HPow.hPow (α := R) (-1) p

Tactic:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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

Tactic:
h_comm.symm.pow_dvd_sub_pow_of_pow_eq_zero_right hp hx

Premises used: Commute.symm, Commute.pow_dvd_sub_pow_of_pow_eq_zero_right
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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

Tactic:
exact h_comm.symm.pow_dvd_sub_pow_of_pow_eq_zero_right hp hx

Premises used: Commute.symm, Commute.pow_dvd_sub_pow_of_pow_eq_zero_right
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
⊢ (x + y - y) ^ n = 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
Goal:
R : Type u_1
x y : R
n m p : ℕ
inst : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
⊢ (x + y) ^ m ∣ x ^ p

Tactic:
add_comm x y ▸ h_comm.symm.add_pow_dvd_pow_of_pow_eq_zero_right hp hy

Premises used: Eq.rec, add_comm, Commute.symm, Commute.add_pow_dvd_pow_of_pow_eq_zero_right, Eq.symm
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
obtain : ∀ (k1 : R) (hk1 : a * x + b * y = p * k1), p ∣ (a * d - b * c) * x
⊢ p ∣ (a * d - b * c) * x

Tactic:
obtain ⟨k1, hk1⟩ := h1
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
obtain : ∀ (k2 : R) (hk2 : c * x + d * y = p * k2), p ∣ (a * d - b * c) * x
⊢ p ∣ (a * d - b * c) * x

Tactic:
obtain ⟨k2, hk2⟩ := h2
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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

Tactic:
⟨d * k1 - b * k2, ?_⟩

Premises used: HMul.hMul, HSub.hSub, Exists.intro
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
refine : (a * d - b * c) * x = p * (d * k1 - b * k2)
⊢ p ∣ (a * d - b * c) * x

Tactic:
refine ⟨d * k1 - b * k2, ?_⟩
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
⊢ (a * d - b * c) * x = p * (d * k1 - b * k2)

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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) * y

Tactic:
(mul_comm a _ ▸ mul_comm c _ ▸ dvd_mul_sub_mul_mul_left_of_dvd
    (add_comm (c * x) _ ▸ h2) (add_comm (a * x) _ ▸ h1))

Premises used: Eq.rec, dvd_mul_sub_mul_mul_left_of_dvd, mul_comm, Eq.symm
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
rw : p ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ ((a * d - b * c) * x) ((a * d - b * c) * y)
⊢ p ∣ (a * d - b * c) * @gcd _ CommSemiring.toCommMonoidWithZero _ x y

Tactic:
rw [← (gcd_mul_left' (a * d - b * c) x y).dvd_iff_dvd_right]

Premises used: HMul.hMul, HSub.hSub, gcd_mul_left', Associated.dvd_iff_dvd_right
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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 ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ ((a * d - b * c) * x) ((a * d - b * c) * y)

Tactic:
(dvd_gcd_iff _ _ _).2 ⟨dvd_mul_sub_mul_mul_left_of_dvd h1 h2,
    dvd_mul_sub_mul_mul_right_of_dvd h1 h2⟩

Premises used: Iff.mpr, dvd_mul_sub_mul_mul_left_of_dvd, And.intro, dvd_mul_sub_mul_mul_right_of_dvd, dvd_gcd_iff
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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 ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ ((a * d - b * c) * x) ((a * d - b * c) * y)

Tactic:
exact (dvd_gcd_iff _ _ _).2 ⟨dvd_mul_sub_mul_mul_left_of_dvd h1 h2,
    dvd_mul_sub_mul_mul_right_of_dvd h1 h2⟩

Premises used: Iff.mpr, dvd_mul_sub_mul_mul_left_of_dvd, And.intro, dvd_mul_sub_mul_mul_right_of_dvd, dvd_gcd_iff
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
inr : ∀ (h : |x| = -x), Associated |x| y ↔ Associated x y
⊢ Associated |x| y ↔ Associated x y

Tactic:
obtain h | h := abs_choice x

Premises used: abs_choice
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
x y : R
h : |x| = x
⊢ Associated |x| y ↔ Associated x y

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
x y : R
h : |x| = -x
⊢ Associated |x| y ↔ Associated x y

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Divisibility.Lemmas
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
rw₂ rw₃ : Associated x y ↔ Associated x y
⊢ Associated x |y| ↔ Associated x y

Tactic:
rw [Associated.comm, associated_abs_left_iff, Associated.comm]

Premises used: Associated.comm, associated_abs_left_iff
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : EquivLike F R S
inst_1 : Mul R
inst_2 : Add R
inst_3 : Mul S
inst_4 : Add S
h : RingEquivClass F R S
⊢ AddEquivClass F R S

Tactic:
{ h with }

Premises used: AddEquivClass.mk, RingEquivClass.map_add
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : EquivLike F R S
inst_1 : NonAssocSemiring R
inst_2 : NonAssocSemiring S
h : RingEquivClass F R S
⊢ RingHomClass F R S

Tactic:
{ h with
    map_zero := map_zero
    map_one := map_one }

Premises used: RingHomClass.mk
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : EquivLike F R S
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : NonUnitalNonAssocSemiring S
h : RingEquivClass F R S
⊢ NonUnitalRingHomClass F R S

Tactic:
{ h with
    map_zero := map_zero }

Premises used: NonUnitalRingHomClass.mk
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e f : R ≃+* S
h₁ : e.toFun = f.toFun
h₂ : e.invFun = f.invFun
mk :
  ∀ (toEquiv : R ≃ S) (map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
    (map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y)
    (h₁ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun = f.toFun)
    (h₂ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun = f.invFun),
    { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } = f
⊢ e = f

Tactic:
cases e
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
f : R ≃+* S
toEquiv : R ≃ S
map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y
h₁ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun = f.toFun
h₂ : { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun = f.invFun
mk :
  ∀ (toEquiv_1 : R ≃ S) (map_mul'_1 : ∀ (x y : R), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y)
    (map_add'_1 : ∀ (x y : R), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y)
    (h₁ :
      { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun =
        { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.toFun)
    (h₂ :
      { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun =
        { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.invFun),
    { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 }
⊢ { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } = f

Tactic:
cases f
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
toEquiv : R ≃ S
map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y
toEquiv_1 : R ≃ S
map_mul'_1 : ∀ (x y : R), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y
map_add'_1 : ∀ (x y : R), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y
h₁ :
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.toFun
h₂ :
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.invFun
mk : toEquiv = toEquiv_1
⊢ { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S } =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
toEquiv : R ≃ S
map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y
map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y
toEquiv_1 : R ≃ S
map_mul'_1 : ∀ (x y : R), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y
map_add'_1 : ∀ (x y : R), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y
h₁ :
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.toFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.toFun
h₂ :
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' : R ≃+* S }.invFun =
    { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* S }.invFun
⊢ toEquiv = toEquiv_1

Tactic:
apply Equiv.coe_fn_injective h₁

Premises used: Equiv.coe_fn_injective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f g : R ≃+* S
h : ∀ (x : R), Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) ((g : (a : R) → S) x : S)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
x x' : R
⊢ x = x' → Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S)

Tactic:
DFunLike.congr_arg f

Premises used: DFunLike.congr_arg
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f g : R ≃+* S
h : f = g
x : R
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) ((g : (a : R) → S) x : S)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃ S
h₃ : ∀ (x y : R), e.toFun (x * y) = e.toFun x * e.toFun y
h₄ : ∀ (x y : R), e.toFun (x + y) = e.toFun x + e.toFun y
⊢ Eq (α := (a : R) → S) (⇑{ toEquiv := e, map_mul' := h₃, map_add' := h₄ : R ≃+* S } : (a : R) → S) (⇑e : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
e' : S → R
h₁ : Function.LeftInverse e' (⇑e : (a : R) → S)
h₂ : Function.RightInverse e' (⇑e : (a : R) → S)
h₃ :
  ∀ (x y : R),
    { toFun := (⇑e : (a : R) → S), invFun := e', left_inv := h₁, right_inv := h₂ : R ≃ S }.toFun (x * y) =
      { toFun := (⇑e : (a : R) → S), invFun := e', left_inv := h₁, right_inv := h₂ : R ≃ S }.toFun x *
        { toFun := (⇑e : (a : R) → S), invFun := e', left_inv := h₁, right_inv := h₂ : R ≃ S }.toFun y
h₄ :
  ∀ (x y : R),
    { toFun := (⇑e : (a : R) → S), invFun := e', left_inv := h₁, right_inv := h₂ : R ≃ S }.toFun (x + y) =
      { toFun := (⇑e : (a : R) → S), invFun := e', left_inv := h₁, right_inv := h₂ : R ≃ S }.toFun x +
        { toFun := (⇑e : (a : R) → S), invFun := e', left_inv := h₁, right_inv := h₂ : R ≃ S }.toFun y
⊢ { toFun := (⇑e : (a : R) → S), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ :
      R ≃+* S } =
    e

Tactic:
ext fun _ => rfl

Premises used: RingEquiv.ext, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
⊢ f.toEquiv = (↑f : R ≃ S)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
⊢ Eq (α := (a : R) → S) (⇑(↑f : R ≃ S) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
⊢ f.toAddEquiv = (↑f : R ≃+ S)

Tactic:
rfl

Premises used: AddEquivClass.toAddEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
⊢ f.toMulEquiv = (↑f : R ≃* S)

Tactic:
rfl

Premises used: MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
⊢ Eq (α := (a : R) → S) (⇑(↑f : R ≃* S) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
⊢ Eq (α := (a : R) → S) (⇑(↑f : R ≃+ S) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
x y : R
⊢ (e : (a : R) → S) (x * y) = HMul.hMul (α := S) (β := S) ((e : (a : R) → S) x : S) ((e : (a : R) → S) y : S)

Tactic:
map_mul e x y

Premises used: map_mul
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
x y : R
⊢ (e : (a : R) → S) (x + y) = HAdd.hAdd (α := S) (β := S) ((e : (a : R) → S) x : S) ((e : (a : R) → S) y : S)

Tactic:
map_add e x y

Premises used: map_add
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑e : (a : R) → S)

Tactic:
EquivLike.bijective e

Premises used: EquivLike.bijective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑e : (a : R) → S)

Tactic:
EquivLike.injective e

Premises used: EquivLike.injective