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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
⊢ ∃ d, P.natDegree = P.eraseLead.natDegree + 1 + d ∧ d = P.natDegree - P.eraseLead.degree.succ

Tactic:
by
    use P.natDegree - P.eraseLead.natDegree - 1
    have := eraseLead_natDegree_le P
    lia

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝² : Field Fq
inst✝¹ : Fintype Fq
inst✝ : DecidableEq Fq
p : Fq[X]
⊢ cardPowDegree p = if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree

Tactic:
by
  simp [cardPowDegree]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).natDegree = m + n

Tactic:
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_mul]
    exact one_ne_zero

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).natDegree = m + n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
r : R
⊢ (C r).natDegree < 1

Tactic:
natDegree_C

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
r : R
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
⊢ (C r).natDegree < 1

Tactic:
natDegree_C

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: 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)
⊢ spanCoeffs(q) ^ (deg(r) + 1) * spanCoeffs(p) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
by gcongr; exacts [le_sup_left, deg_r_lt_deg_p]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
⊢ (if hq : q.Monic then (p.divModByMonicAux hq).2 else p).coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
split_ifs with H

Goal state after:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ (p.divModByMonicAux H).2.coeff i ∈ Mq ^ deg(p) * Mp

case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ p.coeff i ∈ Mq ^ deg(p) * Mp
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
⊢ (if hq : q.Monic then (p.divModByMonicAux hq).1 else 0).coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
split_ifs with H

Goal state after:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ (p.divModByMonicAux H).1.coeff i ∈ Mq ^ deg(p) * Mp

case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ coeff 0 i ∈ Mq ^ deg(p) * Mp
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) 1 = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)

Tactic:
Finsupp.update_eq_add_single (by simp),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ (MvPolynomial.monomial ((fun₀ | 0 => m) + fun₀ | 1 => n - m)) 1 = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ MvPolynomial.eval₂ f g (p.homogenize n) = eval₂ f (g 0) p

Tactic:
apply Polynomial.induction_with_natDegree_le
    (fun p ↦ MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0)) (N := n)

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0

case C_mul_pow
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (n_1 : ℕ) (r : R),
    r ≠ 0 → n_1 ≤ n → MvPolynomial.eval₂ f g ((C r * X ^ n_1).homogenize n) = eval₂ f (g 0) (C r * X ^ n_1)

case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
a b : α
hab : R a b
⊢ IsChain R (a :: destutter' R b l)

Tactic:
by
  simpa [destutter'_cons, hab] using isChain_destutter' R (b :: l) a

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, IsChain R (a :: l) → destutter' R a l = a :: l
a : α
h : IsChain R (a :: b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
obtain ⟨h, hc⟩ := isChain_cons_cons.mp h
    rw [l.destutter'_cons_pos h, hb hc]

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ 0 ≤ p.natDegree - q ∧
    ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) 0

Tactic:
use Nat.zero_le _

Goal state after:
case right
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr
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 - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
      exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
⊢ 0 ≤ 0 - q ∧
    ∀ (r : A) {p' : A[X]},
      map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p' →
        (aeval r) (sumIDeriv 0) = (q - 1)! • eval r p' + q ! • (aeval r) 0

Tactic:
use Nat.zero_le _

Goal state after:
case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
⊢ ∀ (r : A) {p' : A[X]},
    map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p' →
      (aeval r) (sumIDeriv 0) = (q - 1)! • eval r p' + q ! • (aeval r) 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)

Tactic:
refine ⟨?_, by gcongr⟩

Goal state after:
case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n < n + (n - m + k)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
mul_comm q,

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp.re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.re = re 0

Tactic:
simp [h _ this.left, h _ this.right]

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

Goal state before:
pp: case mp.im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * z = 0
this : w.re * norm z = 0 ∧ w.im * norm z = 0
⊢ w.im = im 0

Tactic:
simp [h _ this.left, h _ this.right]

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

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ norm z ∈ R⁰ → z ∈ (QuadraticAlgebra R a b)⁰

Tactic:
simp only [mem_nonZeroDivisors_iff_right]
    intro h w hw
    have : norm z • w = 0 := by
      rw [← C_mul_eq_smul, C_eq_algebraMap, algebraMap_norm_eq_mul_star, mul_comm, ← mul_assoc, hw,
        zero_mul]
    simp only [QuadraticAlgebra.ext_iff, re_smul, smul_eq_mul, mul_comm, re_zero, im_smul,
      im_zero] at this
    ext <;> simp [h _ this.left, h _ this.right]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
⊢ ∀ {x y z : Conj G}, (MulAut.conj x) ((MulAut.conj y) z) = (MulAut.conj ((MulAut.conj x) y)) ((MulAut.conj x) z)

Tactic:
intro x y z
    dsimp only [MulAut.conj_apply]
    simp [mul_assoc]

Goal state after:
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₃
⊢ q.i * (q.j * (q.i * q.j)) = -((c₁ * c₃) • 1)

Tactic:
← mul_assoc q.j _ _,

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₃
⊢ q.i * (q.j * q.i * q.j) = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F q.i * F q.i = c₁ • 1 + c₂ • F q.i

Tactic:
by rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_3
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
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a : B
⊢ ∀ (y : B),
    a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      y ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
        (mkRingHom r) a = 0 → (mkRingHom r) y = 0 → (mkRingHom r) (a + y) = 0

Tactic:
b

Goal state after:
case refine_3
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
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
a b : B
⊢ a ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
    b ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a} →
      (mkRingHom r) a = 0 → (mkRingHom r) b = 0 → (mkRingHom r) (a + b) = 0
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
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
⊢ ∀ (x y : RingQuot s), Quot.lift ⇑f ⋯ (x * y).toQuot = Quot.lift ⇑f ⋯ x.toQuot * Quot.lift ⇑f ⋯ y.toQuot

Tactic:
rintro ⟨⟨x⟩⟩ ⟨⟨y⟩⟩
    simp only [mul_quot, map_mul _ x y]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
by
  ext; simp [coeff, update]; rfl

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
f : SkewMonoidAlgebra k G
a : G
⊢ a ∈ f.support ↔ f.coeff a ≠ 0

Tactic:
rcases f with ⟨⟩

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a : G
coeff✝ : G →₀ k
⊢ a ∈ { coeff := coeff✝ }.support ↔ { coeff := coeff✝ }.coeff a ≠ 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : DecidableEq G
f : SkewMonoidAlgebra k G
a : G
b : G → k → N
⊢ (f.sum fun x v ↦ if x = a then b x v else 0) = if a ∈ f.support then b a (f.coeff a) else 0

Tactic:
simp only [sum_def', f.coeff.support.sum_ite_eq', support]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddGroup k
a : G
b : k
⊢ single a (-b) = -single a b

Tactic:
by
  simp [← ofCoeff_single]

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

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ ∀ (b : α₂) (m₁ m₂ : β),
    (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) ((m₁ + m₂) * b • b₂)) =
      (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (m₁ * b • b₂)) +
        ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (b * a₂) (m₂ * b • b₂)

Tactic:
by simp [add_mul, single_add, sum_add]

Goal state after:
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)
⊢ spectrum R (star f).ofConv = star (spectrum R f.ofConv)

Tactic:
ext x
  simp_rw [Set.mem_star, spectrum.mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one]
  rw [← isUnit_intrinsicStar_iff]
  simp [one_eq_id]

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

Goal state before:
pp: case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ x ∈ X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)

Tactic:
X.toRingedSpace.mem_basicOpen _ _ hxU

Goal state after:
case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case naturality
J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
f : X ⟶ Y
⊢ (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (pushforwardEq ⋯ (F.obj (unop Y)).presheaf).hom.app
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U)) ≫
        (F.obj (unop Y)).presheaf.map (eqToIso ⋯).hom =
    (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f

Tactic:
erw [← (F.obj (unop Y)).presheaf.map_comp, (F.map f.unop).c.naturality_assoc,
      ← (F.obj (unop Y)).presheaf.map_comp]

Goal state after:
case naturality
J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
f : X ⟶ Y
⊢ (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map
        ((NatIso.op
                  (Opens.mapIso ((F ⋙ forget C).map f.unop ≫ colimit.ι (F ⋙ forget C) (unop X))
                      (colimit.ι (F ⋙ forget C) (unop Y)) ⋯).symm).hom.app
            ((Opens.map
                    (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
              (op U)) ≫
          (eqToIso ⋯).hom) =
    (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map ((Opens.map (F.map f.unop).base).op.map (eqToIso ⋯).hom ≫ eqToHom ⋯)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
t : (fun X ↦ X) (T x)
⊢ ∃ a, (ConcreteCategory.hom (stalkToFiber P x)) a = t

Tactic:
rcases w t with ⟨U, f, h, rfl⟩
  fconstructor
  · exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩
  · exact stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ sheafedSpaceMap (f ≫ g).unop = sheafedSpaceMap f.unop ≫ sheafedSpaceMap g.unop

Tactic:
simp [Spec.sheafedSpaceMap_comp]

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

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
⊢ ∀ {Y_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ} (f_1 : U ⟶ Y_1),
    (Y.restrict ⋯).presheaf.map f_1 ≫
        (asIso (f.c.app (op ((opensFunctor f).obj (unop Y_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
      (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
        ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1

Tactic:
V

Goal state after:
case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
⊢ ∀ (f_1 : U ⟶ V),
    (Y.restrict ⋯).presheaf.map f_1 ≫
        (asIso (f.c.app (op ((opensFunctor f).obj (unop V)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
      (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
        ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ X.zeroLocus ↑(Ideal.span s) = X.zeroLocus s

Tactic:
ext x
  simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]
  refine ⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩
  · simp only [Scheme.basicOpen_zero]; exact not_false
  · exact fun a b _ _ ha hb H ↦ (X.basicOpen_add_le a b H).elim ha hb
  · simp +contextual

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑I ⊆ X.zeroLocus ↑I.radical

Tactic:
simp only [Set.subset_def, mem_zeroLocus_iff, SetLike.mem_coe]

Goal state after:
X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
⊢ ∀ (x : ↥X), (∀ f ∈ I, x ∉ X.basicOpen f) → ∀ f ∈ I.radical, x ∉ X.basicOpen f