mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝⁶ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasWeakSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝³ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
⊢ Epi ((F.obj M).freeHomEquiv.symm ((F.obj M).freeHomEquiv (G.mapFreeHom F η)))

Tactic:
simp only [mapFreeHom, Equiv.symm_apply_apply, epi_comp_iff_of_epi]

Goal state after:
C : Type u'
inst✝⁶ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasWeakSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝³ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
⊢ Epi (F.map G.π)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
x✝² : Sheaf J (Type u_1)
Z : Over X
x✝¹ : Presieve Z
x✝ : Presieve.FamilyOfElements ((Over.forget X).op ⋙ x✝².obj) x✝¹
hx : x✝.Compatible
Y₁ Y₂ : Over X
W : C
f₁ : W ⟶ (Over.forget X).obj Y₁
f₂ : W ⟶ (Over.forget X).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝¹ g₁
hg₂ : x✝¹ g₂
h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂
⊢ (ConcreteCategory.hom (x✝².obj.map f₁.op)) (x✝ g₁ hg₁) = (ConcreteCategory.hom (x✝².obj.map f₂.op)) (x✝ g₂ hg₂)

Tactic:
let W' : Over X := Over.mk (f₁ ≫ Y₁.hom)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
x✝² : Sheaf J (Type u_1)
Z : Over X
x✝¹ : Presieve Z
x✝ : Presieve.FamilyOfElements ((Over.forget X).op ⋙ x✝².obj) x✝¹
hx : x✝.Compatible
Y₁ Y₂ : Over X
W : C
f₁ : W ⟶ (Over.forget X).obj Y₁
f₂ : W ⟶ (Over.forget X).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝¹ g₁
hg₂ : x✝¹ g₂
h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂
W' : Over X := Over.mk (f₁ ≫ Y₁.hom)
⊢ (ConcreteCategory.hom (x✝².obj.map f₁.op)) (x✝ g₁ hg₁) = (ConcreteCategory.hom (x✝².obj.map f₂.op)) (x✝ g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
let g₁' : W' ⟶ Y₁ := Over.homMk f₁.left

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : f = 0
⊢ False

Tactic:
← Subobject.mk_eq_bot_iff_zero

Goal state after:
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : mk f = ⊥
⊢ False
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
y : T
hy : y ∈ Y
⊢ ∃ U f_1, (Sieve.pullback f S).arrows f_1 ∧ y ∈ U

Tactic:
by
    rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩
    refine ⟨U ⊓ Y, homOfLE inf_le_right, ?_, hU, hy⟩
    apply S.downward_closed hg (homOfLE inf_le_left)

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
⊢ (grothendieckTopology T).CoversTop U ↔ IsOpenCover U

Tactic:
by
  rw [GrothendieckTopology.coversTop_iff_of_isTerminal _ ⊤ isTerminalTop]
  dsimp [Opens.grothendieckTopology]
  simp only [IsOpenCover, eq_top_iff, SetLike.le_def, exists_and_right, Opens.mem_top,
    Opens.mem_iSup, forall_const]
  refine ⟨fun h x ↦ ?_, fun hU x hx ↦ ?_⟩
  · obtain ⟨V, ⟨u, ⟨i, ⟨hi⟩⟩⟩, hx⟩ := h x trivial
    use i, leOfHom hi hx
  · obtain ⟨i, hi⟩ := hU (x := x)
    exact ⟨U i, ⟨homOfLE le_top, ⟨i, ⟨𝟙 _⟩⟩⟩, hi⟩

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

Goal state before:
pp: case refine_1
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ Sieve.generate (Presieve.ofArrows V fun x ↦ homOfLE ⋯) ∈ (Opens.grothendieckTopology ↑X) (unop U)

pp: case refine_2
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ ∀ ⦃Y : Opens ↑X⦄ ⦃f : Y ⟶ unop U⦄,
    Presieve.ofArrows V (fun x ↦ homOfLE ⋯) f →
      (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) s = (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) t

Tactic:
· exact fun x hx ↦ ⟨V ⟨x, hx⟩, homOfLE (hV _), Sieve.ofArrows_mk _ _ _, hxV _⟩

Goal state after:
case refine_2
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ ∀ ⦃Y : Opens ↑X⦄ ⦃f : Y ⟶ unop U⦄,
    Presieve.ofArrows V (fun x ↦ homOfLE ⋯) f →
      (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) s = (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) t
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
⊢ ((pullback C f).map u).app (op U) ≫
      (Limits.IsColimit.coconePointUniqueUpToIso
          ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
          (Limits.colimitOfDiagramTerminal
            { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢))).hom =
    (Limits.IsColimit.coconePointUniqueUpToIso
          ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
          (Limits.colimitOfDiagramTerminal
            { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))).hom ≫
      u.app (op (hf.functor.obj U))

Tactic:
refine ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U)).hom_ext
    (fun j ↦ ?_)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) ≫
        (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
            (Limits.colimitOfDiagramTerminal
              { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢))).hom =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (Limits.colimitOfDiagramTerminal
              { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))).hom ≫
        u.app (op (hf.functor.obj U))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X)) =
    (RingCat.Hom.hom (φ.hom.app U)).comp (RingCat.Hom.hom (S.obj.map (hX.to U)))

Tactic:
← RingCat.hom_comp,

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app X ≫ R.obj.map (hX'.to (F.op.obj U))) =
    (RingCat.Hom.hom (φ.hom.app U)).comp (RingCat.Hom.hom (S.obj.map (hX.to U)))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app X ≫ R.obj.map (hX'.to (F.op.obj U))) =
    (RingCat.Hom.hom (φ.hom.app U)).comp (RingCat.Hom.hom (S.obj.map (hX.to U)))

Tactic:
← RingCat.hom_comp,

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app X ≫ R.obj.map (hX'.to (F.op.obj U))) = RingCat.Hom.hom (S.obj.map (hX.to U) ≫ φ.hom.app U)
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
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ ∀ (j : WalkingParallelPair),
    ((Cocone.precompose
                    (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                        ⋯).inv).obj
                (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose
                    (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                        ⋯).inv).obj
                (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
      (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app j

Tactic:
by rintro (_ | _)
      <;> simp [Presentation.mapRelations, GeneratingSections.mapFreeHom, ← Functor.map_comp]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
e : M
⊢ (c.smulRight (x + y)) e = (c.smulRight x + c.smulRight y) e

Tactic:
apply smul_add (c e)

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

Goal state before:
pp: κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
hs : Cardinal.mk ι < κ
⊢ ∃ j, ∀ (k : ι), f k ≤ j

Tactic:
by
    have h : Function.Surjective (fun i ↦ (⟨f i, i, rfl⟩ : Set.range f)) := fun _ ↦ by aesop
    contrapose! hs
    rw [← hκ.out.cof_ord, ← Ordinal.cof_toType]
    refine (Order.cof_le fun j ↦ ?_).trans (Cardinal.mk_le_of_surjective h)
    obtain ⟨k, hk⟩ := hs j
    exact ⟨_, Set.mem_range_self k, hk.le⟩

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

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
i : ι
⊢ f i ≫ a ≫ F.map d = f i₀ ≫ a ≫ F.map d

Tactic:
← hn (i₀, i),

Goal state after:
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
i : ι
⊢ f i ≫ a ≫ F.map (b (i₀, i) ≫ c (i₀, i)) = f i₀ ≫ a ≫ F.map (b (i₀, i) ≫ c (i₀, i))
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ m = Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯

Tactic:
ext1
      apply PullbackCone.IsLimit.hom_ext hc
      · simpa using! congr(($e₁).left)
      · simpa using! congr(($e₂).left)

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
r : S
x : M
⊢ { toFun := fun a ↦ ⟨(r • x) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id S) r • { toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext
    simp [smul_tmul']

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

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L
⊢ ∀ x ∈ (Subalgebra.map f S.toSubalgebra).carrier, x⁻¹ ∈ (Subalgebra.map f S.toSubalgebra).carrier

Tactic:
by
    rintro _ ⟨x, hx, rfl⟩
    exact ⟨x⁻¹, S.inv_mem hx, map_inv₀ f x⟩

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
E : IntermediateField K ↥F
⊢ lift E ≤ F

Tactic:
rintro _ ⟨x, _, rfl⟩
  exact x.2

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : p = 0
⊢ P

Tactic:
rw [h] at p_charP

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R 0
h : p = 0
⊢ P
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (k % z).toNat < z.natAbs

Tactic:
← Int.ofNat_lt,

Goal state after:
case mp.refine_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ ↑(k % z).toNat < ↑z.natAbs
Module: Mathlib.Algebra.CharZero.Quotient

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

Tactic:
rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),
    Int.cast_natCast]

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
⊢ f (iterate f (f a) n) = f (f (iterate f a n))

Tactic:
exact congrArg f ih

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

Goal state before:
pp: case bisim
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
⊢ t₁.head = t₂.head ∧ ∃ s s', s.val = t₁.tail ∧ s'.val = t₂.tail ∧ R s s'

Tactic:
match t₁, t₂, e with
    | _, _, ⟨s, s', rfl, rfl, r⟩ =>
      suffices head s = head s' ∧ R (tail s) (tail s') from
        And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this
      have h := bisim r; revert r h
      refine recOn s ?_ ?_ <;> intro r' <;> refine recOn s' ?_ ?_ <;> intro a' r h
      · constructor <;> dsimp at h
        · rw [h]
        · rw [h] at r
          rw [tail_pure, tail_pure, h]
          assumption
      · rw [destruct_pure, destruct_think] at h
        exact False.elim h
      · rw [destruct_pure, destruct_think] at h
        exact False.elim h
      · simp_all

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a ++ₛ drop n a).get m

Tactic:
get_append_left

Goal state after:
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = (take n a)[m]

case h
α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ m < (take n a).length
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (x ++ₛ a).get i✝ = x[i✝]

Tactic:
get_append_left

Goal state after:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ x[i✝] = x[i✝]

case h
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ i✝ < x.length
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 : Int.fract v ≠ 0
⊢ (IntFractPair.of v).fr = Int.fract v

Tactic:
simp [IntFractPair.of]

Goal state after: