mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ p.coeff m = q.coeff m

Tactic:
isMonicOfDegree_iff

Goal state after:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm : n ≤ m
a✝ : Nontrivial R
⊢ p.coeff m = q.coeff m
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case h₂
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ span R coeffs(p) ≤ spanCoeffs(q) * spanCoeffs(p)

Tactic:
Submodule.sup_mul,

Goal state after:
case h₂
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ span R coeffs(p) ≤ 1 * spanCoeffs(p) ⊔ span R coeffs(q) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
⊢ (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)

Tactic:
refine sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝ : ℕ
⊢ smul_pow x x✝ 0 = 0

case refine_2
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝² : ℕ
x✝¹ x✝ : R
⊢ smul_pow x x✝² (x✝¹ + x✝) = smul_pow x x✝² x✝¹ + smul_pow x x✝² x✝
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial
R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
n : ℕ
a : R
⊢ (r • a) • x ^ n = r • a • x ^ n

Tactic:
smul_assoc

Goal state after:
case monomial
R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
n : ℕ
a : R
⊢ r • a • x ^ n = r • a • x ^ n
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (p ^ n * p ^ 1).smeval x = p.smeval x ^ (n + 1)

Tactic:
smeval_mul,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (p ^ n).smeval x * (p ^ 1).smeval x = p.smeval x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).coeff k ≠ 0

Tactic:
trinomial_trailing_coeff' hkm hmn

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ u ≠ 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).coeff k = u

Tactic:
trinomial_trailing_coeff' hkm hmn

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ u = u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ ↑u = (trinomial k m n ↑u ↑v ↑w).coeff k

Tactic:
trinomial_trailing_coeff' hkm hmn

Goal state after:
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ ↑u = ↑u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3

Tactic:
trinomial_trailing_coeff' hkm hmn

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑u ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ ((X - C η) * (monomial d) c).nextCoeff = -(η * c)

Tactic:
convert coeff_mul_monomial (X - C η) d 0 c

Goal state after:
case e'_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ ((X - C η) * (monomial d) c).nextCoeff = ((X - C η) * (monomial d) c).coeff (0 + d)

case e'_3
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ -(η * c) = (X - C η).coeff 0 * c
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
hj : j ∈ s
dnb : (∏ k ∈ s.erase j, g k).degree ≠ ⊥
⊢ (r₁ j - r₂ j).degree < (g j).degree

Tactic:
exact (degree_sub_le (r₁ j) (r₂ j)).trans_lt (max_lt (hr₁.2 j hj) (hr₂.2 j hj))

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ ↑j.rev = gi i ^ (↑j + 1 + ↑j.rev) * (algebraMap R[X] K) (g i) ^ ↑j.rev

Tactic:
Fin.val_rev,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ (n i - (↑j + 1)) =
    gi i ^ (↑j + 1 + (n i - (↑j + 1))) * (algebraMap R[X] K) (g i) ^ (n i - (↑j + 1))
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Tactic:
simp only [re_mul, sub_eq_add_neg, add_smul, neg_smul, imI_mul, ← add_assoc, imJ_mul, imK_mul]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x.re * y.re) • 1 + (c₁ * x.imI * y.imI) • 1 + (c₃ * x.imJ * y.imJ) • 1 + (c₂ * c₃ * x.imJ * y.imK) • 1 +
                                    -((c₁ * c₃ * x.imK * y.imK) • 1) +
                                  (x.re * y.imI) • q.i +
                                (x.imI * y.re) • q.i +
                              (c₂ * x.imI * y.imI) • q.i +
                            -((c₃ * x.imJ * y.imK) • q.i) +
                          (c₃ * x.imK * y.imJ) • q.i +
                        (x.re * y.imJ) • q.j +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  (c₂ * x.imJ * y.imI) • q.j +
                -((c₁ * x.imK * y.imI) • q.j) +
              (x.re * y.imK) • q.k +
            (x.imI * y.imJ) • q.k +
          (c₂ * x.imI * y.imK) • q.k +
        -((x.imJ * y.imI) • q.k) +
      (x.imK * y.re) • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (↑j.rev + 1 + ↑j) * (algebraMap R[X] K) (g i) ^ ↑j * (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (g i) ^ ↑j

Tactic:
Fin.val_rev,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (n i - (↑j + 1) + 1 + ↑j) * (algebraMap R[X] K) (g i) ^ ↑j * (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (g i) ^ ↑j
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
by
  have : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
    ext : 1 <;> assumption
  -- Split into fields and prove they are equal using the above.
  cases inst₁; cases inst₂
  congr

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime : IsCoprime g₁ g₂
⊢ ∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Tactic:
let g : Bool → R[X] := Bool.rec g₂ g₁
  have hg (i : Bool) (_ : i ∈ Finset.univ) : (g i).Monic := Bool.rec hg₂ hg₁ i
  have hcoprime : Set.Pairwise (Finset.univ : Finset Bool) fun i j => IsCoprime (g i) (g j) := by
    simp [g, Set.pairwise_insert, hcoprime, hcoprime.symm]
  obtain ⟨q, r, hr, hf⟩ := div_prod_eq_quo_add_sum_rem_div K f hg hcoprime
  refine ⟨q, r true, r false, hr true (Finset.mem_univ true), hr false (Finset.mem_univ false), ?_⟩
  simpa [g, add_assoc] using hf

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : 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) (y✝ * c) (y✝ * d)

Tactic:
induction hcd with

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x✝ c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x✝ * c) (x✝ * d)

Tactic:
induction hcd with

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ ∑ x ∈ f.coeff.support, (f.coeff x • (of k G) x) • v ∈ ↑W

Tactic:
smul_assoc

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ ∑ x ∈ f.coeff.support, f.coeff x • (of k G) x • v ∈ ↑W
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : 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) (y✝ + c) (y✝ + d)

Tactic:
induction hcd with

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x✝ c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x✝ + c) (x✝ + d)

Tactic:
induction hcd with

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (n : ℕ) (x : RingQuot r), (n + 1) • x = n • x + x

Tactic:
by
    rintro n ⟨⟨⟩⟩
    simp only [smul_quot, nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul,
               add_comm, add_quot]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝⁴ : AddMonoid k
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ k
inst✝¹ : SMulZeroClass S₂ k
inst✝ : IsScalarTower S₁ S₂ k
x✝² : S₁
x✝¹ : S₂
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ { coeff := (x✝² • x✝¹) • coeff✝ } = { coeff := x✝² • x✝¹ • coeff✝ }

Tactic:
smul_assoc

Goal state after:
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ x + z

Tactic:
· rwa [add_eq_right hx]

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ (∀ (x : E), star (f.ofConv (star x)) = f.ofConv x) ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

Tactic:
star_eq_iff_star_eq,

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ (∀ (x : E), star (f.ofConv x) = f.ofConv (star x)) ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x : E
⊢ star (toConv (mulRight R x)) = toConv (mulLeft R (star x))

Tactic:
star_eq_iff_star_eq,

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x : E
⊢ star (toConv (mulLeft R (star x))) = toConv (mulRight R x)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
α : R
x : V
⊢ star (f.ofConv (star x)) = α • x ↔ f.ofConv (star x) = star α • star x

Tactic:
star_eq_iff_star_eq,

Goal state after:
R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
α : R
x : V
⊢ star (α • x) = f.ofConv (star x) ↔ f.ofConv (star x) = star α • star x
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
h : P.pred f
x : ↥U
⊢ P.pred fun x ↦ f ((𝟙 U) x)

Tactic:
convert! h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      CommRingCat.ofHom
          (comap (CommRingCat.Hom.hom f) (unop (op ⊤)) ((TopologicalSpace.Opens.map (Spec.topMap f)).obj (unop (op ⊤)))
            ⋯) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial

Tactic:
erw [toOpen_comp_comap_assoc]

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      CommRingCat.ofHom
          (algebraMap ↑S
            ↑((structureSheaf ↑S).obj.obj
                (op
                  ((TopologicalSpace.Opens.comap
                      { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                    ⊤)))) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ (f ≫ inv f) ⁻¹ᵁ U = U

Tactic:
rw [IsIso.hom_inv_id]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ PreservesLimitsOfShape WalkingCospan (opensFunctor f)

Tactic:
dsimp [Scheme.Hom.opensFunctor]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : (fun X ↦ X) X), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))

Tactic:
refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨Y, g, ⟨i⟩, hx⟩ := h x
    use i
  · obtain ⟨i, hx⟩ := h x
    use Y i, f i, ⟨i⟩

Goal state after: