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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r ((X - C r) ^ 1) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) • (X - C r) ^ (q - (k - i) - 1) * (⇑derivative)^[i] p') =
    0

Tactic:
pow_one,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r (X - C r) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) • (X - C r) ^ (q - (k - i) - 1) * (⇑derivative)^[i] p') =
    0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k)
hy : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff m)
hz : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff n)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • ((X - C r) ^ 1 * (X - C r) ^ (q - (q - (x + 1)) - 1)) *
        (⇑derivative)^[x + 1] p') =
    0

Tactic:
pow_one,

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • ((X - C r) * (X - C r) ^ (q - (q - (x + 1)) - 1)) *
        (⇑derivative)^[x + 1] p') =
    0
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 + ((trinomial k m n ↑u ↑v ↑w).coeff m ^ 2 + ↑w ^ 2) = 3

Tactic:
trinomial_middle_coeff hkm hmn,

Goal state after:
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
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : q ≤ k
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
obtain ⟨p', p'_le, hp'⟩ := exists_iterate_derivative_eq_factorial_smul p k
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hk
  refine ⟨((q + k).descFactorial k : R[X]) * p', (natDegree_C_mul_le _ _).trans p'_le, fun r => ?_⟩
  simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ q - 1 ≤ p.natDegree

Tactic:
calc
      q - 1 ≤ q - 1 + p'.natDegree := le_self_add
      _ = (p.map <| algebraMap R A).natDegree := by
        rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
        · exact pow_ne_zero _ (X_sub_C_ne_zero r)
        · rintro rfl
          rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp
          exact p0 hp
      _ ≤ p.natDegree := natDegree_map_le

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

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : (0 ≤ x ∧ x < q) ∧ q ≤ x ∧ x < p.natDegree + 1
⊢ False

Tactic:
exact hx.1.2.not_ge hx.2.1

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
u : { u // u * u = a • 1 + b • u }
z w : QuadraticAlgebra R a b
⊢ (z.re • 1 + z.im • ↑u) * (w.re • 1 + w.im • ↑u) = (z * w).re • 1 + (z * w).im • ↑u

Tactic:
calc
          (z.re • (1 : A) + z.im • ↑u) * (w.re • 1 + w.im • ↑u) =
            (z.re * w.re) • (1 : A) + (z.re * w.im) • u +
              (z.im * w.re) • u + (z.im * w.im) • (u * u) := by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'
          _ = (z.re * w.re) • (1 : A) + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (u * u) := by
              congr 1
              simp only [add_assoc]
              rw [← add_smul]
          _ = (z.re * w.re) • 1 + (z.re * w.im + z.im * w.re) • u +
                (z.im * w.im) • (a • 1 + b • u) := by
              simp [u.prop]
          _ = (z.re * w.re + a * z.im * w.im) • 1 +
                (z.re * w.im + z.im * w.re + b * z.im * w.im) • u := by
              simp only [smul_add]
              module
            _ = (z * w).re • 1 + (z * w).im • u := by
              simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
by ext <;> simp [mul_add, add_mul] <;> abel

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
⊢ ∀ {x y z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
by
    intro x y z
    simp only [dihedralAct]
    ring_nf

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✝ : 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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    ((algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)) *
        ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
      (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  (algebraMap R[X] K) (q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₁ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) =
    (algebraMap R[X] K) (q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₂ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
(FaithfulSMul.algebraMap_injective R[X] K).eq_iff

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
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    ((algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)) *
        ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
      (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₁ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₂ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
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 : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ ^ 1 =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹ ^ 1
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)

Tactic:
pow_one,

Goal state after:
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 : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ x ∈ s, ((algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)
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
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ (algebraMap R[X] K) q₁ + ∑ x ∈ s, (algebraMap R[X] K) (r₁ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ 1 =
    (algebraMap R[X] K) q₂ + ∑ x ∈ s, (algebraMap R[X] K) (r₂ x) * ((algebraMap R[X] K) (g x))⁻¹ ^ 1

Tactic:
pow_one,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ (algebraMap R[X] K) q₁ + ∑ x ∈ s, (algebraMap R[X] K) (r₁ x) * ((algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q₂ + ∑ x ∈ s, (algebraMap R[X] K) (r₂ x) * ((algebraMap R[X] K) (g x))⁻¹
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inr.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s a : R
ne_a : a ≠ 0
hs✝ : IsSumSq 0
ih : 0 ≠ 0 → IsSumNonzeroSq 0
hs : a * a + 0 ≠ 0
⊢ IsSumNonzeroSq (a * a + 0)

pp: case sq_add.inr.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
· simpa using IsSumNonzeroSq.sq ne_a

Goal state after:
case sq_add.inr.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    simp only [ZeroMemClass.coe_zero, map_zero]
    exact rfl

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✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ ∀ {x : k} {y : G}, (Algebra.ofId k A) (y • x) * F y = F y * (Algebra.ofId k A) x

Tactic:
simp_rw [show ∀ (g : G) (r : k), g • r = r by
        exact fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)]

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ ∀ {x : k} {y : G}, (Algebra.ofId k A) x * F y = F y * (Algebra.ofId k A) x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
classical
  ext a
  simp [support_single_mul_eq_image f (IsLeftRegular.all x) hrx]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk.mk
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
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝¹ } + { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝ } + { toQuot := Quot.mk (Rel r) a✝¹ }

Tactic:
simp only [add_quot, add_comm]

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✝ → Prop
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (a : RingQuot r), -a + a = 0

Tactic:
by
    rintro ⟨⟨⟩⟩
    simp [neg_quot, add_quot, ← zero_quot]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a a' : G
b : k
h : b ≠ 0
⊢ single a b = single a' b ↔ a = a'

Tactic:
rw [← coeff_inj]
  exact Finsupp.single_left_inj h

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
by
  rw [mul_def, coeff_sum]; congr; ext
  rw [coeff_sum]; congr; ext
  exact coeff_single_apply

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

Goal state before:
pp: case refine_1
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 (End R E)ˣ
⊢ (star (toConv ↑f.ofConv)).ofConv * (star (toConv ↑f.ofConv⁻¹)).ofConv = 1

pp: case refine_2
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 (End R E)ˣ
⊢ (star (toConv ↑f.ofConv⁻¹)).ofConv * (star (toConv ↑f.ofConv)).ofConv = 1

Tactic:
all_goals
      rw [mul_eq_comp, ← toConv_injective.eq_iff, ← LinearMap.intrinsicStar_comp']
      simp [← mul_eq_comp, one_eq_id]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f)

Tactic:
by
  apply isUnit_of_isUnit_germ
  rintro x ⟨hxU, hx⟩
  convert! hx
  exact X.presheaf.germ_res_apply _ _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : ↑Γ(Y, V)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appLE f V U e)) s) = U ⊓ f ⁻¹ᵁ Y.basicOpen s

Tactic:
simp only [preimage_basicOpen, Hom.appLE, CommRingCat.comp_apply]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : ↑Γ(Y, V)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE e).op)) ((ConcreteCategory.hom (Hom.app f V)) s)) =
    U ⊓ X.basicOpen ((ConcreteCategory.hom (Hom.app f V)) s)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op { carrier := carrier✝, is_open' := is_open'✝ }))))

Tactic:
dsimp only [Functor.op, Opens.map]

Goal state after:
case op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op
      ((opensFunctor f).obj
        ((↑(TopCat.Hom.frameHom f.base)).toFunctor.obj { carrier := carrier✝, is_open' := is_open'✝ }))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ } ≤
    (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ }

Tactic:
rintro _ ⟨x, h₁, rfl⟩
                    exact ⟨_, h₁, CategoryTheory.congr_fun pullback.condition x⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings Y

Tactic:
rw [Precoverage.mem_comap_iff, Presieve.map_ofArrows,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf ⊢
    intro x
    obtain ⟨i, hi⟩ := hf (F.map g x)
    have : HasPullback g (f i) := (h i).hasPullback
    use i
    have : F.map (p₁ i) = F.map ((h i).isoPullback.hom) ≫ pullbackComparison F g (f i) ≫
        pullback.fst _ _ := by simp [← Functor.map_comp]
    rwa [this, types_comp, types_comp, Function.comp_assoc, Set.range_comp,
      Function.Surjective.range_eq <| (H _ _).comp (surjective_of_epi _), Set.image_univ,
      Types.range_pullbackFst]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.IsStableUnderComposition
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u_1 v_1)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ P.precoverage.coverings (X i)
Z : C
p : Z ⟶ S
i : (i : ι) × σ i
⊢ P (g i.fst i.snd ≫ f i.fst)

Tactic:
exact P.comp_mem _ _ (hg _ ⟨i.2⟩) (hf ⟨i.1⟩)

Goal state after: