mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op ≫
        (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (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 V)).ι.app
        j ≫
      (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V))
            (colimitOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ))).hom ≫
        ℱ.map (IsOpenMap.functorMap HU HV le).op

Tactic:
rw [Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, reassoc_of% eq,
    Limits.IsColimit.comp_coconePointUniqueUpToIso_hom,
    Limits.coconeOfDiagramTerminal_ι_app, Limits.coconeOfDiagramTerminal_ι_app]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)
⊢ (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ).map
      (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
        ((CostructuredArrow.map (homOfLE le).op).obj j)) =
    (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ).map
        (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ } j) ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ (Opens.grothendieckTopology ↑X) U

Tactic:
intro U x hx

Goal state after:
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_1.refine_2
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
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj.map f ≫
        ((ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to Y))) (RingCat.Hom.hom (φ.hom.app Y))
                ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj Y)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj Y)).symm ≪≫
            (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                  (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj Y))))).app
              (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj Y)).hom =
      ((ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to X_1))) (RingCat.Hom.hom (φ.hom.app X_1))
                ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj X_1)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj X_1)).symm ≪≫
            (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                  (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj X_1))))).app
              (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj X_1)).hom ≫
        ((forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
                    sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                      F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).obj
                M).obj.map
          f

Tactic:
· cat_disch

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

Goal state before:
pp: case refine_2
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)
⊢ ∀ {X_1 Y : SheafOfModules R} (f : X_1 ⟶ Y),
    (pushforward φ ⋙ forgetToSheafModuleCat S X hX).map f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj U))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj U))
              ⋯)).hom ≫
        (forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
              sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).map
          f

Tactic:
· cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
x✝ : ι
⊢ (ConcreteCategory.hom (G.obj.map (leSupr U x✝).op)) ((ConcreteCategory.hom (f.hom.app (op (iSup U)))) s) =
    (ConcreteCategory.hom (G.obj.map (leSupr U x✝).op)) ((ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t)

Tactic:
← NatTrans.naturality_apply,

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
x✝ : ι
⊢ (ConcreteCategory.hom (f.hom.app (op (U x✝)))) ((ConcreteCategory.hom (F.obj.map (leSupr U x✝).op)) s) =
    (ConcreteCategory.hom (G.obj.map (leSupr U x✝).op)) ((ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
⊢ CategoryWithHomology (TopModuleCat R)

Tactic:
constructor
  intro S
  let D₁ : S.LeftHomologyData := ⟨_, _, _, _, _, isLimitKer _, by simp, isColimitCoker _⟩
  let D₂ : S.RightHomologyData := ⟨_, _, _, _, by simp, isColimitCoker _, _, isLimitKer _⟩
  let F := ShortComplex.leftRightHomologyComparison' D₁ D₂
  suffices IsIso F from ⟨⟨.ofIsIsoLeftRightHomologyComparison' D₁ D₂⟩⟩
  have hF : Function.Bijective F := by
    change Function.Bijective ((forget₂ _ (ModuleCat R)).map F)
    rw [← ConcreteCategory.isIso_iff_bijective, ShortComplex.map_leftRightHomologyComparison']
    infer_instance
  have hF' : Topology.IsEmbedding F := by
    refine .of_comp F.1.2 D₂.ι.1.2 ?_
    -- `isEmbedding_of_isOpenQuotientMap_of_isInducing` is the key lemma that shows the two
    -- definitions of homology give the same topology.
    refine isEmbedding_of_isOpenQuotientMap_of_isInducing
      D₁.i (F ≫ D₂.ι) D₁.π D₂.p ?_ .subtypeVal
      (Submodule.isOpenQuotientMap_mkQ _).isQuotientMap
      (Submodule.isOpenQuotientMap_mkQ _)
      (Subtype.val_injective.comp hF.1) ?_
    · rw [← ContinuousLinearMap.coe_comp, ← ContinuousLinearMap.coe_comp,
        ← hom_comp, ← hom_comp, ShortComplex.π_leftRightHomologyComparison'_ι]
    · suffices ∀ x y, S.g y = 0 → D₂.p y = D₂.p x → S.g x = 0 by
        simpa [Set.subset_def, D₁, kerι_apply S.g] using this
      intro x y hy e
      obtain ⟨z, hz⟩ := (Submodule.Quotient.eq _).mp e
      obtain rfl := eq_sub_iff_add_eq.mp hz
      simpa [show S.g (S.f z) = 0 from ConcreteCategory.congr_hom S.zero z] using hy
  rw [← isIso_iff_of_reflects_iso _ (forget₂ (TopModuleCat R) TopCat),
    TopCat.isIso_iff_isHomeomorph, isHomeomorph_iff_isEmbedding_surjective]
  exact ⟨hF', hF.2⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
⊢ ({eqToHom ⋯ ≫ Hom.fst b} + {eqToHom ⋯ ≫ Hom.snd b}).Nodup

Tactic:
simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
          let f : ((left a : WalkingMulticospan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False
          apply ne_of_apply_ne f
          conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]
          conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]
          simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (Under.forget X)

Tactic:
refine ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
  obtain i := Nonempty.some ((inferInstance : Nonempty J))
  let s' : Cocone F := ⟨Under.mk ((F.obj i).hom ≫ s.ι.app i), fun j ↦ Under.homMk (s.ι.app j) (by
    obtain ⟨k, hik, hjk, -⟩ := IsFilteredOrEmpty.cocone_objs i j
    simp only [Functor.const_obj_obj, Under.mk_right, Under.mk_hom,
      ← s.w hjk, ← s.w hik]
    simp), fun j k e ↦ by ext; simpa using s.w e⟩
  refine ⟨(hc.desc s').right, fun j ↦ congr($(hc.fac s' j).right), fun f hf ↦ ?_⟩
  dsimp at hf
  exact congr($(hc.uniq s' (Under.homMk f (by simp [s', ← hf]))
    fun j ↦ Under.UnderMorphism.ext (hf j)).right)

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
⊢ ∃ j u v, f₁ ≫ F.map u = f₂ ≫ F.map v

Tactic:
by
  have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
  have := isFiltered_of_isCardinalFiltered J κ
  exact exists_eq_of_preservesColimit_coyoneda hc f₁ f₂ hf

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

Goal state before:
pp: case mp
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
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ (ι₃ ∘ₗ F) k = ι₃ x

Tactic:
← hF,

Goal state after:
case mp
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
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ (f₂ ∘ₗ ι₂) k = ι₃ x
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * ↑(ringChar R) = 1
⊢ IsUnit ↑p

Tactic:
hch,

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * 0 = 1
⊢ IsUnit ↑p
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 M
x : ↥(((AlgebraTensorModule.lTensor S M) f).eqLocus ((AlgebraTensorModule.lTensor S M) g))
⊢ ((AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype) ((tensorEqLocusInv S M f g) x) = ↑x

Tactic:
simp [LinearMap.tensorEqLocusInv]

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

Goal state before:
pp: F : Type u_4
inst✝⁴ : Field F
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).range = Subalgebra.map f L.toSubalgebra

Tactic:
AlgHom.range_comp,

Goal state after:
F : Type u_4
inst✝⁴ : Field F
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ Subalgebra.map f L.val.range = Subalgebra.map f L.toSubalgebra
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n : ℕ
h : (fun b ↦ a = b) ((b :: s).get n)
⊢ a = b ∨ a ∈ s

Tactic:
by
  rcases n with - | n'
  · left
    exact h
  · right
    rw [get_succ, tail_cons] at h
    exact ⟨n', h⟩

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

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

Tactic:
cases f0 : s.1 0 <;> intro h

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

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
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ IsBisimulation fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s

Tactic:
intro s1 s2 h

Goal state after:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct

Tactic:
rcases h with ⟨s, h1, h2⟩

Goal state after:
α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ (cons x s).Terminates ↔ s.Terminates

Tactic:
constructor <;> intro ⟨n, h⟩

Goal state after:
case mp
α : Type u
x : α
s : Seq α
n : ℕ
h : (cons x s).TerminatedAt n
⊢ s.Terminates

case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ List.map f (take n a) = take n (map f a)

Tactic:
by
  apply List.ext_getElem <;> simp

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

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

Tactic:
by
  apply List.ext_getElem <;> simp

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ (cons x s).length' = s.length' + 1

Tactic:
by_cases h : (cons x s).Terminates <;> have h' := h <;> rw [terminates_cons_iff] at h'

Goal state after:
case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
h' : s.Terminates
⊢ (cons x s).length' = s.length' + 1

case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case r
α : Type u
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)

Tactic:
· exact ⟨s, t, u, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ IsBisimulation fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)

Tactic:
intro s1 s2 h

Goal state after:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1.destruct
    s2.destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, nil) S).join.destruct (cons a (nil.append S.join)).destruct

Tactic:
simp [join_cons_nil]

Goal state after: