mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
⊢ motive (m * n * y * b) ⋯

Tactic:
simp_rw [LinearMap.mem_range] at hm hn

Goal state after:
case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm✝ : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn✝ : n ∈ (ι Q).range
hm : ∃ y, (ι Q) y = m
hn : ∃ y, (ι Q) y = n
⊢ motive (m * n * y * b) ⋯
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
⊢ x = 0 ∧ r = 0

pp: case refine_2
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r

Tactic:
· let : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
    have : IsCentralScalar R M := ⟨fun r m => rfl⟩
    have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := toTrivSqZeroExt_ι _
    rw [h, AlgHom.commutes] at hf0
    have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
    exact this.symm.imp_left Eq.symm

Goal state after:
case refine_2
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N

Tactic:
refine CliffordAlgebra.foldl _ ?_ ?_

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N

case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N), (?refine_1 m) ((?refine_1 m) x) = 0 m • x
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case ι_mul
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ : CliffordAlgebra 0
m✝ : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ g.compAlternatingMap (f i)) ((CliffordAlgebra.ι 0) m✝ * x✝) =
    g ((liftAlternating f) ((CliffordAlgebra.ι 0) m✝ * x✝))

Tactic:
rw [liftAlternating_ι_mul, liftAlternating_ι_mul, ← hx]

Goal state after:
case ι_mul
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ : CliffordAlgebra 0
m✝ : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ (g.compAlternatingMap (f i.succ)).curryLeft m✝) x✝ =
    (liftAlternating fun i ↦ g.compAlternatingMap ((f i.succ).curryLeft m✝)) x✝
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case pos
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : ↑i < m
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))

pp: case neg
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))

Tactic:
· rw [← Fin.castAdd_castLT n i hi, Fin.append_left, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_castAdd]
    aesop

Goal state after:
case neg
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))
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 (⇑(ιMulti R n) '' {a | range a ⊆ s}) = ⊤

Tactic:
by
  apply LinearMap.map_injective (ker_subtype (⋀[R]^n M))
  simpa [LinearMap.map_span, Set.image_image] using ιMulti_span_fixedDegree_of_span_eq_top R n M hs

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

Goal state before:
pp: case h
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 α
α_card : (Finset.image α Finset.univ).card = n
⊢ ExteriorAlgebra.ιMulti_family R n v ⟨Finset.image α Finset.univ, α_card⟩ =
    (ExteriorAlgebra.ιMulti R n)
      ((v ∘ α) ∘
        ⇑(((Finset.image α Finset.univ).orderIsoOfFin α_card).trans
            ((Equiv.setCongr ⋯).trans (Equiv.ofInjective α α_inj).symm)))

Tactic:
rw [ExteriorAlgebra.ιMulti_family, Function.comp_assoc]

Goal state after:
case h
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 α
α_card : (Finset.image α Finset.univ).card = n
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ ⇑(ofFinEmbEquiv.symm ⟨Finset.image α Finset.univ, α_card⟩)) =
    (ExteriorAlgebra.ιMulti R n)
      (v ∘
        α ∘
          ⇑(((Finset.image α Finset.univ).orderIsoOfFin α_card).trans
              ((Equiv.setCongr ⋯).trans (Equiv.ofInjective α α_inj).symm)))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).inv.app j ≫ (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom = 𝟙 ((F₁ ⊗ F₂ ⊗ F₃).obj j)

Tactic:
← associator_hom_app,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).inv.app j ≫ (α_ F₁ F₂ F₃).hom.app j = 𝟙 ((F₁ ⊗ F₂ ⊗ F₃).obj j)
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
this : Nonempty C := Nonempty.intro x
⊢ IsConnected C

Tactic:
apply isConnected_of_zigzag

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
this : Nonempty C := ⋯
⊢ ∀ (j₁ j₂ : C), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
this : Nonempty C := Nonempty.intro x
j₁ j₂ : C
⊢ ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
use [x, j₂]

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
this : Nonempty C := ⋯
j₁ j₂ : C
⊢ List.IsChain Zag [j₁, x, j₂] ∧ [j₁, x, j₂].getLast ⋯ = j₂
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
this : Nonempty C := Nonempty.intro x
⊢ IsConnected C

Tactic:
apply isConnected_of_zigzag

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
this : Nonempty C := ⋯
⊢ ∀ (j₁ j₂ : C), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
this : Nonempty C := Nonempty.intro x
j₁ j₂ : C
⊢ ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
use [x, j₂]

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsTerminal x
this : Nonempty C := ⋯
j₁ j₂ : C
⊢ List.IsChain Zag [j₁, x, j₂] ∧ [j₁, x, j₂].getLast ⋯ = j₂
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
⊢ ∀ (d : C × C), IsConnected (StructuredArrow d (Functor.diag C))

Tactic:
rintro ⟨c₁, c₂⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
c₁ c₂ : C
⊢ IsConnected (StructuredArrow (c₁, c₂) (Functor.diag C))
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
c₁ c₂ : C
this : Nonempty (StructuredArrow (c₁, c₂) (Functor.diag C))
⊢ IsConnected (StructuredArrow (c₁, c₂) (Functor.diag C))

Tactic:
apply isConnected_of_zigzag

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
c₁ c₂ : C
this : Nonempty (StructuredArrow (c₁, c₂) (Functor.diag C))
⊢ ∀ (j₁ j₂ : StructuredArrow (c₁, c₂) (Functor.diag C)), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ IsIso (CartesianMonoidalCategory.prodComparison colim X Y)

Tactic:
rw [← factorization_prodComparison_colim]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ IsIso
    ((HasColimit.isoOfNatIso ((externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom ≫
      colimit.pre (X ⊠ Y) (Functor.diag C) ≫
        (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))).hom)
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) colim
⊢ (d : C × C) → colimit (Functor.diag C ⋙ coyoneda.obj (op d)) ≅ PUnit.{u + 1}

Tactic:
rintro ⟨c₁, c₂⟩

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) colim
c₁ c₂ : C
⊢ colimit (Functor.diag C ⋙ coyoneda.obj (op (c₁, c₂))) ≅ PUnit.{u + 1}
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
⊢ F.Final ↔
    (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
by
  refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩
  · intro d
    obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty
    exact ⟨_, ⟨f.hom⟩⟩
  · let s₁ : C ≌ AsSmall.{max u₁ v₁ u₂ v₂} C := AsSmall.equiv
    let s₂ : D ≌ AsSmall.{max u₁ v₁ u₂ v₂} D := AsSmall.equiv
    have : IsFilteredOrEmpty (AsSmall.{max u₁ v₁ u₂ v₂} C) := .of_equivalence s₁
    intro d c s s'
    obtain ⟨c', t, ht⟩ := Functor.Final.exists_coeq_of_locally_small (s₁.inverse ⋙ F ⋙ s₂.functor)
      (AsSmall.up.map s) (AsSmall.up.map s')
    exact ⟨AsSmall.down.obj c', AsSmall.down.map t, s₂.functor.map_injective (by simp_all [s₁, s₂])⟩

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k ≫ (F.obj j).map fk ≫ (F.map fj).app k'

Tactic:
slice_rhs 2 3 => rw [← (D.obj j).π.naturality]

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
⊢ s.π.app j' ≫ (D.obj j').π.app k' =
    s.π.app j ≫ (((const K).obj (D.obj j).pt).map fk ≫ (D.obj j).π.app k') ≫ (F.map fj).app k'
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
⊢ m = P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } }

Tactic:
refine P.uniq
      { pt := s.pt
        ι := _ } m ?_
    rintro ⟨j, k⟩
    dsimp
    rw [← w j]
    simp

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k = limit.π (uncurry.obj F) (j, k)

Tactic:
dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso]

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (Cone.forget (F ⋙ lim)).map
        ((limit.isLimit (F ⋙ lim)).liftConeMorphism
          (coneOfConeUncurry (fun j ↦ limit.isLimit (F.obj j)) (limit.cone (uncurry.obj F)))) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (uncurry.obj F) (j, k)
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit (uncurry.obj (curry.obj G)) ≅ colimit (curry.obj G ⋙ colim)

Tactic:
exact colimitUncurryIsoColimitCompColim ((@curry J _ K _ C _).obj G)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
J : GrothendieckTopology C
S : Sieve X
⊢ S ∈ J X ↔ J.Covers S (𝟙 X)

Tactic:
by simp [covers_iff]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝¹ : PreservesLimitsOfShape WalkingCospan F
inst✝ : J.IsStableUnderBaseChange
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
hf : Presieve.ofArrows Y f ∈ (comap F J).coverings S
Z : C
g : Z ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Z
p₂ : (i : ι) → P i ⟶ Y i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ (comap F J).coverings Z

Tactic:
simp only [mem_comap_iff, Presieve.map_ofArrows] at hf ⊢

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝¹ : PreservesLimitsOfShape WalkingCospan F
inst✝ : J.IsStableUnderBaseChange
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
Z : C
g : Z ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Z
p₂ : (i : ι) → P i ⟶ Y i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
hf : (Presieve.ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)) ∈ J.coverings (F.obj S)
⊢ (Presieve.ofArrows (fun i ↦ F.obj (P i)) fun i ↦ F.map (p₁ i)) ∈ J.coverings (F.obj Z)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (GrothendieckTopology C)
⊢ (sInf T).toPretopology = sInf (GrothendieckTopology.toPretopology '' T)

Tactic:
ext X S

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (GrothendieckTopology C)
X : C
S : Presieve X
⊢ S ∈ (sInf T).toPretopology.coverings X ↔ S ∈ (sInf (GrothendieckTopology.toPretopology '' T)).coverings X
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
Z : C
g : Z ⟶ Y
hg : singleton f g
⊢ Z = X

Tactic:
cases hg; rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ generate R = ⊤

Tactic:
rw [← id_mem_iff_eq_top]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
⊢ ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
t₁

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ : P.obj (op X)
⊢ ∀ (t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x →
    Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)

Tactic:
intro t Y Z f g hf hg

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ (ConcreteCategory.hom (P.map (pullback.fst f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f hf) =
    (ConcreteCategory.hom (P.map (pullback.snd f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x g hg)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
⊢ ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
t₁

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ : P.obj (op X)
⊢ ∀ (t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
⊢ ∀ (t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
t₁

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ : (P ⋙ coyoneda.obj E).obj (op X)
⊢ ∀ (t₂ : (P ⋙ coyoneda.obj E).obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
x : FamilyOfElements P' R
⊢ ∀ (t₁ t₂ : P'.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
t₁

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
x : FamilyOfElements P' R
t₁ : P'.obj (op X)
⊢ ∀ (t₂ : P'.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
X : A
hX : IsTerminal X
⊢ ∀ (X_1 : Sheaf J A) (m : X_1 ⟶ terminal J hX), m = { hom := (Functor.isTerminalConst Cᵒᵖ hX).from X_1.obj }

Tactic:
by intros; ext; simpa using! hX.hom_ext _ _

Goal state after: