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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
Q : QuadraticMap R M N
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ f (Q (x + y)) = f (Q x) + f (Q y) + ((LinearMap.compr₂ B f) x) y

Tactic:
by simp only [h, map_add, LinearMap.compr₂_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
x y : M
⊢ (⇑f * ⇑g) (x + y) =
    (⇑f * ⇑g) x + (⇑f * ⇑g) y + (((LinearMap.mul R A).compl₁₂ f g + (LinearMap.mul R A).flip.compl₁₂ g f) x) y

Tactic:
by
      simp only [Pi.mul_apply, map_add, left_distrib, right_distrib, LinearMap.add_apply,
        LinearMap.compl₁₂_apply, LinearMap.mul_apply', LinearMap.flip_apply]
      abel_nf

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ (2 • ⅟2) (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝

Tactic:
nsmul_eq_mul,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ (↑2 * ⅟2) (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(((of (fun i ↦ ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = 0

Tactic:
rw [of_eq_of_ne _ _ _ (Ne.symm h)]
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁

Tactic:
rw [selfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint]

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✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < (Multiset.map Prod.snd s).sum
⊢ ∀ xn ∈ s.toList, ∀ k < xn.2, xn.1 k = 0

Tactic:
by simpa using hs

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✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ ∀ x ∈ s.toList, ∀ k < ?m.56, x k = 0

Tactic:
by simpa using hs

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✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ ∀ xn ∈ s.toList, ∀ k < xn.2, xn.1 k = 0

Tactic:
by simpa using hs

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✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ ∀ x ∈ s.toList, ∀ k < ?m.59, x k = 0

Tactic:
by simpa using hs

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
p : Fin (n + 1)
f : MultilinearMap R M M₂
c : R
x : M p
⊢ mk' (fun m ↦ f (p.insertNth (c • x) m)) ⋯ ⋯ = (RingHom.id R) c • mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯

Tactic:
ext; simp [map_insertNth_smul]

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
val✝ : Infinite α
⊢ Nat.card ↑(powersetCard α n) = (Nat.card α).choose n

Tactic:
rcases n with _ | n
    · simp [powersetCard]
    · rw [Nat.card_eq_zero_of_infinite (α := α), Nat.choose_zero_succ]
      exact Nat.card_eq_zero_of_infinite

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f

Tactic:
by
  refine ⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩
  obtain ⟨x, hx⟩ := h (ι R y)
  existsi ιInv x
  rw [← LinearMap.comp_apply, ← ιInv_comp_map, LinearMap.comp_apply]
  simp [hx, ιInv]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X 1)
X✝ Y✝ : C
f : X✝ ⟶ X
g : X✝ ⟶ Y✝
x✝ : Mono g
φ : { X₁ := X✝, X₂ := Y✝, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ ⟶ X
hφ :
  (Ext.mk₀ { X₁ := X✝, X₂ := Y✝, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.f).comp (Ext.homEquiv₀.symm φ)
      ⋯ =
    Ext.mk₀ f
⊢ Ext.homEquiv₀.symm (g ≫ φ) = Ext.homEquiv₀.symm f

Tactic:
by simpa using hφ

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext Y X d
hd✝ : d = n + (k + 1)
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
hd : n + k + 1 = d
⊢ (Ext.mk₀ { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.g).comp e ⋯ = 0

Tactic:
subst hd

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
Y : C
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
e : Ext Y X (n + k + 1)
hd : n + k + 1 = n + (k + 1)
⊢ (Ext.mk₀ { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.g).comp e ⋯ = 0
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
s : Set M
hs : span R s = ⊤
⊢ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}) = ⋀[R]^n M

Tactic:
apply le_antisymm
  · rw [span_le]
    rintro - ⟨y, ⟨y_mem, rfl⟩⟩
    apply ExteriorAlgebra.ιMulti_range R n
    simp
  · rw [ExteriorAlgebra.exteriorPower, LinearMap.range_eq_map, ← hs, map_span, span_pow, span_le]
    rintro x hx
    obtain ⟨f, rfl⟩ := Set.mem_pow.mp hx
    refine mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩
    · rw [Set.mem_ofPred_eq, Set.range_comp, Set.image_subset_iff]
      apply Subset.trans ?_ (s.image_subset_preimage_of_inverse ExteriorAlgebra.ι_leftInverse)
      grind
    · rw [ExteriorAlgebra.ιMulti_apply]
      apply congrArg (List.prod ∘ List.ofFn)
      ext i
      obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2
      rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃ = ↑(n + p)

Tactic:
← hN,

Goal state after:
R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃ = ↑(finrank R ↑S.X₁ + p)
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
h : PreservesFiniteProducts colim
⊢ IsSifted C

Tactic:
have := isSiftedOrEmpty_of_colim_preservesFiniteProducts C
  have := nonempty_of_colim_preservesLimitsOfShapeFinZero C
  constructor

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right ≫ t) =
    (StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))).hom

Tactic:
by simpa using ht.symm

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
P : ObjectProperty J
inst✝ : ObjectProperty.EssentiallySmall.{v, v, u} P
hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)
Q : ObjectProperty J
H : ObjectProperty.Small.{v, v, u} Q
hQ : P ≤ Q.isoClosure
this :
  Small.{v, u}
    (have this := Q;
    ↑this)
i j : J
hj : P j
f : j ⟶ i
k : J
hk : Q k
e : j ≅ k
⊢ ∃ j ∈ Q, Nonempty (j ⟶ i)

Tactic:
exact ⟨k, hk, ⟨e.inv ≫ f⟩⟩

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'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m) =
    (ιR cR) r • (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m

Tactic:
ModuleColimit.smul_eq,

Goal state after:
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'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m) =
    ιM (r • (((toPresheaf R).map f).app U).hom' m)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ ∀ (x : C), (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)

Tactic:
intro W

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
⊢ (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) = R

Tactic:
by
  refine le_antisymm ?_ ?_
  · rintro _ _ ⟨X, h⟩
    exact h
  · rintro X g hg
    exact .mk (ι := R.category) ⟨Over.mk g, hg⟩

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd ≍
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry

Tactic:
rw [heq_iff_eq] at h

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd =
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd ≍
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).uncurry

Tactic:
rw [heq_iff_eq] at h

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd =
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).uncurry
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
⊢ (FamilyOfElements.pullback f x).SieveCompatible

Tactic:
intro W

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W : C
⊢ ∀ ⦃Z : C⦄ (f_1 : W ⟶ Y) (g : Z ⟶ W) (hf : (Sieve.pullback f S).arrows f_1),
    FamilyOfElements.pullback f x (g ≫ f_1) ⋯ =
      (ConcreteCategory.hom (P.map g.op)) (FamilyOfElements.pullback f x f_1 hf)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
⊢ ofArrows Y f ≤ ofObjects Y X

Tactic:
intro W

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
⊢ ∀ (f_1 : W ⟶ X), (ofArrows Y f).arrows f_1 → (ofObjects Y X).arrows f_1
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
⊢ ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows f_1

Tactic:
intro W

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
⊢ ∀ (f_1 : W ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows f_1
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : t₁ = x (𝟙 X) trivial
q₂ : t₂ = x (𝟙 X) trivial
⊢ t₁ = t₂

Tactic:
q₁,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : t₁ = x (𝟙 X) trivial
q₂ : t₂ = x (𝟙 X) trivial
⊢ x (𝟙 X) trivial = t₂
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ Nonempty (Unique ({ pt := E, π := π } ⟶ P.mapCone S.arrows.cocone.op))

Tactic:
← eqv.left_inv π

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ Nonempty (Unique ({ pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } := ⋯
⊢ ∀ (a b : { pt := E, π := π } ⟶ P.mapCone S.arrows.cocone.op), a = b

Tactic:
← eqv.left_inv π

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∀ (a b : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op), a = b
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (b : S.functor ⟶ P), ∃! a, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a = S.shrinkFunctorIsoFunctor.homFromEquiv.symm b) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f

Tactic:
refine forall_congr' fun a ↦ ?_

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
⊢ (∃! a_1, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a_1 = S.shrinkFunctorIsoFunctor.homFromEquiv.symm a) ↔
    ∃! g, S.functorInclusion ≫ g = a
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
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map ((f i).op ≫ g.op) = y ≫ P.map ((f i).op ≫ g.op)

Tactic:
P.map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map (f i).op ≫ P.map g.op = y ≫ P.map (f i).op ≫ P.map g.op