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

Goal state before:
pp: case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ MvPolynomial.coeff m ((MvPolynomial.monomial fun₀ | 0 => k | 1 => n - k) c) =
    if m 0 + m 1 = n then if k = m 0 then c else 0 else 0

Tactic:
MvPolynomial.coeff_monomial

Goal state after:
case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (if (fun₀ | 0 => k | 1 => n - k) = m then c else 0) = if m 0 + m 1 = n then if k = m 0 then c else 0 else 0
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
r₂ : Fin (n + 1) → R[X]
hr₂ : ∀ (i : Fin (n + 1)), (r₂ i).degree < g.degree
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, Fin.snoc rs₁ r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = r₂

Tactic:
cases r₂ using Fin.snocCases with

Goal state after:
case succ.snoc.snoc
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : q₁ * g ^ (n + 1) + ∑ i, Fin.snoc rs₁ r₁ i * g ^ ↑i = q₂ * g ^ (n + 1) + ∑ i, Fin.snoc rs₂ r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ Fin.snoc rs₁ r₁ = Fin.snoc rs₂ r₂
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp0 : p ≠ 0 := hp.ne_zero
  have hp1 : p ≠ 1 := by rintro rfl; rw [natDegree_one] at hp2; cases hp2
  rw [hp.irreducible_iff_lt_natDegree_lt hp1]
  simp_rw [show p.natDegree / 2 = 1 from
      (Nat.div_le_div_right hp3).antisymm
        (by apply Nat.div_le_div_right (c := 2) hp2),
    show Finset.Ioc 0 1 = {1} from rfl,
    Finset.mem_singleton, Multiset.eq_zero_iff_forall_notMem, mem_roots hp0, ← dvd_iff_isRoot]
  refine ⟨fun h r ↦ h _ (monic_X_sub_C r) (natDegree_X_sub_C r), fun h q hq hq1 ↦ ?_⟩
  rw [hq.eq_X_add_C hq1, ← sub_neg_eq_add, ← C_neg]
  apply h

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * X ^ n + C v * X ^ (n - m + k) + C w * X ^ (n - n + k) = trinomial k (n - m + k) n w v u

Tactic:
Nat.sub_self,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
hw : w ≠ 0
⊢ C u * X ^ n + C v * X ^ (n - m + k) + C w * X ^ (0 + k) = trinomial k (n - m + k) n w v u
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
exact card_support_trinomial hkm hmn u.ne_zero v.ne_zero w.ne_zero

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

Goal state before:
pp: p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial

Tactic:
rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]

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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) (↑((q + k).descFactorial k) * p')

Tactic:
hp',

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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ((q + k)! • p') = q ! • (aeval r) (↑((q + k).descFactorial k) * p')
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: 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
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
h : C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n) = C ↑u * X ^ (m' + n) + C ↑w * X ^ (n - m' + k + n)
⊢ q = p ∨ q = p.mirror

Tactic:
binomial_eq_binomial u.ne_zero w.ne_zero

Goal state after:
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
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
h :
  m + n = m' + n ∧ n - m + k + n = n - m' + k + n ∨
    ↑u = ↑w ∧ m + n = n - m' + k + n ∧ n - m + k + n = m' + n ∨
      ↑u + ↑w = 0 ∧ m + n = n - m + k + n ∧ m' + n = n - m' + k + n
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝¹ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝ : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this : ((X - C η) * P).leadingCoeff = P.leadingCoeff
h₉ : ¬((X - C η) * P).nextCoeff = 0
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
suffices ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead by
        have := leadingCoeff_cons_eraseLead h₉
        have := coeffList_eraseLead (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₉)
        grind [leadingCoeff_eraseLead_eq_nextCoeff]
      suffices monomial P.natDegree ((X - C η) * P).nextCoeff =
          monomial P.natDegree P.nextCoeff - C η * monomial P.natDegree P.leadingCoeff by
        grind [X_mul_monomial, sub_mul, mul_sub, self_sub_monomial_natDegree_leadingCoeff,
          natDegree_eraseLead_add_one, leadingCoeff_eraseLead_eq_nextCoeff]
      grind [coeff_X_sub_C_mul, nextCoeff_of_natDegree_pos, leadingCoeff]

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✝¹ : Monoid S
inst✝ : MulAction S R
x✝² x✝¹ : S
x✝ : QuadraticAlgebra R a b
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext <;> simp [mul_smul]

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.re * w.re) • 1 + (z.re * w.im) • ↑u + (z.im * w.re) • ↑u + (z.im * w.im) • (↑u * ↑u)

Tactic:
by
              simp only [mul_add, mul_one, add_mul, one_mul, ← add_assoc, smul_mul_smul]
              apply add_add_add_comm'

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

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr : QuadraticAlgebra.C (norm x) * QuadraticAlgebra.C r = QuadraticAlgebra.C 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1

Tactic:
C_eq_algebraMap,

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
r : R
hr :
  (algebraMap R (QuadraticAlgebra R a b)) (norm x) * (algebraMap R (QuadraticAlgebra R a b)) r =
    (algebraMap R (QuadraticAlgebra R a b)) 1
hr' : r * norm x = 1
⊢ ∃ b_1, x * b_1 = 1 ∧ b_1 * x = 1
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: 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
⊢ QuadraticAlgebra.C (norm z) * w = 0

Tactic:
C_eq_algebraMap,

Goal state after:
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
⊢ (algebraMap R (QuadraticAlgebra R a b)) (norm z) * w = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℕ
⊢ trace ↑n = 2 * ↑n

Tactic:
by
  simp [trace_def, re_natCast, im_natCast]

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : ¬norm z = 0
⊢ QuadraticAlgebra.C (norm z)⁻¹ * (z * star z) = 1

Tactic:
C_eq_algebraMap,

Goal state after:
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : ¬norm z = 0
⊢ (algebraMap K (QuadraticAlgebra K a b)) (norm z)⁻¹ * (z * star z) = 1
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃ op y = op x ◃ op y
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
h : op x ◃ op x = op y ◃ op y ↔ op x = op y
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y

Tactic:
simpa using h

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
⊢ inst₁ = inst₂

Tactic:
have : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne :=
    AddMonoidWithOne.ext h_add h_one

Goal state after:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
NonUnitalNonAssocSemiring.mem_center_iff,

Goal state after:
α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ AddMonoid.End.mulRight a = L a ∧ L a ∈ (toEndRingHom α).rangeS ↔ ∀ (b : α), Commute (L b) (L a)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
x : H
⊢ l.coeff (f.symm x) = (Finsupp.mapDomain (⇑f) l.coeff) x

Tactic:
Finsupp.mapDomain_equiv_apply

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (star a) * ↑(star z) = a * ↑(star z)

Tactic:
by rw [star_star]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial n) a = a • X ^ n

Tactic:
calc monomial n a = monomial n (a * 1) := by simp only [mul_one]
    _ = monomial n (a • 1) := by simp [mul_one, smul_eq_mul]
    _ = a • monomial n 1 := (SkewMonoidAlgebra.smul_single _ _ _).symm
    _ = a • X ^ n  := by rw [X_pow_eq_monomial]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b : R
h : Rel r a b
⊢ Rel r (Star.star a) (Star.star b)

Tactic:
by
  induction h with
  | of h          => exact Rel.of (hr _ _ h)
  | add_left _ h  => rw [star_add, star_add]
                     exact Rel.add_left h
  | mul_left _ h  => rw [star_mul, star_mul]
                     exact Rel.mul_right h
  | mul_right _ h => rw [star_mul, star_mul]
                     exact Rel.mul_left h

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
⊢ (a.coeff.sum fun a₁ b₁ ↦ b.coeff.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * b₂)) =
    b.coeff.sum fun a₁ b₁ ↦ a.coeff.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * b₂)

Tactic:
rw [Finsupp.sum_comm]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : CommMonoid G
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
a b : SkewMonoidAlgebra k G
hgk : ∀ (g : G) (r : k), g • r = r
⊢ (b.coeff.sum fun x' v' ↦ a.coeff.sum fun x v ↦ single (x * x') (v * v')) =
    b.coeff.sum fun a₁ b₁ ↦ a.coeff.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * b₂)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝³ : Monoid G
inst✝² : AddCommMonoid M
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid k
g : G
⊢ g • 0 = 0

Tactic:
by
    ext
    simp [comapSMul_def, mapDomain]

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ untrop (x + y) = untrop x

Tactic:
simpa using h

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ untrop (x + y) = untrop y

Tactic:
simpa using h

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

Goal state before:
pp: R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ toConv
      (mul' R A ∘ₗ
        ↑(TensorProduct.comm R A A) ∘ₗ
          (↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)

Tactic:
← comp_assoc _ (TensorProduct.comm R A A).toLinearMap

Goal state after:
R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ toConv
      ((mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) ∘ₗ
        (↑(TensorProduct.comm R A A) ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ (A (((of R).symm (B u)).coeff x✝¹) + A (((of R).symm (B v)).coeff x✝¹)).coeff x✝ =
    (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ + (A (((of R).symm (B v)).coeff x✝¹)).coeff x✝

Tactic:
rw [← HahnSeries.coeff_add]

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

Goal state before:
pp: case refine_2
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
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ ((Functor.const Jᵒᵖ).obj (s.pt.presheaf.obj U)).map f ≫
      (s.ι.app (unop j')).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)).map
        f

Tactic:
· dsimp
    rw [PresheafedSpace.congr_app (s.w f.unop).symm U]
    have w :=
      Functor.congr_obj
        (congr_arg Opens.map (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j)))
        (unop U)
    simp only [Opens.map_comp_obj_unop] at w
    replace w := congr_arg op w
    have w' := NatTrans.congr (F.map f.unop).c w
    rw [w']
    simp

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
h : g₁.c.app (op V) ≫ eqToHom ⋯ = g₂.c.app (op V)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
w :
  ∀ (x : ↥U),
    ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
by
    specialize w x
    rcases w with ⟨V, m, i, p⟩
    specialize p ⟨x.1, m⟩
    rcases p with ⟨V', m', i', p'⟩
    exact ⟨V', m', i' ≫ i, p'⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
Q : ∃ W s,
  ∃ (hW : P.pred s),
    tU = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
      tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ :=
  ?refine_1
⊢ tU = tV

Tactic:
choose W s hW e using Q

Goal state after:
case refine_2
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
W : (OpenNhds x)ᵒᵖ
s : (w : ↥↑(unop W)) → T ↑w
hW : P.pred s
e :
  tU = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
    tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩
⊢ tU = tV
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: 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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π (componentwiseDiagram F U) (op j) =
    (colimit.ι F j).c.app (op U)

Tactic:
by
  rw [← Iso.eq_inv_comp, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app]

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

Goal state before:
pp: 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
⊢ ∀ ⦃X_1 Y_1 : (Opens ↑↑X)ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
    X.presheaf.map f_1 ≫ invApp f (unop Y_1) ≫ g.c.app (op (⋯.functor.obj (unop Y_1))) ≫ Y.presheaf.map (eqToHom ⋯) =
      (invApp f (unop X_1) ≫ g.c.app (op (⋯.functor.obj (unop X_1))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map f_1

Tactic:
by
        intro U V i
        induction U
        induction V
        simp only [(inv_naturality_assoc), restrict_carrier, restrict_presheaf,
          TopCat.Presheaf.pushforward_obj_obj, Functor.comp_obj, Functor.op_obj,
          TopCat.Presheaf.pushforward_obj_map, Functor.comp_map, Functor.op_map, Quiver.Hom.unop_op,
          NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op,
          ← Functor.map_comp, Category.assoc]
        rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
i : op U ⟶ op V
⊢ Y.presheaf.map ((opensFunctor f).map i.unop).op ≫ (appIso f V).hom = (appIso f U).hom ≫ X.presheaf.map i

Tactic:
by
  simp [← cancel_mono (f.appIso V).inv]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
⊢ Epi f.base ∧ IsOpenEmbedding ⇑f → IsIso f.base

pp: case refine_2
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f.base → Epi f.base ∧ IsOpenEmbedding ⇑f

Tactic:
· rintro ⟨h₁, h₂⟩
    convert_to!
      IsIso
        (TopCat.isoOfHomeo
          (Equiv.toHomeomorphOfContinuousOpen
            (.ofBijective _ ⟨h₂.injective, (TopCat.epi_iff_surjective _).mp h₁⟩) h₂.continuous
            h₂.isOpenMap)).hom
    infer_instance

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f.base → Epi f.base ∧ IsOpenEmbedding ⇑f