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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (d + 1 + 1)) (P.coeff (d + 1)) -
      ((monomial (d + 1)) (P.coeff d) - (monomial (d + 1)) (η * P.coeff (d + 1))) =
    X * P - C η * P - ((monomial (d + 1 + 1)) (P.coeff (d + 1)) - (monomial (d + 1)) (η * P.coeff (d + 1))) -
      (monomial (d + 1)) (P.coeff d)

Tactic:
abel

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

Goal state before:
pp: case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
· rw [h1] at hq
    rw [trinomial_def] at hp
    rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg]
      at hp
    rw [← neg_mul_neg, ← mirror_neg] at hpq
    rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inr p.mirror_neg))

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

Tactic:
simp only [smul_add]

Goal state after:
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 * w.re) • 1 + (z.re * w.im + z.im * w.re) • ↑u + ((z.im * w.im) • a • 1 + (z.im * w.im) • b • ↑u) =
    (z.re * w.re + a * z.im * w.im) • 1 + (z.re * w.im + z.im * w.re + b * z.im * w.im) • ↑u
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

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

Tactic:
abel

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

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

Tactic:
abel

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

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

Tactic:
abel

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

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

Tactic:
abel

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✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
z : QuadraticAlgebra R a b
⊢ { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        s *
      z =
    z *
      { toFun := fun s ↦ QuadraticAlgebra.C ((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        s

Tactic:
ext <;> simp [Algebra.commutes]

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
r1 r2 : R
⊢ r1 • QuadraticAlgebra.C r2 = QuadraticAlgebra.C (r1 * r2)

Tactic:
by rw [C_mul, C_mul_eq_smul]

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
⊢ norm z = 1 ↔ z ∈ unitary (QuadraticAlgebra R a b)

Tactic:
rw [Unitary.mem_iff_self_mul_star, ← algebraMap_norm_eq_mul_star]

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ norm z = 1 ↔ (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 1
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
⊢ Quotient.liftOn 1 (mapAux f) ⋯ = 1

Tactic:
change Quotient.liftOn ⟦Rack.PreEnvelGroup.unit⟧ (toEnvelGroup.mapAux f) _ = 1

Goal state after:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
⊢ ⟦unit⟧.liftOn (mapAux f) ⋯ = 1
Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup G
inst✝² : Module R G
inst✝¹ : DecidableEq G
s : Finset R
t : Finset G
inst✝ : DecidableEq R
⊢ -s • t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]
  exact image₂_image_left_comm neg_smul

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₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (algebraMap R A) x.re + (algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    (algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      ((algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)

Tactic:
abel

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

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
a✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹,
        mul_assoc := mul_assoc✝¹ }.toNonUnitalNonAssocSemiring =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_assoc := mul_assoc✝ }.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_assoc := mul_assoc✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_assoc := mul_assoc✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toAddMonoidWithOne R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toAddMonoidWithOne✝¹ : AddMonoidWithOne R
add_comm✝¹ : ∀ (a b : R), a + b = b + a
toAddMonoidWithOne✝ : AddMonoidWithOne R
add_comm✝ : ∀ (a b : R), a + b = b + a
a✝ :
  { toAddMonoidWithOne := toAddMonoidWithOne✝¹, add_comm := add_comm✝¹ }.toAddMonoidWithOne =
    { toAddMonoidWithOne := toAddMonoidWithOne✝, add_comm := add_comm✝ }.toAddMonoidWithOne
⊢ { toAddMonoidWithOne := toAddMonoidWithOne✝¹, add_comm := add_comm✝¹ } =
    { toAddMonoidWithOne := toAddMonoidWithOne✝, add_comm := add_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocSemiring R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocSemiring =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalSemiring✝ : NonUnitalSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalSemiring =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalSemiring
⊢ { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocRing R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toNonUnitalRing R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toNonUnitalRing✝¹ : NonUnitalRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalRing✝ : NonUnitalRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalRing =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }.toNonUnitalRing
⊢ { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toSemiring R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toSemiring✝¹ : Semiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toSemiring✝ : Semiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }.toSemiring
⊢ { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ } = { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
⊢ Function.Injective (@toRing R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Goal state after:
R : Type u
toRing✝¹ : Ring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toRing✝ : Ring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : { toRing := toRing✝¹, mul_comm := mul_comm✝¹ }.toRing = { toRing := toRing✝, mul_comm := mul_comm✝ }.toRing
⊢ { toRing := toRing✝¹, mul_comm := mul_comm✝¹ } = { toRing := toRing✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommGroup k
p : SkewMonoidAlgebra k G
⊢ (-p).support = p.support

Tactic:
rw [support, coeff_neg, Finsupp.support_neg, support_coeff]

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✝ : Algebra S R
r : R → R → Prop
⊢ ∀ (x y : S),
    { toQuot := Quot.mk (Rel r) ((algebraMap S R) (x + y)) } =
      { toQuot := Quot.mk (Rel r) ((algebraMap S R) x) } + { toQuot := Quot.mk (Rel r) ((algebraMap S R) y) }

Tactic:
by simp [add_quot]

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
⊢ ∀ (x y : R), { toQuot := Quot.mk (Rel r) (x + y) } = { toQuot := Quot.mk (Rel r) x } + { toQuot := Quot.mk (Rel r) y }

Tactic:
by simp [add_quot]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a : R
n : ℕ
hn : (⇑φ)^[n] a = ofAdd n • a
⊢ (⇑φ)^[n + 1] a = ofAdd (n + 1) • a

Tactic:
| succ n hn =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
this : 1 = (monomial 0) 1
⊢ coeff 1 n = if 0 = n then 1 else 0

Tactic:
rw [this, coeff_monomial]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
hn : X ^ n = (monomial n) 1
⊢ X ^ (n + 1) = (monomial (n + 1)) 1

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym b + unsym a * unsym c + (unsym b * unsym a + unsym c * unsym a) =
    unsym a * unsym b + unsym b * unsym a + (unsym a * unsym c + unsym c * unsym a)

Tactic:
abel

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym c + unsym b * unsym c + (unsym c * unsym a + unsym c * unsym b) =
    unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)

Tactic:
abel

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

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ star (toConv (↑f.ofConv ∘ₗ ↑f.ofConv⁻¹)) = toConv 1

Tactic:
simp [← mul_eq_comp, one_eq_id]

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

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ star (toConv (↑f.ofConv⁻¹ ∘ₗ ↑f.ofConv)) = toConv 1

Tactic:
simp [← mul_eq_comp, one_eq_id]

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)
x : R
⊢ IsUnit ((algebraMap R (End R V)) x - (star f).ofConv) ↔ IsUnit ((algebraMap R (End R V)) (star x) - f.ofConv)

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
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)
x : R
⊢ IsUnit (x • 1 - (star f).ofConv) ↔ IsUnit (star x • 1 - f.ofConv)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  (H.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) =
    (𝟙 X).c.app (op ((Opens.map H.hom.base).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))

Tactic:
have eq₂ := H.hom.c.naturality (eqToHom (congr_obj (congr_arg Opens.map
      ((forget C).congr_map H.inv_hom_id.symm)) U)).op

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  (H.hom ≫ H.inv).c.app (op ((Opens.map H.hom.base).obj U)) =
    (𝟙 X).c.app (op ((Opens.map H.hom.base).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
eq₂ :
  Y.presheaf.map (eqToHom ⋯).op ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯).op
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'

Tactic:
by
  subst hxx'
  simp

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

Goal state before:
pp: case w
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
j : J
U : ↑↑(F.obj j)
⊢ (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ desc F s).base) U = (ConcreteCategory.hom (s.ι.app j).base) U

pp: case h
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
j : J
U : Opens ↑↑s.pt
⊢ (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)

Tactic:
· simp [desc]

Goal state after:
case h
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
j : J
U : Opens ↑↑s.pt
⊢ (((colimitCocone F).ι.app j ≫ desc F s).c ≫ whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1 + Nat.succ 0)) = X.basicOpen f

Tactic:
| succ n hn =>

Goal state after:
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
⊢ (Limits.colimit F).presheaf.obj (op U) ≅ limit (componentwiseDiagram F U)

Tactic:
refine
    ((sheafIsoOfIso (colimit.isoColimitCocone ⟨_, colimitCoconeIsColimit F⟩).symm).app
          (op U)).trans
      ?_
  refine (limitObjIsoLimitCompEvaluation _ _).trans (Limits.lim.mapIso ?_)
  fapply NatIso.ofComponents
  · intro X
    refine (F.obj (unop X)).presheaf.mapIso (eqToIso ?_)
    simp only [Functor.op_obj, op_inj_iff, Opens.map_coe, SetLike.ext'_iff,
      Set.preimage_preimage]
    refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)
    simp only [colimitCocone, colimit, ← TopCat.comp_app]
    congr
    exact ι_preservesColimitIso_inv (forget C) F (unop X)
  · intro X Y f
    change ((F.map f.unop).c.app _ ≫ _ ≫ _) ≫ (F.obj (unop Y)).presheaf.map _ = _ ≫ _
    rw [TopCat.Presheaf.Pushforward.comp_inv_app]
    erw [Category.id_comp]
    rw [Category.assoc]
    erw [← (F.obj (unop Y)).presheaf.map_comp, (F.map f.unop).c.naturality_assoc,
      ← (F.obj (unop Y)).presheaf.map_comp]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
obtain ⟨⟨s, ⟨_, n, rfl⟩⟩, hsn⟩ :=
    @IsLocalization.surj _ _ _ _ _ _
      (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) s'

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (g.c.app (op (h.functor.obj U)))

Tactic:
exact c_iso' g ((opensFunctor f).obj U) (by ext; simp)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) = X.presheaf.map (eqToHom ⋯)

Tactic:
rw [invApp, Category.assoc, IsIso.inv_hom_id, Category.comp_id]

Goal state after: