mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i)) =
    polarSym2 (⇑Q) (Sym2.map f s(a, a)) + ∑ x ∈ s, polarSym2 (⇑Q) (Sym2.map f s(a, x)) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))

Tactic:
Sym2.map_mk,

Goal state after:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i)) =
    polarSym2 ⇑Q s(f a, f a) + ∑ x ∈ s, polarSym2 ⇑Q s(f a, f x) + ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (∑ i ∈ Finset.cons a s ha, f i) =
    ∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ Finset.cons a s ha, Q (f i)

Tactic:
simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons,
      Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply,
      Sym2.map_mk, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
      polarBilin_apply_apply, polar_self]
    abel_nf

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_2.refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (m m' : A),
    ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m) 0) →
      ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m')) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m') 0) →
        ↑(((decompose 𝒜) (↑⟨c, hc⟩ * (m + m'))) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) (m + m')) 0)

Tactic:
· intro _ _ hd he
        simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p

Tactic:
simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n

Tactic:
simp_rw [← submodule_map_reverse_eq_comap, submodule_map_pow_reverse]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
x : ι × ι
hx : x ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = k}
hm : m ≤ x.1
hn : n ≤ x.2
⊢ False

Tactic:
obtain rfl : x.1 + x.2 = k := by simp_all

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
x : ι × ι
hm : m ≤ x.1
hn : n ≤ x.2
hk : x.1 + x.2 < m + n
hx : x ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = x.1 + x.2}
⊢ False
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ (map n (g ∘ₗ f)) x✝ = x✝

Tactic:
hg,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ (map n LinearMap.id) x✝ = x✝
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
this : ∃ σ, (ExteriorAlgebra.ιMulti R n) ((v ∘ α) ∘ ⇑σ) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
by
    obtain ⟨σ, hσ⟩ := this
    rw [AlternatingMap.map_perm] at hσ
    refine (Submodule.smul_mem_iff_of_isUnit _ (r := (σ.sign : R)) ?_).mp hσ
    rw [isUnit_iff_exists_inv]
    use (σ.sign : R)
    norm_cast
    simp only [Int.units_mul_self, Units.val_one, Int.cast_one]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsPreconnected C
inst✝ : HasColimit (constPUnitFunctor C)
a b : colimit (constPUnitFunctor C)
⊢ a = b

Tactic:
obtain ⟨c, ⟨⟩, rfl⟩ := jointly_surjective' a

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsPreconnected C
inst✝ : HasColimit (constPUnitFunctor C)
b : colimit (constPUnitFunctor C)
c : C
⊢ (ConcreteCategory.hom (colimit.ι (constPUnitFunctor C) c)) PUnit.unit = b
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ F.partialLeftAdjointMap g ≫ F.partialLeftAdjointHomEquiv.symm f = F.partialLeftAdjointHomEquiv.symm (g.hom ≫ f)

Tactic:
Equiv.eq_symm_apply,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap g ≫ F.partialLeftAdjointHomEquiv.symm f) = g.hom ≫ f
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ F.partialRightAdjointHomEquiv (f ≫ F.partialRightAdjointMap g) = F.partialRightAdjointHomEquiv f ≫ g.hom

Tactic:
by
  rw [partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map,
    ← assoc, ← partialRightAdjointHomEquiv_comp, comp_id]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
N : ModuleCat ↑cR.pt
f : M ⟶ M'
g : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N
⊢ (homEquiv hcR hcM) ((homEquiv hcR hcM).symm (f ≫ (homEquiv hcR hcM') g)) =
    (homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ (homEquiv hcR hcM').symm ((homEquiv hcR hcM') g))

Tactic:
simp [homEquiv_naturality_left]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
⊢ pullbackObjIsDefined φ = ⊤

Tactic:
by
  ext M
  simp only [Pi.top_apply, Prop.top_eq_true, iff_true]
  apply leftAdjointObjIsDefined_of_isColimit
    M.isColimitFreeYonedaCoproductsCokernelCofork
  rintro (_ | _)
  all_goals
    apply leftAdjointObjIsDefined_colimit _
      (fun _ ↦ pullbackObjIsDefined_free_yoneda _ _)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback (g ≫ f) (Sieve.generate (S.bind Ti)) ∈ J Y

Tactic:
Sieve.pullback_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback g (Sieve.pullback f (Sieve.generate (S.bind Ti))) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ ⊥.Covers S f ↔ S.arrows f

Tactic:
by
  rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
x✝¹ x✝ : J.Cover X
h1 : x✝¹ ≤ x✝
h2 : x✝ ≤ x✝¹
Y : C
f : Y ⟶ X
⊢ (↑x✝¹).arrows f → (↑x✝).arrows f

Tactic:
by apply h1

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows Z g).bind Ti ∈ J.coverings X

Tactic:
have : (Presieve.ofArrows Z g).bind Ti =
        .ofArrows (fun ij : Σ i, κ (g i) ⟨i⟩ ↦ W _ _ ij.2) (fun ij ↦ p _ _ ij.2 ≫ g ij.1) := by
      apply le_antisymm
      · rintro T u ⟨S, v, w, ⟨i⟩, hv, rfl⟩
        rw [hp] at hv
        obtain ⟨j⟩ := hv
        exact .mk <| Sigma.mk (β := fun i : ι ↦ κ (g i) ⟨i⟩) i j
      · rintro T u ⟨ij⟩
        use Z ij.1, p (g ij.1) ⟨ij.1⟩ ij.2, g ij.1, ⟨ij.1⟩
        rw [hp]
        exact ⟨⟨_⟩, rfl⟩

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
⊢ (ofArrows Z g).bind Ti ∈ J.coverings X
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_1
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
i : s.pt
⊢ (Fork.ofι f w).pt

pp: case refine_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ (↾fun i ↦ ?refine_1) ≫ (Fork.ofι f w).ι = s.ι

pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ ?refine_1

Tactic:
· apply Classical.choose (t (s.ι i) _)
      apply congr_hom s.condition i

Goal state after:
case refine_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ (↾fun i ↦ Classical.choose ⋯) ≫ (Fork.ofι f w).ι = s.ι

case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : I → C
I' : Type u_2
X' : I' → C
Y : C
h : Set.range X ⊆ Set.range X'
⊢ ofObjects X Y ≤ ofObjects X' Y

Tactic:
rintro Z f ⟨i, ⟨g⟩⟩
  obtain ⟨i', h⟩ := h ⟨i, rfl⟩
  exact ⟨i', ⟨h ▸ g⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    (ConcreteCategory.hom (forkMap P X π)) t =
      (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) x)

Tactic:
Equiv.eq_symm_apply,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t) =
      (equivShrink ((j : I) → P.obj (op (X j)))) x
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
t₂ : P₂.obj (op X)
ht₂ : x₂.IsAmalgamation t₂
⊢ t₂ = e (hP₁.amalgamate x₁ hx₁)

Tactic:
refine e.symm.injective ?_

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
t₂ : P₂.obj (op X)
ht₂ : x₂.IsAmalgamation t₂
⊢ e.symm t₂ = e.symm (e (hP₁.amalgamate x₁ hx₁))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
i : S.shape.L
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index P) i))
      ((ConcreteCategory.hom
          (Multiequalizer.lift (S.index P) (multiequalizer (⊤.index P))
            (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.map I e)) ⋯))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x)) =
    (ConcreteCategory.hom (Multiequalizer.ι (S.index P) i)) ((Meq.equiv P S).symm (Meq.mk S x))

Tactic:
simp only [← ConcreteCategory.comp_apply, Category.assoc, Multiequalizer.lift_ι,
    Meq.equiv_symm_eq_apply]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
i : S.shape.L
⊢ (ConcreteCategory.hom (P.map (Cover.Arrow.map i e).f.op)) x = ↑(Meq.mk S x) i
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P fun i ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : (g₁ ≫ g i₁) ≫ inv f = (g₂ ≫ g i₂) ≫ inv f
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

Tactic:
simp only [Category.assoc] at h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P fun i ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ ≫ inv f = g₂ ≫ g i₂ ≫ inv f
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ G.sieveOfSection s ∈ J (unop U)

Tactic:
convert! J.top_mem U.unop

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ G.sieveOfSection s = ⊤
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
⊢ IsLimit (s.mapCone (Fork.ofι (forkMap R P) ⋯)) ≃ IsLimit (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯)

Tactic:
by
  let e : parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
    parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R)
      (Equalizer.Presieve.secondMap (P ⋙ s) R) := by
    refine parallelPair.ext (PreservesProduct.iso s _) ((PreservesProduct.iso s _))
      (limit.hom_ext (fun j => ?_)) (limit.hom_ext (fun j => ?_))
    · dsimp [Equalizer.Presieve.firstMap, firstMap]
      simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt,
        Fan.mk_π_app, assoc, piComparison_comp_π_assoc]
    · dsimp [Equalizer.Presieve.secondMap, secondMap]
      simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt,
        Fan.mk_π_app, assoc, piComparison_comp_π_assoc]
  refine Equiv.trans (isLimitMapConeForkEquiv _ _) ?_
  refine (IsLimit.postcomposeHomEquiv e _).symm.trans
    (IsLimit.equivIsoLimit (Fork.ext (Iso.refl _) ?_))
  dsimp [Equalizer.forkMap, forkMap, e, Fork.ι]
  simp only [id_comp, map_lift_piComparison]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
| Subfunctor.range f.hom

Tactic:
← I.fac

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
| Subfunctor.range (I.e ≫ I.m).hom
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
⊢ ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ (range ⇑(ConcreteCategory.hom c.inl))ᶜ

Tactic:
exact fun _ => or_not

Goal state after: