mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
⊢ ArchimedeanClass.mk (∑ i ∈ f.support, ↑(f i)) ≠ ArchimedeanClass.mk a

Tactic:
have hmem (x : FiniteArchimedeanClass M) : (f x).val ∈ u.stratum x :=
      Set.mem_of_mem_of_subset (f x).prop (by simp)

Goal state after:
case pos
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
⊢ ArchimedeanClass.mk (∑ i ∈ f.support, ↑(f i)) ≠ ArchimedeanClass.mk a
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁷ : PartialOrder Γ'
inst✝⁶ : AddCommMonoid V
Γ : Type u_6
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : PartialOrder Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ ((of R).symm ((single 0) r • x)).coeff a = r • ((of R).symm x).coeff a

Tactic:
by
  nth_rw 1 [← zero_vadd Γ a]
  exact coeff_single_smul_vadd

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
s : Multiset β
hs : s ≠ 0
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Tactic:
induction s using Multiset.induction_on with
  | empty => contradiction
  | cons a s h =>
    simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]
    by_cases h1 : s = 0
    · simp [h1]
    · obtain ⟨w, h2, h3⟩ := h h1
      rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
      · exact .inl h4
      · exact .inr ⟨w, h2, le_trans h4 h3⟩

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Tactic:
rw [← smul_eq_mul]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ x.orderTop + y.orderTop ≤ (x • y).orderTop
Module: Mathlib.Order.Quotient

Goal state before:
pp: case refine_2
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂

Tactic:
· exact .trans (.single <| .inr hx) <| .trans h (.single <| .inr (symm hy))

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h
α : Type u_1
s : Setoid α
inst✝ : LE α
z : Quotient s
x y : α
h₂ : ⟦y⟧ ≤ z
h₁ : ⟦x⟧ ≤ ⟦y⟧
⊢ ⟦x⟧ ≤ z

Tactic:
induction z using Quotient.inductionOn with

Goal state after:
case h.h.h
α : Type u_1
s : Setoid α
inst✝ : LE α
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
z : α
h₂ : ⟦y⟧ ≤ ⟦z⟧
⊢ ⟦x⟧ ≤ ⟦z⟧
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : ⟦y⟧ = ⟦z⟧
⊢ z < x → ⟦x⟧ = ⟦z⟧

Tactic:
exact fun h ↦ ((H _).out h₂.symm rfl ⟨h.le, h₁⟩).trans h₂

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : ¬↑b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
by_cases h : (a : K) = 0

Goal state after:
case pos
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ↑a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

case neg
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ∃ a_1, ↑↑a_1 * 1 = ↑↑a

Tactic:
use a

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ↑↑a * 1 = ↑↑a
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → A.unitGroup ≤ B.unitGroup

Tactic:
rintro h x (hx : A.valuation x = 1)

Goal state after:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : A.valuation ↑x = 1
⊢ x ∈ B.unitGroup
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ t * ↑(upperClosure s) = ↑(upperClosure (t * s))

Tactic:
exact mul_upperClosure _ _

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]
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:
gcongr; exacts [le_sup_left, deg_r_lt_deg_p]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : n ≤ p.natDegree + p.natTrailingDegree
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : ¬n ≤ p.natDegree + p.natTrailingDegree
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)

Tactic:
by_cases h3 : p.natTrailingDegree ≤ n

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : p.natTrailingDegree ≤ n
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : ¬p.natTrailingDegree ≤ n
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
⊢ Irreducible f

Tactic:
constructor
  · exact h1
  · intro g h fgh
    let k := g * h.mirror
    have key : f * f.mirror = k * k.mirror := by
      rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h,
        mul_comm g.mirror, mul_assoc, ← mul_assoc]
    have g_dvd_f : g ∣ f := by
      rw [fgh]
      exact dvd_mul_right g h
    have h_dvd_f : h ∣ f := by
      rw [fgh]
      exact dvd_mul_left h g
    have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
    have h_dvd_k_rev : h ∣ k.mirror := by
      rw [mirror_mul_of_domain, mirror_mirror]
      exact dvd_mul_left h g.mirror
    have hk := h2 k key
    rcases hk with (hk | hk | hk | hk)
    · exact Or.inr (h3 h_dvd_f (by rwa [← hk]))
    · exact Or.inr (h3 h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))
    · exact Or.inl (h3 g_dvd_f (by rwa [← hk]))
    · exact Or.inl (h3 g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p ∣ q
⊢ p.homogenize p.natDegree ∣ q.homogenize q.natDegree

Tactic:
by
  rcases h with ⟨r, rfl⟩
  obtain rfl | rfl | ⟨hp₀, hr₀⟩ : p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0 := by tauto
  · simp
  · simp
  · rw [natDegree_mul hp₀ hr₀, homogenize_mul _ _ le_rfl le_rfl]
    apply dvd_mul_right

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p =
    p + derivative (∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p)

Tactic:
derivative_sum,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p =
    p + ∑ b ∈ range (p.natDegree + 1), derivative ((⇑derivative)^[b] p)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (∏ i ∈ Finset.cons j s hj, g i)

Tactic:
rw [Finset.prod_cons, IsCoprime.mul_right_iff]

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ x = 0

Tactic:
← algebraMap_inj,

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ (algebraMap R (QuadraticAlgebra R ?m.26 ?m.27)) x = (algebraMap R (QuadraticAlgebra R ?m.26 ?m.27)) 0

R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ R

R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ R
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
⊢ Equivalence (PreEnvelGroupRel R)

Tactic:
by
    constructor
    · apply PreEnvelGroupRel.refl
    · apply PreEnvelGroupRel.symm
    · apply PreEnvelGroupRel.trans

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.k * q.k = -((c₁ * c₃) • 1)

Tactic:
by
  rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_sub, ←
    mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, sub_mul, smul_mul_assoc, mul_smul_comm,
    smul_mul_assoc, mul_assoc, j_mul_j, add_mul, smul_mul_assoc, j_mul_j, smul_smul,
    smul_mul_assoc, mul_assoc, j_mul_j]
  linear_combination (norm := module)

Goal state after:
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
a✝ : α
⊢ (a + b) * ↑a✝ = a * ↑a✝ + b * ↑a✝

Tactic:
cases a <;> cases b <;> try rfl

Goal state after:
case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²
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✝ : NonUnitalNonAssocRing α
f : CentroidHom α
a b : α
⊢ (↑(-↑f)).toFun (a * b) = a * (↑(-↑f)).toFun b

Tactic:
by
        simp [map_mul_left]

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:
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.RingQuot

Goal state before:
pp: case mp.rel.of
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝¹ y✝¹ x✝ y✝ : R
h✝ : r x✝ y✝
⊢ RingConGen.Rel r x✝ y✝

Tactic:
| of =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr.of
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ : R
a✝ : r x✝ y✝
⊢ Relation.EqvGen (Rel r) x✝ y✝

Tactic:
| of =>

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
⊢ ∀ (a : RingQuot r), 1 * a = a

Tactic:
by
    rintro ⟨⟨⟩⟩
    simp only [mul_quot, ← one_quot, one_mul]

Goal state after:
Module: Mathlib.Algebra.RingQuot

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

Tactic:
simp only [mul_quot, add_quot, right_distrib]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
toQuot✝ : Quot (Rel s)
a : A
⊢ ∃ a_1, (fun x ↦ { toQuot := Quot.mk (Rel s) x }) a_1 = { toQuot := Quot.mk (Rel s) a }

Tactic:
use a

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
h : c ≠ 0
⊢ ((monomial 1) c).support = {1}

Tactic:
support_monomial 1 h

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
h : c ≠ 0
⊢ {1} = {1}
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) (a + -b) = (monomial n) a - (monomial n) b

Tactic:
monomial_add,

Goal state after:
R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) a + (monomial n) (-b) = (monomial n) a - (monomial n) b
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:

Tactic:
(f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 :=
      (Finset.sum_congr (by ext; simp [Finset.mem_filter, Finset.mem_product, hs, and_comm])
        fun _ _ ↦ rfl)
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = b * a

Tactic:
rw [mul_def, mul_def, add_comm]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = b * a

Tactic:
by rw [mul_def, mul_def, add_comm]

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' ↑∅)

pp: case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Tactic:
· simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x) z ⋯)) (g x) =
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x ⊓ V y) z ⋯))
      ((ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y))

Tactic:
germ_res_apply

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x) z ⋯)) (g x) =
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V y) z ⋯)) (g y)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x) z ⋯)) (g x) =
    (ConcreteCategory.hom ((sheaf X).presheaf.germ (V y) z ⋯)) (g y)

Tactic:
apply (h z ((iVU x).le hzVx)).mul_right_inj.mp

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ U z ⋯)) f * (ConcreteCategory.hom ((sheaf X).presheaf.germ (V x) z ⋯)) (g x) =
    (ConcreteCategory.hom (X.presheaf.germ U z ⋯)) f * (ConcreteCategory.hom ((sheaf X).presheaf.germ (V y) z ⋯)) (g y)