mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : 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 : ι
⊢ ↑(∑ a ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
        ((of (fun i ↦ ↥(A i)) (a.1 + a.2)) (GradedMonoid.GMul.mul (r a.1) (r' a.2))) n) =
    ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = n, ↑(r ij.1) * ↑(r' ij.2)

Tactic:
AddSubmonoidClass.coe_finsetSum

Goal state after:
ι : 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 : ι
⊢ ∑ i ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      ↑(((of (fun i ↦ ↥(A i)) (i.1 + i.2)) (GradedMonoid.GMul.mul (r i.1) (r' i.2))) n) =
    ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = n, ↑(r ij.1) * ↑(r' ij.2)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : 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 : ι
⊢ ↑(∑ i ∈ DFinsupp.support r,
        (DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n) =
    DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0

Tactic:
AddSubmonoidClass.coe_finsetSum

Goal state after:
ι : 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 : ι
⊢ ∑ i ∈ DFinsupp.support r,
      ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n) =
    DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case e_f
ι : 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✝ : ι
⊢ ↑(∑ i ∈ DFinsupp.support r', ((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n) =
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)

Tactic:
AddSubmonoidClass.coe_finsetSum

Goal state after:
case e_f
ι : 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✝ : ι
⊢ ∑ i ∈ DFinsupp.support r', ↑(((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n) =
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)
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
B₁ : BilinMap R M N
h : ∀ (x y : M), (B₁ x) y = (B₁ y) x
x y : M
⊢ (B₁ x) y + (B₁ x) y = 2 • (B₁ x) y

Tactic:
two_smul

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
B₁ : BilinMap R M N
h : ∀ (x y : M), (B₁ x) y = (B₁ y) x
x y : M
⊢ (B₁ x) y + (B₁ x) y = (B₁ x) y + (B₁ x) y
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
⊢ ((toMatrix b₁ b₂) ((toLin b₁ b₂) A))ᵀ * (toMatrix₂ b₂ b₂) ((toLinearMap₂ b₂ b₂) J') =
      (toMatrix₂ b₁ b₁) ((toLinearMap₂ b₁ b₁) J) * (toMatrix b₂ b₁) ((toLin b₂ b₁) A') ↔
    J.IsAdjointPair J' A A'

Tactic:
LinearMap.toMatrix_toLin,

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
⊢ Aᵀ * (toMatrix₂ b₂ b₂) ((toLinearMap₂ b₂ b₂) J') = (toMatrix₂ b₁ b₁) ((toLinearMap₂ b₁ b₁) J) * A' ↔
    J.IsAdjointPair J' A A'
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
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ (B₁ x✝) y + (B₁ x✝) y = 2 • (B₁ x✝) y

Tactic:
two_smul

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
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ (B₁ x✝) y + (B₁ x✝) y = (B₁ x✝) y + (B₁ x✝) y
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 : M
⊢ Q x + Q x = 2 • Q x

Tactic:
two_smul

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 : M
⊢ Q x + Q x = Q x + Q x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
r : R
⊢ P (reverse ((Algebra.algebraMap R (CliffordAlgebra Q)) r))

Tactic:
simpa only [reverse.commutes] using algebraMap r

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ (↑s).Nontrivial ↔ 1 < n

Tactic:
← one_lt_card_iff_nontrivial,

Goal state after:
α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ 1 < #↑s ↔ 1 < n
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s t : ↑(powersetCard α n)
⊢ s = t ↔ ↑s ⊆ ↑t

Tactic:
by
  rw [Finset.subset_iff_eq_of_card_le (t.prop.trans_le s.prop.ge), Subtype.ext_iff]

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ Finset.map f ↑s ∈ powersetCard β n

Tactic:
rw [mem_iff, card_map, s.prop]

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

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
⊢ (basisRepr Q v) w = (weightedSumSquares R fun i ↦ Q (v i)) w

Tactic:
basisRepr_apply,

Goal state after:
ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
⊢ Q (∑ i, w i • v i) = (weightedSumSquares R fun i ↦ Q (v i)) w
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 ↦ x) fun x ↦ y) = (f fun x_1 ↦ x) fun x ↦ y

Tactic:
rw [curryFinFinset_symm_apply]; congr
  · ext
    rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]
    apply Finset.orderEmbOfFin_mem
  · ext
    rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]
    exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (((Functor.const J).obj c.pt).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
⊢ (s.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s))) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j =
    ((hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j

Tactic:
rw [Functor.mapCone_π_app, assoc, assoc, ← Functor.map_comp, IsLimit.fac]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (((Functor.const J).obj c.pt).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone s).π.app j) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j)
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: case symm
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ y✝ : (j : C) × F.obj j
a✝ : Relation.EqvGen F.ColimitTypeRel x✝ y✝
ih : Zigzag x✝.fst y✝.fst
⊢ Zigzag y✝.fst x✝.fst

Tactic:
exact ih.symm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : InitiallySmall C
⊢ ∃ D x, ∃ (_ : IsCofiltered D), ∃ F, F.Initial

Tactic:
obtain ⟨D, _, _, F, _⟩ := FinallySmall.exists_of_isFiltered.{w} Cᵒᵖ
  exact ⟨Dᵒᵖ, inferInstance, inferInstance, F.leftOp, inferInstance⟩

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✝¹ : IsCofilteredOrEmpty C
T : C ⥤ D
inst✝ : T.Initial
Y : D
X : C
⊢ IsConnected (CostructuredArrow (Over.forget X ⋙ T) Y)

Tactic:
exact (initial_comp (Over.forget X) T).out _

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
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
rw [← cancel_mono (colimitIsoColimitCurryCompColim G).inv]

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
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom) ≫ (colimitIsoColimitCurryCompColim G).inv =
    (colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j) ≫ (colimitIsoColimitCurryCompColim G).inv
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
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y Y' : C
g : Y ⟶ Y'
f : Y' ⟶ c'.pt
j : J
⊢ {
          toFun := fun f ↦
            hc.lift
              { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
          invFun := fun g ↦
            hc'.lift
              { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }
        (g ≫ f) ≫
      c.π.app j =
    (ConcreteCategory.hom ((F.op ⋙ yoneda.obj c.pt).map g.op))
        ({
            toFun := fun f ↦
              hc.lift
                { pt := F.1 Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
            invFun := fun g ↦
              hc'.lift
                { pt := Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }
          f) ≫
      c.π.app j

Tactic:
dsimp
    simp only [IsLimit.fac, partialRightAdjointHomEquiv_comp, assoc]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (λ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom =
    (Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ▷
        (pushforward₀OfCommRingCat F R).obj x✝ ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) ⊗
                      (pushforward₀OfCommRingCat F R).obj x✝).obj
                  x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (λ_ x✝).hom

Tactic:
ext1
        exact tensor_ext fun m₁ m₂ ↦ rfl

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (ρ_ ((pushforward₀OfCommRingCat F R).obj x✝)).hom =
    (pushforward₀OfCommRingCat F R).obj x✝ ◁
        (Iso.refl (𝟙_ (PresheafOfModules ((F.op ⋙ R) ⋙ forget₂ CommRingCat RingCat)))).hom ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj x✝ ⊗
                      (pushforward₀OfCommRingCat F R).obj
                        (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)))).obj
                  x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (ρ_ x✝).hom

Tactic:
ext1
        exact tensor_ext fun m₁ m₂ ↦ rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
h : Sieve.ofArrows Z f ∈ J X
hR : ∀ (i : ι), Sieve.generate (R i) ∈ J (Z i)
⊢ Sieve.generate (Presieve.bindOfArrows Z f R) ∈ J X

Tactic:
refine J.superset_covering (Presieve.bind_ofArrows_le_bindOfArrows _ _ _) ?_
  exact J.bind_covering h fun _ _ _ ↦ J.pullback_stable _ (hR _)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
⊢ (∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g) → J.Covers R f

Tactic:
intro k
  apply J.transitive h
  intro Z g hg
  rw [← Sieve.pullback_comp]
  apply k (g ≫ f) hg

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
⊢ S.arrows (g₁ ≫ f₁)

Tactic:
exact Sieve.downward_closed S hf₁ g₁

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ functorPushforward G (functorPushforward F R) f → functorPushforward (F ⋙ G) R f

Tactic:
· rintro ⟨X, f₁, g₁, ⟨X', f₂, g₂, h₁, rfl⟩, rfl⟩
    exact ⟨X', f₂, g₁ ≫ G.map g₂, h₁, by simp⟩

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

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

Tactic:
exact ⟨⟨_, f⟩, hf, ⟨_, g⟩, ht, Sigma.ext rfl (heq_of_eq hv)⟩

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

Goal state before:
pp: case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝³.arrows f → x✝¹.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝².arrows f → x✝¹.arrows f
x✝ : C
f : x✝ ⟶ X
hf : x✝³.arrows f
⊢ x✝¹.arrows f

pp: case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝³.arrows f → x✝¹.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝².arrows f → x✝¹.arrows f
x✝ : C
f : x✝ ⟶ X
hf : x✝².arrows f
⊢ x✝¹.arrows f

Tactic:
· exact h₁ _ hf

Goal state after:
case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R x✝³ x✝² x✝¹ : Sieve X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝³.arrows f → x✝¹.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝².arrows f → x✝¹.arrows f
x✝ : C
f : x✝ ⟶ X
hf : x✝².arrows f
⊢ x✝¹.arrows f
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
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map ((pullback.snd f₁ f₂).op ≫ (pullback.lift g₁ g₂ comm).op))) (x f₂ hf₂) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)

Tactic:
← op_comp,

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map (pullback.lift g₁ g₂ comm ≫ pullback.snd f₁ f₂).op)) (x f₂ hf₂) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ 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
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ (ofObjects Y X).arrows g

Tactic:
rw [mem_ofArrows_iff] at hg

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
g : W ⟶ X
hg : ∃ i a, g = a ≫ f i
⊢ (ofObjects Y X).arrows g
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
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map (f₁.op ≫ g₁.op))) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)

Tactic:
← op_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map (g₁ ≫ f₁).op)) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map ((↑fg.1.snd).op ≫ (pullback.fst ↑fg.1.snd ↑fg.2.snd).op))).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝

Tactic:
← op_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd ≫ ↑fg.1.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝