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

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            ((AddMonoidAlgebra.single (k + k) (↑u * ↑w)).coeff +
                    (AddMonoidAlgebra.single (k + (n - m + k)) (↑u * ↑v)).coeff +
                  (AddMonoidAlgebra.single (k + n) (↑u * ↑u)).coeff +
                ((AddMonoidAlgebra.single (m + k) (↑v * ↑w)).coeff +
                    (AddMonoidAlgebra.single (m + (n - m + k)) (↑v * ↑v)).coeff +
                  (AddMonoidAlgebra.single (m + n) (↑v * ↑u)).coeff) +
              ((AddMonoidAlgebra.single (n + k) (↑w * ↑w)).coeff +
                  (AddMonoidAlgebra.single (n + (n - m + k)) (↑w * ↑v)).coeff +
                (AddMonoidAlgebra.single (n + n) (↑w * ↑u)).coeff))) }

Tactic:
Finsupp.filter_add,

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (k + k) (↑u * ↑w)).coeff +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                    (AddMonoidAlgebra.single (k + (n - m + k)) (↑u * ↑v)).coeff +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (k + n) (↑u * ↑u)).coeff +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (m + k) (↑v * ↑w)).coeff +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                    (AddMonoidAlgebra.single (m + (n - m + k)) (↑v * ↑v)).coeff +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (m + n) (↑v * ↑u)).coeff) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (n + k) (↑w * ↑w)).coeff +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
                  (AddMonoidAlgebra.single (n + (n - m + k)) (↑w * ↑v)).coeff +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (AddMonoidAlgebra.single (n + n) (↑w * ↑u)).coeff)) }
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 x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : 2 * ↑v * (↑w + ↑u) = 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = p.mirror

Tactic:
mul_right_inj' (show 2 * (v : ℤ) ≠ 0 from mul_ne_zero two_ne_zero v.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 x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : ↑w + ↑u = ↑z + ↑x
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: 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
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ k = k'

Tactic:
rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ←
      trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ← natTrailingDegree_mul_mirror, hpq,
      natTrailingDegree_mul_mirror, hq, trinomial_natTrailingDegree hkm' hmn' x.ne_zero]

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 = C ↑u * X ^ k + C ↑v * X ^ m + C ↑w * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
← neg_inj,

Goal state after:
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 = -(C ↑u * X ^ k + C ↑v * X ^ m + C ↑w * X ^ n)
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
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
⊢ z * z⁻¹ = 1

Tactic:
simp only [inv_def, Algebra.mul_smul_comm]

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
⊢ (norm z)⁻¹ • (z * star z) = 1
Module: Mathlib.Algebra.Quandle

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

Tactic:
have h := @self_act_act_eq _ _ (op x) (op y)

Goal state after:
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
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
t : Finset G
a : R
⊢ -a • t = -(a • t)

Tactic:
by
  simp only [← image_smul, ← image_neg_eq_neg, image_image, neg_smul, Function.comp_def]

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₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    x.re • y.re • 1 + x.re • y.imI • q.i + x.re • y.imJ • q.j + x.re • y.imK • q.k +
          (x.imI • y.re • q.i + x.imI • y.imI • (q.i * q.i) + x.imI • y.imJ • (q.i * q.j) +
            x.imI • y.imK • (q.i * q.k)) +
        (x.imJ • y.re • q.j + x.imJ • y.imI • (q.j * q.i) + x.imJ • y.imJ • (q.j * q.j) + x.imJ • y.imK • (q.j * q.k)) +
      (x.imK • y.re • q.k + x.imK • y.imI • (q.k * q.i) + x.imK • y.imJ • (q.k * q.j) + x.imK • y.imK • (q.k * q.k))

Tactic:
smul_smul

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
          ((x.imI * y.re) • q.i + (x.imI * y.imI) • (q.i * q.i) + (x.imI * y.imJ) • (q.i * q.j) +
            (x.imI * y.imK) • (q.i * q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (q.j * q.i) + (x.imJ * y.imJ) • (q.j * q.j) +
          (x.imJ * y.imK) • (q.j * q.k)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • (q.k * q.i) + (x.imK * y.imJ) • (q.k * q.j) +
        (x.imK * y.imK) • (q.k * q.k))
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
x : R
hx : x ^ 2 = 0
⊢ x = 0

Tactic:
by_contra! hc

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
x : R
hx : x ^ 2 = 0
hc : x ≠ 0
⊢ False
Module: Mathlib.Algebra.Ring.Subgroup

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -r₁ + -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
exact (M.1 * N.1).add_mem h₁ h₂

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case 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 → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
toQuot✝¹ : Quot (Rel s)
x : A
toQuot✝ : Quot (Rel s)
y : A
⊢ Quot.lift ⇑f ⋯ ({ toQuot := Quot.mk (Rel s) x } * { toQuot := Quot.mk (Rel s) y }).toQuot =
    Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel s) x }.toQuot * Quot.lift ⇑f ⋯ { toQuot := Quot.mk (Rel s) y }.toQuot

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

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

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

Tactic:
eq_neg_iff_add_eq_zero,

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ (p.update n 0).support = p.support.erase n

Tactic:
by
  simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = { coeff := f.coeff } + { coeff := g.coeff }

Tactic:
eta

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = f + { coeff := g.coeff }
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = { coeff := f.coeff } + { coeff := g.coeff }

Tactic:
eta

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = f + { coeff := g.coeff }
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
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
a : G →₀ k
⊢ { coeff := _s₁ • a } = { coeff := _s₂ • a }

Tactic:
ofCoeff_smul,

Goal state after:
k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
a : G →₀ k
⊢ _s₁ • { coeff := a } = _s₂ • { coeff := a }
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : star y * y = 1
⊢ y ∈ unitary S

Tactic:
simp [mem_iff, this, mul_comm y]

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ trop (s.inf f) = ∑ i ∈ s, trop (f i)

Tactic:
s.trop_inf

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ ∑ i ∈ s, trop (f i) = ∑ i ∈ s, trop (f i)
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
a₁ a₂ : G
b₁ b₂ : k
⊢ single (a₁ * a₂) (b₁ * a₁ • 0) = 0

Tactic:
simp [smul_zero, mul_zero, single_zero]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
            (⋯.functor.op.whiskerLeft ((Sheaf.forget A Y).map u))).hom ≫
        (ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj Y✝).obj) ⋯)).hom =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      (ObjectProperty.homMk (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj X✝).obj) ⋯) ≫
          (sheafPullback A hf).map u).hom

Tactic:
ObjectProperty.FullSubcategory.comp_hom

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
            (⋯.functor.op.whiskerLeft ((Sheaf.forget A Y).map u))).hom ≫
        (ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj Y✝).obj) ⋯)).hom =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      (ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj X✝).obj) ⋯)).hom ≫
        ((sheafPullback A hf).map u).hom
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
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m = desc F s

Tactic:
have t :
      m.base =
        colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) := by
      dsimp
      -- `colimit.hom_ext` used to be automatically applied by `ext` before https://github.com/leanprover-community/mathlib4/pull/21302
      apply colimit.hom_ext fun j => ?_
      ext
      rw [colimit.ι_desc, mapCocone_ι_app, ← w j]
      simp

Goal state after:
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
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
⊢ m = desc F s
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
intro x; have ⟨V, hV, i, h⟩ := w x; use V, hV, i

Goal state after:
case h
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ P.pred fun x ↦ f (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_2
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)

Tactic:
intro x; have ⟨V, hV, i, h⟩ := w x; use V, hV, i

Goal state after:
case h
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ Q.pred fun x ↦ f (i x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))).hom x)

Tactic:
← localRingHom_comp_stalkIso,

Goal state after:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (CommRingCat.ofHom
        (stalkIso (↑(CommRingCat.of ↑R))
                (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                  x)).symm.toRingEquiv.toRingHom ≫
      CommRingCat.ofHom
          (Localization.localRingHom
            (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) x).asIdeal
            x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯) ≫
        CommRingCat.ofHom (stalkIso (↑(CommRingCat.of (Localization M))) x).toRingEquiv.toRingHom)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
⊢ (f ≫ g) x = g (f x)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ PreservesLimitsOfShape WalkingCospan (opensFunctor f)

Tactic:
dsimp [Scheme.Hom.opensFunctor]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ PreservesLimitsOfShape WalkingCospan (LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ jointlySurjectivePrecoverage.coverings S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ jointlySurjectivePrecoverage.coverings (X i)
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ jointlySurjectivePrecoverage.coverings S

Tactic:
simp_rw [ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf hg ⊢
    intro x
    obtain ⟨i, y, rfl⟩ := hf x
    obtain ⟨j, z, rfl⟩ := hg i y
    use ⟨i, j⟩, z
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
ι : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings X ↔
    ∀ (x : F.obj X), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.IsStableUnderComposition
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u_1 v_1)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ P.precoverage.coverings (X i)
Z : C
p : Z ⟶ S
⊢ Presieve.ofArrows (fun p ↦ Y p.fst p.snd) (fun x ↦ g x.fst x.snd ≫ f x.fst) p → P p

Tactic:
intro ⟨i⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.IsStableUnderComposition
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u_1 v_1)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ P.precoverage.coverings (X i)
Z : C
p : Z ⟶ S
i : (i : ι) × σ i
⊢ P (g i.fst i.snd ≫ f i.fst)
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 : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst

Tactic:
by
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `NatTrans.ext`
  refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun x => ?_
  · change pullback.lift _ _ _ ≫ pullback.fst _ _ = _
    simp
  · induction x with | op x => ?_
    change ((_ ≫ _) ≫ _ ≫ _) ≫ _ = _
    simp_rw [Category.assoc]
    erw [← s.pt.presheaf.map_comp]
    erw [s.snd.c.naturality_assoc]
    have := congr_app s.condition (op (opensFunctor f |>.obj x))
    dsimp only [comp_c_app, unop_op] at this
    rw [← IsIso.comp_inv_eq] at this
    replace this := reassoc_of% this
    erw [← this, hf.invApp_app_assoc, s.fst.c.naturality_assoc]
    simp [eqToHom_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ (precoverage P).coverings X ↔ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(E.f i)) ∧ ∀ (i : E.I₀), P (E.f i)

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.snd f g)

Tactic:
SheafedSpace.isOpenImmersion_iff_hom

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.snd f g).hom
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
SheafedSpace.isOpenImmersion_iff_hom

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (pullback.fst g f).hom
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.hom.base
this : IsIso (forgetToPresheafedSpace.map f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso _ (SheafedSpace.forgetToPresheafedSpace)

Goal state after: