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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
⊢ (ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
      ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁))) =
    (ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
      ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)))

Tactic:
refine IsLocallyFull.ext G _ (G.map iVW ≫ i ≫ f₂) fun V₂ iV₂V₁ iV₂Y₂ e₂ ↦ ?_

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
⊢ (ConcreteCategory.hom (ℱ.obj.map (G.map iV₂V₁).op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
        ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁)))) =
    (ConcreteCategory.hom (ℱ.obj.map (G.map iV₂V₁).op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
        ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂))))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
Z : D
U : C
iUY : U ⟶ Y
iZU : Z ⟶ G.obj U
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S)) ∈ K (G.obj U)

Tactic:
clear iZU Z

Goal state after:
case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S)) ∈ K (G.obj U)
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝ : Category.{v₃, u₃} A
⊢ IsDenseSubsite J (e.inverse.inducedTopology J) e.functor

Tactic:
have : J = e.functor.inducedTopology (e.inverse.inducedTopology J) := by
    ext
    simp [mem_inducedTopology_iff_of_isCoverDense, mem_inducedTopology_iff_of_isCoverDense,
      Sieve.functorPushforward_equivalence_eq_pullback]
  nth_rw 1 [this]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj

Tactic:
W_eq_isLocal_range_sheafToPresheaf_obj,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj) =
    ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ ((E.map (Over.forget X)).map F).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂) ∈ K W.left

Tactic:
exact E'.mem₁ _ _ _ _ congr($(w).left)

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

Goal state before:
pp: case refine_1.top
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve Y
X✝ : C
s : X✝ ⟶ X
⊢ (Sieve.overEquiv { left := X✝, right := right, hom := s }).symm ⊤ ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := X✝, right := right, hom := s }

Tactic:
| top =>

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
x : ↑Y
hx : x ∈ V
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' ↑V ∪ ⇑(ConcreteCategory.hom f) ⁻¹' t = ⇑(ConcreteCategory.hom f) ⁻¹' t

Tactic:
Set.union_eq_right

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
x : ↑Y
hx : x ∈ V
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' ↑V ⊆ ⇑(ConcreteCategory.hom f) ⁻¹' t
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x : ↑X
hx : x ∈ ↑((map f).obj U)
⊢ (ConcreteCategory.hom f) x ∈ ↑(hf.functor.obj ⊤ ⊓ U)

Tactic:
exact ⟨⟨x, trivial, rfl⟩, hx⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.adjunction.counit.app (⋯.functor.obj V) = eqToHom ⋯

Tactic:
by
  subsingleton

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 𝒥₁ 𝒥₂
  exact { has_limit := fun F => HasLimit.mk (finiteLimitCone F) }

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
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
Y : D
⊢ Sieve.functorPullback G (Sieve.ofObjects P.X (G.obj Y)) ≤ Sieve.ofObjects (fun i ↦ i.fst) Y

Tactic:
intro Z g ⟨i, ⟨v⟩⟩

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
Y Z : D
g : Z ⟶ Y
i : P.I
v : G.obj Z ⟶ P.X i
⊢ (Sieve.ofObjects (fun i ↦ i.fst) Y).arrows g
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
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)
⊢ (((SheafOfModules.pushforward φ).obj M).over i.fst).Presentation

Tactic:
letI overS : SheafOfModules.{u} S ⥤ SheafOfModules.{u} (S.over i.1) :=
      SheafOfModules.pushforward (𝟙 _)
    letI G' := Over.post (X := i.1) G ⋙ Over.map i.2.2
    letI ψ : S.over i.1 ⟶
        (G'.sheafPushforwardContinuous RingCat.{u} (K.over i.1) (J.over (P.X i.2.1))).obj
          (R.over (P.X i.2.1)) :=
      ((Over.forget i.1).sheafPushforwardContinuous RingCat.{u} (K.over i.1) K).map φ
    letI e : (SheafOfModules.pushforward ψ).obj (unit (R.over (P.X i.snd.fst))) ≅
      unit (S.over i.fst) := overS.mapIso η
    haveI : PreservesColimitsOfSize.{u, u, _} (SheafOfModules.pushforward ψ) := h _ _ _
    exact (P.presentation i.2.1).map (SheafOfModules.pushforward ψ) e.symm

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ F.obj.map (homOfLE ⋯).op = s.fst

Tactic:
rw [interUnionPullbackConeLift, Category.assoc, ← F.1.map_comp]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 ↦
                Opposite.casesOn X_1 fun unop ↦
                  Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 ↦
                    ULift.casesOn a fun down ↦
                      WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
              naturality := ⋯ } } ≫
      F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    s.fst
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ F.obj.map (homOfLE ⋯).op = s.snd

Tactic:
rw [interUnionPullbackConeLift, Category.assoc, ← F.1.map_comp]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ ⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 ↦
                Opposite.casesOn X_1 fun unop ↦
                  Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 ↦
                    ULift.casesOn a fun down ↦
                      WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op),
              naturality := ⋯ } } ≫
      F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    s.snd
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:
by
    dsimp
    ext <;> simp [smul_apply]

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.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
⊢ IsIso (F.map φ)

Tactic:
have := h ι
  have := h (ι ≫ φ)
  exact IsIso.of_isIso_fac_left (F.map_comp ι φ).symm

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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
by
  obtain ⟨s, γ, δ, h₁, h₂⟩ := IsFiltered.bowtie
    (IsFiltered.leftToMax i₀ j) β (IsFiltered.rightToMax i₀ j) α
  dsimp [coconeιApp]
  rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_id_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    τ

Tactic:
grw [← hτ₃, ← coinduced_mono (continuous_iff_coinduced_le.mp f.hom.2)]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun
      (TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str) ≤
    TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) (TopologicalSpace.coinduced (TopCat.Hom.hom f).toFun X.str)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ IsFiltered J

Tactic:
rw [IsFiltered.iff_cocone_nonempty.{w}]
  intro A _ _ F
  have hA : HasCardinalLT (Arrow A) κ := by
    refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le
    simp only [hasCardinalLT_aleph0_iff]
    infer_instance
  exact ⟨cocone F hA⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
this :
  (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
      (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0 ↔
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
        (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
⊢ (ConcreteCategory.hom (π ≫ g)) ↑r = 0

Tactic:
simp [show π r = 0 from hs.le (Ideal.subset_span r.2)]

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

Goal state before:
pp: 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_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
⊢ Exact ⇑F ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)

Tactic:
have H₁ : ∀ x, f₂ (σ x) = x := congr_fun hσ

Goal state after:
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_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
⊢ Exact ⇑F ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)
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 : C₁
⊢ x ∈ Set.range ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) → G x = 0

Tactic:
rintro ⟨x, rfl⟩
    simp only [δ, coe_mk, AddHom.coe_mk]
    rw [← G.comp_apply, hF, π₂.comp_apply, H₂, hπ₂.apply_apply_eq_zero]

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

Goal state before:
pp: α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ x = y

Tactic:
by rw [← get_zero_cons x s, h, get_zero_cons]

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

Goal state before:
pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

Tactic:
apply Subtype.ext
    funext n
    induction n with
    | zero => injection h with h'; rwa [h'] at f0
    | succ n IH => exact s.2 IH

Goal state after: