mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : 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 𝒜
x✝¹ x✝ : A
⊢ ↑(((decompose 𝒜) x✝¹ + (decompose 𝒜) x✝) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)

Tactic:
add_apply,

Goal state after:
ι : 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 𝒜
x✝¹ x✝ : A
⊢ ↑(((decompose 𝒜) x✝¹) 0 + ((decompose 𝒜) x✝) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)
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₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹)

Tactic:
dsimp only [Matrix.IsAdjointPair]

Goal state after:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A₂ ↔ (P * A₁ * P⁻¹)ᵀ * J = J * (P * A₂ * P⁻¹)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case cons
ι : 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
inst✝ : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih : (∀ x ∈ tail, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < tail.length • m → tail.prod n = 0
hl : ∀ x ∈ head :: tail, ∀ k < m, x k = 0
n : ι
hn : n < (head :: tail).length • m
⊢ (head :: tail).prod n = 0

Tactic:
simp only [List.mem_cons, forall_eq_or_imp, List.length_cons, List.prod_cons] at hl hn ⊢

Goal state after:
case cons
ι : 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
inst✝ : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih : (∀ x ∈ tail, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < tail.length • m → tail.prod n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, head k = 0) ∧ ∀ a ∈ tail, ∀ k < m, a k = 0
⊢ (head * tail.prod) n = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
⊢ ∀ (z : V), ∃ c, z + c • x ∈ Submodule.orthogonalBilin B (K ∙ x)

Tactic:
intro y

Goal state after:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y : V
⊢ ∃ c, y + c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ 1 ≤ evenOdd Q 0

Tactic:
refine le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)
  exact (pow_zero _).ge

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (GradedAlgebra.ι Q) m * (GradedAlgebra.ι Q) m = (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)

Tactic:
rw [GradedAlgebra.ι_apply Q, DirectSum.of_mul_of, DirectSum.algebraMap_apply]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext rfl <| ι_sq_scalar _ _)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ∀ (i : ZMod 2) (x : ↥(evenOdd Q i)),
    ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ↑x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i) x

Tactic:
by apply GradedAlgebra.lift_ι_eq Q

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

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

Tactic:
s.prop

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ 1 ≤ #↑s ↔ 1 ≤ n

Tactic:
s.prop

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ #↑s = n

Tactic:
s.prop

Goal state after:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ n = n
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
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
⊢ ExteriorAlgebra R M →ₗ[R] M

Tactic:
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
x✝ : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ x✝ = t.ι.app j
⊢ x✝ = colimitDesc F t

Tactic:
by
    ext ⟨j, x⟩
    exact (congr_hom ((forget (ModuleCat _)).congr_map (h j)) _).trans
      (congr_hom ((forget (ModuleCat _)).congr_map (ι_colimitDesc F t j)) x).symm

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 Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ x.comp ((Ext.mk₀ h.i).comp (Ext.mk₀ h.r) ⋯) ⋯ = 0

Tactic:
← Ext.comp_assoc_of_second_deg_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ (x.comp (Ext.mk₀ h.i) ⋯).comp (Ext.mk₀ h.r) ⋯ = 0
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
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (alternatingMapLinearEquiv (alternatingMapLinearEquiv.symm φ)).compAlternatingMap (ιMulti R n) =
    alternatingMapLinearEquiv.symm φ

Tactic:
dsimp [alternatingMapLinearEquiv]

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
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯).symm
          (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ)).compAlternatingMap
      (ιMulti R n) =
    ((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v', u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
⊢ injectiveDimension M = injectiveDimension N

Tactic:
by
  refine eq_of_forall_ge_iff (fun N ↦ ?_)
  induction N with
  | bot => simpa [injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e.subsingleton_congr
  | coe n =>
    induction n with
    | top => simp
    | coe n =>
      simp [injectiveDimension_le_iff, hasInjectiveDimensionLE_iff_of_semiLinearEquiv eR e n]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
this✝¹ : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
this✝ : PreservesColimits (tensorLeft F) :=
  { preservesColimitsOfShape := @instMonoidalClosedFunctorType._proof_2 C inst✝ F }
this : (tensorLeft F).IsLeftAdjoint
⊢ Closed F

Tactic:
exact Closed.mk _ (Adjunction.ofIsLeftAdjoint (tensorLeft F))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁸ : Category.{v_1, u_1} J
inst✝⁷ : Category.{v_2, u_2} C
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Category.{v_4, u_4} E
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory E
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
⊢ PreservesColimitsOfShape K (tensorLeft F)

Tactic:
apply preservesColimitsOfShape_of_evaluation

Goal state after:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁸ : Category.{v_1, u_1} J
inst✝⁷ : Category.{v_2, u_2} C
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Category.{v_4, u_4} E
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory E
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
⊢ ∀ (k : J), PreservesColimitsOfShape K (tensorLeft F ⋙ (evaluation J C).obj k)
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv =
    (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2)

Tactic:
dsimp [isoObjCoconePointsOfIsColimit, Functor.mapCocone₂]

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ c₃.ι.app j ≫ ((isColimitOfPreserves₂ G hc₁ hc₂).coconePointUniqueUpToIso hc₃).inv =
    (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (F.obj c ⟶ x✝)

Tactic:
use Classical.choice IsCofiltered.nonempty
    exact ⟨Discrete.eqToHom (by simp)⟩

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 (proj T Y) X)

Tactic:
rw [isConnected_iff_of_equivalence (ofCostructuredArrowProjEquivalence T Y X)]

Goal state after:
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)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) →
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Tactic:
rintro ⟨h, _⟩ j₂

Goal state after:
case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
⊢ ∃ j₁, j₂ ≤ f j₁
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s') →
    ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁

Tactic:
rintro ⟨h, _⟩ j₂

Goal state after:
case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'
j₂ : J₂
⊢ ∃ j₂_1, f j₂_1 ≤ j₂
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 : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
⊢ ∃ U x x', ιM x = m ∧ ιM x' = m'

Tactic:
obtain ⟨U, ⟨x, x'⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM')) ⟨m, m'⟩
  rw [Prod.ext_iff] at h
  obtain ⟨rfl, rfl⟩ := h
  exact ⟨U, x, x', rfl, rfl⟩

Goal state after:
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 : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j ≫ (R ⋙ F.partialRightAdjoint).map φ) =
    F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ F.partialRightAdjointMap (R.map φ))

Tactic:
← assoc

Goal state after:
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 : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ (R ⋙ F.partialRightAdjoint).map φ) =
    F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ F.partialRightAdjointMap (R.map φ))
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ ≫ (G₃₂.associator G₂₁ G₁₀).inv)

Tactic:
obtain ⟨τ₀₁₂, rfl⟩ := (conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)).surjective τ₀₁₂

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂)) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₂₃ ≫ G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫ (G₃₂.associator G₂₁ G₁₀).inv)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (m : ↑(M₁.obj X)) (n₁ n₂ : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (n₁ + n₂) =
      (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n₁ +
        (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n₂

Tactic:
intro m₁ m₂ m₂'
      dsimp +instances
      rw [map_add, TensorProduct.tmul_add]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ generate R ≤ S

Tactic:
rwa [generate_le_iff]

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
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible

Tactic:
intro Y₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : S.arrows f₁) (h₂ : S.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((yoneda.obj s.pt).map g₁.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ h₁) =
        (ConcreteCategory.hom ((yoneda.obj s.pt).map g₂.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows

Tactic:
intro H W x hx
    replace H := Classical.choice H
    let s := compatibleYonedaFamily_toCocone S.arrows W x hx
    use H.desc s
    constructor
    · exact fun _ f hf => (H.fac s) ⟨Over.mk f, hf⟩
    · exact fun g hg => H.uniq s g (fun ⟨⟨f, _, hom⟩, hf⟩ => hg hom hf)

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x) →
    (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x

Tactic:
intro t
    apply SecondObj.ext
    intro Y Z g f hf
    simpa [firstMap, secondMap] using t _ g hf

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows (h ≫ pullback.fst g f ≫ g)

Tactic:
← assoc

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst g f) ≫ 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
⊢ x.Compatible

Tactic:
intro Y₁

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₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : R f₁) (h₂ : R f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPushforward (𝟭 C) R = R

Tactic:
ext X f
  constructor
  · intro hf
    obtain ⟨X, g, h, hg, rfl⟩ := hf
    exact R.downward_closed hg h
  · intro hf
    exact ⟨X, f, 𝟙 _, hf, by simp⟩

Goal state after:
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
a : Presieve.FamilyOfElements P R
| (ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)

Tactic:
rw [← Iso.toEquiv_apply]

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
a : Presieve.FamilyOfElements P R
| (firstObjEqFamily P R).toEquiv ((firstObjEqFamily P R).toEquiv.symm a)