mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_2
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
hy : y.Compatible
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
hR2 : R.FactorsThruAlong S g
⊢ (ConcreteCategory.hom (P.map g.op)) z = x g hg

Tactic:
choose WW ii ee hh1 hh2 using hR2

Goal state after:
case refine_2
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
hy : y.Compatible
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C
ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a
ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X
hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)
hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g
⊢ (ConcreteCategory.hom (P.map g.op)) z = x g hg
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
intro H X S hS
    simpa [← Presieve.isSheafFor_iff_generate] using H (f := 𝟙 X) S hS

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

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
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
⊢ toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom =
    G.op.whiskerLeft (toSheafify K F)

Tactic:
change adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
    (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) =
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
⊢ adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
      (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) =
    ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K✝ : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K✝ B
c : Cone (F ⋙ proj K✝ B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
⊢ m.left = (homMk (t.lift ((proj K✝ B).mapCone s)) ⋯).left

Tactic:
apply t.hom_ext

Goal state after:
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K✝ : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K✝ B
c : Cone (F ⋙ proj K✝ B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
⊢ ∀ (j : J), m.left ≫ c.π.app j = (homMk (t.lift ((proj K✝ B).mapCone s)) ⋯).left ≫ c.π.app j
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
this : IsIso (cokernel.π f)
⊢ False

Tactic:
exact w (eq_zero_of_mono_cokernel f)

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ ∀ (J : Type) [𝒥 : SmallCategory J] [FinCategory J], HasLimitsOfShape J α

Tactic:
intro J 𝒥₁ 𝒥₂

Goal state after:
α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasLimitsOfShape J α
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ ∀ (J : Type) [𝒥 : SmallCategory J] [FinCategory J], HasColimitsOfShape J α

Tactic:
intro J 𝒥₁ 𝒥₂

Goal state after:
α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasColimitsOfShape J α
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯) ≫ (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j =
    (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app j

Tactic:
by
        dsimp
        rw [← F.map_comp]
        congr 1

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯) ≫
      (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app
        j =
    (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j

Tactic:
by
        dsimp
        rw [← F.map_comp]
        congr 1

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
X✝ Y✝ : SheafOfModules R
e : X✝ ≅ Y✝
σ : X✝.QuasicoherentData
hσ : σ.IsFinitePresentation
⊢ isFinitePresentation R Y✝

Tactic:
exact ⟨σ.ofIsIso e.hom, inferInstance⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app (op U)))

Tactic:
conv at hsurj =>
    enter [t]
    rw [Subtype.forall' (p := (· ∈ U))]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app (op U)))
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (r • a).1.coprod (r • a).2 = (RingHom.id S) r • a.1.coprod a.2

Tactic:
dsimp
    ext <;> simp [smul_apply]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : Semigrp} {Y : MonCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ MonCat Semigrp).obj Y),
    (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f ≫ g) =
      adjoinOne.map f ≫
        (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g

Tactic:
by
        intros
        ext ⟨_ | _⟩ <;> simp <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

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
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j

Tactic:
rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
D : J ⥤ C
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
f : c.pt ⟶ X
⊢ ∃ j p, c.π.app j ≫ p = f

Tactic:
by
  obtain ⟨j, p, hp⟩ := Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (yoneda.obj X) hc.op) f
  exact ⟨j.unop, p, hp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
l : J
hl : ∀ (i : ι), Nonempty (k i ⟶ l)
a : (i : ι) → k i ⟶ l := fun i ↦ ⋯.some
m : J
b : l ⟶ m
c : j ⟶ m
hm : ∀ (i : ι), (f i ≫ a i) ≫ b = c
⊢ ∃ m a b, ∀ (i : ι), f i ≫ a i = b

Tactic:
exact ⟨m, fun i ↦ a i ≫ b, c, by grind⟩

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
⊢ (π₂ ∘ₗ g₁) (ρ (i₂ (σ (ι₃ x)))) = 0

Tactic:
π₂.comp_apply,

Goal state after:
case mpr
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
⊢ π₂ (g₁ (ρ (i₂ (σ (ι₃ x))))) = 0
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝³ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝² : Q.IsMultiplicative
X Y Z : T
inst✝¹ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
inst✝ : Q.RespectsIso
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) mapComp._auto_1
⊢ P fg

Tactic:
subst hfg; exact P.comp_mem f g hf hg

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Module S M
inst✝⁷ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
f✝ g : N →ₗ[R] P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ (lTensor A f).ker = (lTensor A f.ker.subtype).range

Tactic:
rw [LinearMap.exact_iff.mp (lTensor_exact _ (LinearMap.exact_subtype_ker_map _) hf)]

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) → ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
intro g
    rcases g with ⟨I, ⟨hI_not_top, _⟩⟩
    -- Krull's Thm: There exists a prime ideal `M` such that `I ≤ M`.
    rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
    use M
    constructor
    · exact hM_max
    · cases CharP.exists (R ⧸ M) with
      | intro r hr =>
        convert! hr
        have r_dvd_p : r ∣ p := by
          rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
          convert! congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
        symm
        apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
        exact CharP.char_ne_one (R ⧸ M) r

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
⊢ x ∈ F

Tactic:
let y : E := ⟨x, lift_le (restrict h) hx⟩

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
y : ↥E := ⟨x, ⋯⟩
⊢ x ∈ F
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p

Tactic:
simp_rw [AddSubgroup.mem_zmultiples_iff, div_eq_mul_inv, ← smul_mul_assoc, eq_sub_iff_add_eq]

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Tactic:
let t := tail s₁ ⋈ tail s₂
  change s₁ ⋈ s₂ = head s₁::head s₂::t
  unfold interleave; unfold corecOn; rw [corec_eq]; dsimp; rw [corec_eq]; rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case h
α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a ++ₛ drop (m + n) a = take m a ++ take n (drop m a) ++ₛ drop n (drop m a)

Tactic:
simp [-drop_drop]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case hl
α : Type u
m n : ℕ
a : Stream' α
⊢ (take (m + n) a).length = (take m a ++ take n (drop m a)).length

Tactic:
simp [-drop_drop]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : take m a <+: take n a
⊢ m ≤ n

Tactic:
by simpa using h.length_le

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x ∈
    match (cons y s.tail).destruct with
    | none => []
    | some (x, r) => x :: take (k + 1 + l) r

Tactic:
simp only [destruct_cons, List.mem_cons]

Goal state after:
case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x = y ∨ x ∈ take (k + 1 + l) s.tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ ↑(s.toList h) = s

Tactic:
by
  ext n; simp [ofList]

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
x' y' : FreeCommRing ((i : ι) × G i)
i : ι
x : G i
hx :
  (of G f i) x =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      x'
j : ι
y : G j
hy :
  (of G f j) y =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      y'
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of G f k) (f i k hik x * f j k hjk y) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (x' * y')

Tactic:
by rw [map_mul, of_f, of_f, hx, hy]; rfl

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb
h : LiftRelAux R C ca'.think.destruct cb.destruct
⊢ LiftRel R ca'.think cb

Tactic:
simp only [liftRel_think_left]

Goal state after:
case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb
h : LiftRelAux R C ca'.think.destruct cb.destruct
⊢ LiftRel R ca' cb
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (of v).s.head = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
change (of v).s.get? 0 = _

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (of v).s.get? 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }