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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp } =
    (RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i
Module: Mathlib.Algebra.Polynomial.OfFn

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

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) = m

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
i : Fin 2
⊢ (fun₀ | 0 => m 0 | 1 => m 1) i = m i
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
⊢ p = 0

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
⊢ p.coeff i = coeff 0 i
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case singleton
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
x✝ a : α
⊢ IsChain R (destutter' R a [x✝])

Tactic:
| singleton =>

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

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
n : ℕ
⊢ ((monomial (n + 1)) a).smeval 0 = ((monomial (n + 1)) a).coeff 0 • 1

Tactic:
coeff_monomial_succ,

Goal state after:
case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
n : ℕ
⊢ ((monomial (n + 1)) a).smeval 0 = 0 • 1
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = 3

Tactic:
coeff_mul_mirror

Goal state after:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff

Tactic:
cases _ : SignType.sign P.leadingCoeff

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.zero
⊢ SignType.zero = -SignType.sign P.eraseLead.leadingCoeff

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.neg
⊢ SignType.neg = -SignType.sign P.eraseLead.leadingCoeff

case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
h✝ : SignType.sign P.leadingCoeff = SignType.pos
⊢ SignType.pos = -SignType.sign P.eraseLead.leadingCoeff
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  g i * (q₁ * ∏ x ∈ s, g x) + (r₁ i * ∏ x ∈ s, g x + g i * ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
    g i * (q₂ * ∏ x ∈ s, g x) + (r₂ i * ∏ x ∈ s, g x + g i * ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
rw [add_left_comm, ← mul_add, add_left_comm, ← mul_add] at hf

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  r₁ i * ∏ x ∈ s, g x + g i * (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
    r₂ i * ∏ x ∈ s, g x + g i * (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case hq
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * 0
⊢ False

Tactic:
rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp

Goal state after:
case hq
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
hp : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2.e_a.e_a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ (aeval r) ((⇑derivative)^[q - 1] p) = (q - 1)! • eval r p'

Tactic:
rw [← aeval_iterate_derivative_self _ _ _ hp]

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

Goal state before:
pp: α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : PresentedMonoid rels
⊢ x ∈ closure (range (of rels))

Tactic:
induction x with

Goal state after:
case h
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
a : FreeMonoid α
⊢ (mk rels) a ∈ closure (range (of rels))
Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
⊢ ⇑((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec ⇑((basis a b).repr w)

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
w : QuadraticAlgebra R a b
i : Fin 2
⊢ ((basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w)) i =
    !![z.re, a * z.im; z.im, z.re + b * z.im].mulVec (⇑((basis a b).repr w)) i
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x * act' y * (act' x)⁻¹

Tactic:
by
  rw [eq_mul_inv_iff_mul_eq]; ext z
  apply self_distrib.symm

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 : PreEnvelGroup R
⊢ ((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⟧

Tactic:
induction x with

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

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

Tactic:
have : inst₁.toAddGroupWithOne = inst₂.toAddGroupWithOne :=
    AddGroupWithOne.ext h_add h_one

Goal state after:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddCommGroup = inst₂.toAddCommGroup
this : inst₁.toAddGroupWithOne = inst₂.toAddGroupWithOne
⊢ inst₁ = inst₂
Module: Mathlib.Algebra.SkewPolynomial.Basic

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

Tactic:
by
  simp [support_eq_skewMonoidAlgebra_support, erase]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ f * (g + h) = f * g + f * h

Tactic:
simp only [mul_def]
    refine Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_add_index ?_ ?_)) ?_ <;>
      simp only [smul_zero, smul_add, mul_add, mul_zero, single_zero, single_add,
        forall_true_iff, sum_add]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
⊢ x ∈ kerIdeal R M ↔ x = inr x.snd

Tactic:
obtain ⟨r, m⟩ := x
  simp only [kerIdeal, RingHom.mem_ker, fstHom_apply, fst_mk]
  exact ⟨fun hr => by rw [hr]; rfl, fun hrm => by rw [← fst_mk r m, hrm, fst_inr]⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
E : Type u_6
inst✝⁵ : NonUnitalNonAssocSemiring E
inst✝⁴ : StarRing E
inst✝³ : Module R E
inst✝² : StarModule R E
inst✝¹ : SMulCommClass R E E
inst✝ : IsScalarTower R E E
x : E
⊢ star (toConv (mulRight R x)) = toConv (mulLeft R (star x))

Tactic:
by
  rw [star_eq_iff_star_eq, intrinsicStar_mulLeft, star_star]

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
⊢ ncoeff (of_coeff f hf) n = f (-n - 1)

Tactic:
ext v
  rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]

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)ˣ
⊢ toConv ((star (toConv ↑f.ofConv)).ofConv ∘ₗ (star (toConv ↑f.ofConv⁻¹)).ofConv) = toConv 1

Tactic:
← LinearMap.intrinsicStar_comp'

Goal state after:
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
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)ˣ
⊢ toConv ((star (toConv ↑f.ofConv⁻¹)).ofConv ∘ₗ (star (toConv ↑f.ofConv)).ofConv) = toConv 1

Tactic:
← LinearMap.intrinsicStar_comp'

Goal state after:
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
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      (X.restrictStalkIso h x).inv =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      Hom.stalkMap (X.ofRestrict h) x

Tactic:
| op V =>

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      (X.restrictStalkIso h x).inv =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      Hom.stalkMap (X.ofRestrict h) x
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
F : J ⥤ PresheafedSpace C
j : J
⊢ ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
        (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
          (pushforwardEq ⋯ (F.obj j).presheaf).hom).op =
    𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))

Tactic:
apply (opEquiv _ _).injective
    refine NatTrans.ext (funext fun U => ?_)
    induction U with
    | op U =>
      simp [opEquiv]
      rfl

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

Goal state before:
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)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
carrier✝ : Set ↑↑(((Functor.const J).obj (colimit F)).obj j')
is_open'✝ : IsOpen carrier✝
⊢ ((F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).c ≫
          whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app
      (op { carrier := carrier✝, is_open' := is_open'✝ }) =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
            ((Functor.const J).obj (colimit F)).map f).c.app
      (op { carrier := carrier✝, is_open' := is_open'✝ })

Tactic:
simp [← congr_arg NatTrans.app (limit.w (pushforwardDiagramToColimit F).leftOp f.op)]

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

Goal state before:
pp: X : LocallyRingedSpace
X✝ Y✝ : LocallyRingedSpace
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : forgetToSheafedSpace.map a₁✝ = forgetToSheafedSpace.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext : 1
    exact congr_arg InducedCategory.Hom.hom h

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

Goal state before:
pp: 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)

pp: 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)

Tactic:
exacts [h.1, h.2]

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

Goal state before:
pp: X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
op : {x : ↑X} → T x → T x
hop : ∀ {U : Opens ↑X} {a : (x : ↥U) → T ↑x}, P.pred a → ∀ (p : ↥U), ∃ W i, ↑p ∈ W ∧ P.pred fun x ↦ op (a (i x))
U : Opens ↑X
a : (x : ↥U) → T ↑x
ha : P.sheafify.pred a
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ (fun x ↦ op (a x)) (i x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ha⟩

Goal state after:
X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
op : {x : ↑X} → T x → T x
hop : ∀ {U : Opens ↑X} {a : (x : ↥U) → T ↑x}, P.pred a → ∀ (p : ↥U), ∃ W i, ↑p ∈ W ∧ P.pred fun x ↦ op (a (i x))
U : Opens ↑X
a : (x : ↥U) → T ↑x
ha✝ : P.sheafify.pred a
x : ↥U
Va : Opens ↑X
ma : ↑x ∈ Va
ia : Va ⟶ U
ha : P.pred fun x ↦ a (ia x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ (fun x ↦ op (a x)) (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha : P₁.sheafify.pred a
hb : P₂.sheafify.pred b
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P₃.pred fun x ↦ (fun x ↦ op (a x) (b x)) (i x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ha⟩

Goal state after:
X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha✝ : P₁.sheafify.pred a
hb : P₂.sheafify.pred b
x : ↥U
Va : Opens ↑X
ma : ↑x ∈ Va
ia : Va ⟶ U
ha : P₁.pred fun x ↦ a (ia x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P₃.pred fun x ↦ (fun x ↦ op (a x) (b x)) (i x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case app
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (X_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ) →
    (Y.restrict ⋯).presheaf.obj X_1 ≅ ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).obj X_1

Tactic:
intro U

Goal state after:
case app
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
⊢ (Y.restrict ⋯).presheaf.obj U ≅ ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).obj U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ autoParam
    (∀ {X_1 Y_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
      (Y.restrict ⋯).presheaf.map f_1 ≫
          (asIso (f.c.app (op ((opensFunctor f).obj (unop Y_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
        (asIso (f.c.app (op ((opensFunctor f).obj (unop X_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
          ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1)
    NatIso.ofComponents._auto_1

Tactic:
intro U

Goal state after:
case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
⊢ ∀ {Y_1 : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ} (f_1 : U ⟶ Y_1),
    (Y.restrict ⋯).presheaf.map f_1 ≫
        (asIso (f.c.app (op ((opensFunctor f).obj (unop Y_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
      (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
        ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map f_1
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
h' : Epi f.base
⊢ ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)

Tactic:
intro U

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ IsIso (f.c.app U)