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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
hc :
  ∀ (i : ι),
    ∃ q' r', i ∈ s → (∀ (j : Fin (n i)), (r' j).degree < (g i).degree) ∧ r i = q' * g i ^ n i + ∑ j, r' j * g i ^ ↑j
⊢ ∃ q r,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
choose q' r' hr' hr using hc

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ ∃ q r,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
⊢ (algebraMap R[X] K) (∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
map_sum,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
⊢ (∑ x ∈ s, (algebraMap R[X] K) (∑ j, r x j * g x ^ ↑j * ∏ k ∈ s.erase x, g k ^ n k)) * ∏ i ∈ s, gi i ^ n i =
    ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
⊢ (algebraMap R[X] K) (∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
map_sum,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
⊢ (∑ x, (algebraMap R[X] K) (r i x * g i ^ ↑x * ∏ k ∈ s.erase i, g k ^ n k)) * ∏ i ∈ s, gi i ^ n i =
    ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
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₃]
⊢ q.lift (x * y) = q.lift x * q.lift y

Tactic:
simp only [lift, Algebra.algebraMap_eq_smul_one]

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 • 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
⊢ (algebraMap R[X] K) q * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i +
      ∑ x ∈ s, ∑ i, (algebraMap R[X] K) (r x i) * gi x ^ (↑i + 1) * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i) +
      (algebraMap R[X] K) (∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ i ∈ s.erase i, g i ^ n i)

Tactic:
map_sum,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
⊢ (algebraMap R[X] K) q * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i +
      ∑ x ∈ s, ∑ i, (algebraMap R[X] K) (r x i) * gi x ^ (↑i + 1) * ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i) +
      ∑ x ∈ s, ∑ x_1, (algebraMap R[X] K) (r x x_1.rev * g x ^ ↑x_1 * ∏ i ∈ s.erase x, g i ^ n i)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext <;> congr

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

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext <;> congr

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

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext <;> congr

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

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_4
inst✝⁵ : Monoid G
inst✝⁴ : Semiring A
inst✝³ : CommSemiring k
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
⊢ domCongrAlg k A ⋯ = AlgEquiv.refl

Tactic:
apply AlgEquiv.ext
  aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a n : ℕ
h : a.AtLeastTwo
⊢ (↑(OfNat.ofNat a)).coeff (n + 1) = 0

Tactic:
simp [-Nat.cast_ofNat]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℤ
⊢ C ↑n = ↑n

Tactic:
by simp [← CRingHom_eq_C]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
x✝ : ℕ
⊢ (p.update n a).coeff x✝ = Function.update p.coeff n a x✝

Tactic:
simp [coeff, update]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
x✝ : ℕ
⊢ Function.update (⇑p.coeff) (ofAdd n) a (ofAdd x✝) = Function.update p.coeff n a x✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (liftNC ↑f ⇑g) (a.sum fun a₁ b₁ ↦ b.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (liftNC ↑f ⇑g) (a.sum single) * (liftNC ↑f ⇑g) (b.sum single)

Tactic:
map_sum,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (a.sum fun a b_1 ↦ b.sum fun a_1 b ↦ (liftNC ↑f ⇑g) (single (a * a_1) (b_1 * a • b))) =
    (a.sum fun a b ↦ (liftNC ↑f ⇑g) (single a b)) * b.sum fun a b ↦ (liftNC ↑f ⇑g) (single a b)
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
r : R
m : M
hr : r = 0
⊢ (r, m) = inr (snd (r, m))

Tactic:
rw [hr]; rfl

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0

Tactic:
rw [add_eq_iff]
  constructor
  · rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
    · exact ⟨rfl, le_antisymm (le_zero _) h⟩
    · exact ⟨le_antisymm (le_zero _) h, rfl⟩
  · rintro ⟨rfl, rfl⟩
    simp

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' ↑∅)) = ∑ i ∈ ∅, trop (f i)

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 (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)

Tactic:
· simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]

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
⊢ trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)
Module: Mathlib.CategoryTheory.Sites.Pullback

Goal state before:
pp: C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
D : Type u₃
inst✝⁷ : Category.{v₃, u₃} D
G : C ⥤ D
A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁵ : G.IsContinuous J K
inst✝⁴ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasLeftKanExtension F
inst✝³ : RepresentablyFlat G
inst✝² : HasSheafify K A
inst✝¹ : HasSheafify J A
inst✝ : PreservesFiniteLimits G.op.lan
⊢ PreservesFiniteLimits (sheafPullback G A J K)

Tactic:
have : PreservesFiniteLimits (G.op.lan ⋙ presheafToSheaf K A) :=
    comp_preservesFiniteLimits _ _

Goal state after:
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
D : Type u₃
inst✝⁷ : Category.{v₃, u₃} D
G : C ⥤ D
A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁵ : G.IsContinuous J K
inst✝⁴ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasLeftKanExtension F
inst✝³ : RepresentablyFlat G
inst✝² : HasSheafify K A
inst✝¹ : HasSheafify J A
inst✝ : PreservesFiniteLimits G.op.lan
this : PreservesFiniteLimits (G.op.lan ⋙ presheafToSheaf K A)
⊢ PreservesFiniteLimits (sheafPullback G A J K)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
← stalkMap.comp,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫ Hom.stalkMap (α ≫ β) x = 𝟙 (X.presheaf.stalk x)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
h : α.c ≍ β.c
⊢ α = β

Tactic:
by
  cases α
  cases β
  congr

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap (e.hom ≫ e.inv) x = X.presheaf.stalkSpecializes ⋯

Tactic:
LocallyRingedSpace.stalkMap_congr_hom (e.hom ≫ e.inv) (𝟙 _) (by simp)

Goal state after:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯
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 :
  (X.restrict hf).presheaf.map (eqToHom hV).op ≫
      g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    (X.restrict hf).presheaf.map (eqToHom hV).op ≫
      g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
simp only [g₁.c.naturality, g₂.c.naturality_assoc] at h

Goal state after:
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) ≫ ((Presheaf.pushforward C g₁.base).obj Z.presheaf).map (eqToHom hV).op =
    g₂.c.app (op V) ≫ ((Presheaf.pushforward C g₂.base).obj Z.presheaf).map (eqToHom hV).op ≫ Z.presheaf.map (eqToHom ⋯)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (X.restrict ⋯).presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
dsimp
  rw [Opens.inclusion'_top_functor X.carrier]
  rfl

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
      ?_

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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
⊢ ((pushforward C
              (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).obj
          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt.presheaf).obj
      (op U) ≅
    limit (componentwiseDiagram F U)
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
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (colimit.ι F j ≫
                  (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).c.app
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U)) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
congr_app (colimit.isoColimitCocone_ι_hom _ _),

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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
      (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
            (op
              ((Opens.map
                    (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                U))).inv ≫
        (({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                  U)) ≫
            (F.obj j).presheaf.map (eqToHom ⋯)) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
w : ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      (ConcreteCategory.hom
              (colimit.ι
                (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
                  (subpresheafToTypes P.toPrelocalPredicate))
                U))
            ⟨fU, hU⟩ =
          (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
        (ConcreteCategory.hom
              (colimit.ι
                (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
                  (subpresheafToTypes P.toPrelocalPredicate))
                V))
            ⟨fV, hV⟩ =
          (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩

Tactic:
rcases w with ⟨W, iU, iV, w⟩

Goal state after:
case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : (ConcreteCategory.hom ((P.cocone x).ι.app U)) ⟨fU, hU⟩ = (ConcreteCategory.hom ((P.cocone x).ι.app V)) ⟨fV, hV⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      (ConcreteCategory.hom
              (colimit.ι
                (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
                  (subpresheafToTypes P.toPrelocalPredicate))
                U))
            ⟨fU, hU⟩ =
          (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
        (ConcreteCategory.hom
              (colimit.ι
                (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
                  (subpresheafToTypes P.toPrelocalPredicate))
                V))
            ⟨fV, hV⟩ =
          (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩
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)))

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 (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))

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

Goal state after:
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 (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))