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

Goal state before:
pp: case refine_2
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
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ (seed.coeff (f.support.min' hsupport)) 0 < (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport))

Tactic:
suffices 0 < (f (f.support.min' hsupport)).val by
    apply (seed.strictMono_coeff (f.support.min' hsupport))
    simpa using! this

Goal state after:
case refine_2
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
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ 0 < ↑(f (f.support.min' hsupport))
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2.inr
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
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) =
    ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d

Tactic:
· rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc]
    have hcd : c.val ≤ d.val := hdc
    simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
    convert! LinearMap.map_zero _
    simp

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: 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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
hxy : x - ↑y ∈ closedBall K xy
⊢ f.eval x ≠ ↑↑f y

Tactic:
rw [← seed.ball_sup_stratum_eq xy, Submodule.mem_sup] at hxy

Goal state after:
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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
hxy : ∃ y_1 ∈ ball K xy, ∃ z ∈ seed.stratum xy, y_1 + z = x - ↑y
⊢ f.eval x ≠ ↑↑f y
Module: Mathlib.Algebra.Order.UpperLower

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

Tactic:
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul,
    LowerSet.coe_iSup₂]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ⋃ a ∈ s, a • ↑(lowerClosure t) = ⋃ i ∈ s, ↑(i • lowerClosure t)
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ s ↔ b ∈ s) ↔ a ∈ s

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩

Goal state after:
G : Type u_1
inst✝ : Group G
s : Subgroup G
a : G
h : ∀ (b : G), b * a ∈ s ↔ b ∈ s
⊢ a ∈ s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
⊢ ∀ (x : G), (∀ (b : Gᵐᵒᵖ), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.unop

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_right ha⟩

Goal state after:
G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s
⊢ a ∈ s.unop
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
· rw [eq_C_of_natDegree_eq_zero hdp] at h ⊢
    simp [coeffList_C (C_ne_zero.mp h)]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
obtain Fa := congr_arg abs hF

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(algebraMap ℤ K) ev| =
    |(algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case isUnit_or_isUnit
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
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
have g_dvd_f : g ∣ f := by
      rw [fgh]
      exact dvd_mul_right g h

Goal state after:
case isUnit_or_isUnit
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
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Polynomial.Homogenize

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

Tactic:
homogenize,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∑ kl ∈ antidiagonal n, (MvPolynomial.monomial fun₀ | 0 => kl.1 | 1 => kl.2) (((monomial m) r).coeff kl.1) =
    (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i

Tactic:
have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt <| by lia
    simp [*]

Goal state after:
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).smeval x = p.smeval x + q.smeval x

Tactic:
by
  simp only [smeval_eq_sum]
  refine sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)
  · rw [smul_pow, zero_smul]
  · rw [smul_pow, smul_pow, smul_pow, add_smul]

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
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)
⊢ (r - eval r (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

Tactic:
eval_C,

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)
⊢ (r - 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.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
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        ((r - eval r (C r)) * eval r ((X - C r) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative)^[x + 1] p') =
    0

Tactic:
eval_C,

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
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) • ((r - r) * eval r ((X - C r) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative)^[x + 1] p') =
    0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
p : ℤ[X]
⊢ p.IsUnitTrinomial → (p.sum fun x x_1 ↦ x_1 ^ 2) = 3

Tactic:
rintro ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩
    rw [sum_def, trinomial_support hkm hmn u.ne_zero v.ne_zero w.ne_zero,
      sum_insert (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
      sum_insert (mt mem_singleton.mp hmn.ne), sum_singleton, trinomial_leading_coeff' hkm hmn,
      trinomial_middle_coeff hkm hmn, trinomial_trailing_coeff' hkm hmn]
    simp_rw [← Units.val_pow_eq_pow_val, Int.units_sq, Units.val_one]
    decide

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ trace ((algebraMap R (QuadraticAlgebra R a b)) r) = 2 * r

Tactic:
by
  grind [trace_def]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ trace (star z) = trace z

Tactic:
by
  grind [trace_def]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h : Multiset.countP (fun x ↦ 0 < x) ((X - C η) * Q).roots = n✝ + 1
hp : (X - C η) * Q ≠ 0
η_root : η ∈ ((X - C η) * Q).roots
⊢ n✝ + 1 ≤ ((X - C η) * Q).signVariations

Tactic:
ih Q,

Goal state after:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h : Multiset.countP (fun x ↦ 0 < x) ((X - C η) * Q).roots = n✝ + 1
hp : (X - C η) * Q ≠ 0
η_root : η ∈ ((X - C η) * Q).roots
⊢ Q.signVariations + 1 ≤ ((X - C η) * Q).signVariations

case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h : Multiset.countP (fun x ↦ 0 < x) ((X - C η) * Q).roots = n✝ + 1
hp : (X - C η) * Q ≠ 0
η_root : η ∈ ((X - C η) * Q).roots
⊢ Multiset.countP (fun x ↦ 0 < x) Q.roots = n✝
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case hP
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h : Multiset.countP (fun x ↦ 0 < x) ((X - C η) * Q).roots = n✝ + 1
hp : (X - C η) * Q ≠ 0
η_root : η ∈ ((X - C η) * Q).roots
⊢ Q ≠ 0

Tactic:
exact right_ne_zero_of_mul hp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ (x ◃ y) ◃ x = x ◃ y

Tactic:
by
  have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw [act_one]
  rw [h, ← Shelf.self_distrib, act_one]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
ih_y :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦y⟧ =
    F ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
this : ∀ (x y : EnvelGroup R), F (Mul.mul x y) = F x * F y
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) = F ⟦x.mul y⟧

Tactic:
by
            simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
            rw [← ih_x, ← ih_y, mapAux]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
⊢ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x} = sumNonzeroSq R

Tactic:
refine closure_eq_of_le (fun x hx ↦ by aesop) (fun x hx ↦ ?_)
  -- TODO : fix aesop timeout and change to `induction hx <;> aesop`
  induction hx with
  | sq ha => aesop
  | sq_add ha hs ih =>
    -- `aesop` times out
    apply add_mem
    · apply AddSubsemigroup.mem_closure_of_mem
      aesop
    aesop

Goal state after:
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
a : G
⊢ a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support

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

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
inst✝ : Semiring T
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
⊢ Quot.lift ⇑f ⋯ (toQuot 1) = 1

Tactic:
simp only [← one_quot, f.map_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
⊢ star (f (star 0)) = 0

Tactic:
by
      simp only [star_zero, map_zero]

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
⊢ ((conjStarAlgAut S R) u).symm = (conjStarAlgAut S R) (star u)

Tactic:
ext; simp [conjStarAlgAut_symm_apply]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0

pp: case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a

Tactic:
· rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
    · exact ⟨rfl, le_antisymm (le_zero _) h⟩
    · exact ⟨le_antisymm (le_zero _) h, rfl⟩

Goal state after:
case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case e_g
α : 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
a : α
b : β
c : α₂
⊢ (y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)).coeff c =
    (((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (f a * a₂) (b * f a • b₂)).coeff c

Tactic:
sum_mapDomain_index (by simp) (by simp [smul_add, mul_add, single_add])

Goal state after:
case e_g
α : 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
a : α
b : β
c : α₂
⊢ (y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)).coeff c =
    (y.sum fun a_1 m ↦ single (f a * f a_1) (b * f a • m)).coeff c
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ r • single g 1 = single g r

Tactic:
smul_single,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ single g (r • 1) = single g r
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_3
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 *
        (unsym a * unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) +
          unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) * unsym a)) =
    a * (b * (a * a))

Tactic:
· rw [← mul_def, ← mul_def]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom ({ base := f, c := fc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := fc }.base) x) hx))
        s) =
    (ConcreteCategory.hom ({ base := f, c := gc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := gc }.base) x) hx))
        s)

Tactic:
simp [h']

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ α = β

Tactic:
rcases α with ⟨base, c⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
β : X.Hom Y
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
w : { base := base, c := c }.base = β.base
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ { base := base, c := c } = β
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
⊢ V.carrier ⊆ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}

Tactic:
intro y hy

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ y ∈ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (stalkIso (↑S) p).toRingEquiv.symm
      ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p))
        ((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p))
          ((algebraMap (↑R) (Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal))) x))) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Tactic:
simp only [AlgEquiv.commutes, RingEquiv.symm_apply_eq, AlgEquiv.coe_ringEquiv]

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p))
      ((algebraMap ↑R ↑((structurePresheafInCommRingCat ↑R).stalk (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p))) x) =
    (algebraMap ↑S ↑((structurePresheafInCommRingCat ↑S).stalk p)) ((CommRingCat.Hom.hom f) x)