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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ((Functor.fromPUnit V).obj { as := PUnit.unit }).obj ≤ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i i')).obj

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ V.obj ≤ U i ∧ V.obj ≤ U i'
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
V : (Opens ↑Y)ᵒᵖ
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ unop V
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F ((Opens.map f).obj (unop V)) x hx =
    F.germ (unop V) ((ConcreteCategory.hom f) x) hx

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
V : (Opens ↑Y)ᵒᵖ
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ unop V
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F ((Opens.map f).obj (unop V)) x hx =
    F.germ (unop V) ((ConcreteCategory.hom f) x) hx
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : ContinuousConstSMul R M
⊢ Continuous[inst✝³, inst✝³] fun a ↦ -a

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : ContinuousConstSMul R M
⊢ Continuous[inst✝³, inst✝³] fun a ↦ -a
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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (α.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (α.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
hW : W ∈ B
iWU₁ : W ≤ U₁
iWU₂ : W ≤ U₂
heq : (ConcreteCategory.hom (F.map (homOfLE iWU₁).op)) s = (ConcreteCategory.hom (F.map (homOfLE iWU₂).op)) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t

Tactic:
simpa using

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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (α.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (α.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
hW : W ∈ B
iWU₁ : W ≤ U₁
iWU₂ : W ≤ U₂
heq : (ConcreteCategory.hom (F.map (homOfLE iWU₁).op)) s = (ConcreteCategory.hom (F.map (homOfLE iWU₂).op)) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
c : R
hc : c ∈ {0}ᶜ
⊢ x + c • y ∈ {x}ᶜ

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
c : R
hc : c ∈ {0}ᶜ
⊢ ¬c = 0
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i)) = Set.univ.pi fun i ↦ closure[inst✝¹ i] ↑(s i)

Tactic:
← closure_pi_set

Goal state after:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i)) =
    closure[Pi.topologicalSpace] (Set.univ.pi fun i ↦ ↑(s i))
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)
⊢ IsLimit (F.interUnionPullbackCone U V)

Tactic:
let ι : ULift.{w} WalkingPair → Opens X := fun ⟨j⟩ => WalkingPair.casesOn j U V
  have hι : U ⊔ V = iSup ι := by
    ext
    rw [Opens.coe_iSup, Set.mem_iUnion]
    constructor
    · rintro (h | h)
      exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
    · rintro ⟨⟨_ | _⟩, h⟩
      exacts [Or.inl h, Or.inr h]
  apply PullbackCone.isLimitAux'
  intro s
  use interUnionPullbackConeLift F U V s
  refine ⟨?_, ?_, ?_⟩
  · apply interUnionPullbackConeLift_left
  · apply interUnionPullbackConeLift_right
  · intro m h₁ h₂
    rw [← cancel_mono (F.1.map (eqToHom hι.symm).op)]
    apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_ext
    rintro ((_ | _) | (_ | _)) <;>
    rw [Category.assoc, Category.assoc, Functor.mapCone_π_app, ← F.1.map_comp]
    · convert! h₁
      apply interUnionPullbackConeLift_left
    · convert! h₂
      apply interUnionPullbackConeLift_right
    all_goals
      dsimp only [Functor.op, Pairwise.cocone_ι_app, Functor.mapCone_π_app, Cocone.op,
        Pairwise.coconeιApp, unop_op, op_comp, NatTrans.op]
      simp_rw [F.1.map_comp, ← Category.assoc]
      congr 1
      simp_rw [Category.assoc, ← F.1.map_comp]
    · convert! h₁
      apply interUnionPullbackConeLift_left
    · convert! h₂
      apply interUnionPullbackConeLift_right

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : Nontrivial M₁
e : 0 = 1
x : M₁
hx : x ≠ 0
⊢ x = 0

Tactic:
simpa using

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : Nontrivial M₁
e : 0 = 1
x : M₁
hx : x ≠ 0
⊢ x = 0
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_9
E : Type u_10
F : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
g : F →L[R] E
hinv : g ∘SL f = ContinuousLinearMap.id R E
⊢ Function.LeftInverse ⇑g ⇑f

Tactic:
simpa using

Goal state after:
R : Type u_9
E : Type u_10
F : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
g : F →L[R] E
hinv : g ∘SL f = ContinuousLinearMap.id R E
⊢ Function.LeftInverse ⇑g ⇑f
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
R : Type u_9
inst✝⁴ : DivisionSemiring R
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R M₂
f : M₁ →L[R] R
hf : f ≠ 0
x : M₂
⊢ ↑f ≠ 0

Tactic:
simpa using

Goal state after:
M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
R : Type u_9
inst✝⁴ : DivisionSemiring R
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R M₂
f : M₁ →L[R] R
hf : f ≠ 0
x : M₂
⊢ ¬f = 0
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
n : ℕ
ihn : toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n)
⊢ toSpanSingleton R c ^ n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))

Tactic:
ihn,

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
n : ℕ
ihn : toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n)
⊢ toSpanSingleton R (c ^ n) * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
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
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
this :
  ∀ (x y : (fun X ↦ ↑X.toModuleCat) S.X₂),
    (ConcreteCategory.hom S.g) y = 0 →
      (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x → (ConcreteCategory.hom S.g) x = 0
⊢ ⇑(ConcreteCategory.hom D₂.p) ⁻¹' ⇑(ConcreteCategory.hom D₂.p) '' Set.range ⇑(ConcreteCategory.hom D₁.i) ⊆
    Set.range ⇑(ConcreteCategory.hom D₁.i)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
this :
  ∀ (x y : (fun X ↦ ↑X.toModuleCat) S.X₂),
    (ConcreteCategory.hom S.g) y = 0 →
      (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x → (ConcreteCategory.hom S.g) x = 0
⊢ ∀ (x x_1 : ↑S.X₂.toModuleCat),
    (Hom.hom S.g) x_1 = 0 → (ConcreteCategory.hom D₂.p) x_1 = (ConcreteCategory.hom D₂.p) x → (Hom.hom S.g) x = 0
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
x : ↑S.X₂.toModuleCat
z : ↑S.X₁.toModuleCat
hy : (ConcreteCategory.hom S.g) (↑(Hom.hom S.f) z + x) = 0
e : (ConcreteCategory.hom D₂.p) (↑(Hom.hom S.f) z + x) = (ConcreteCategory.hom D₂.p) x
hz : ↑(Hom.hom S.f) z = ↑(Hom.hom S.f) z + x - x
⊢ (ConcreteCategory.hom S.g) x = 0

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
x : ↑S.X₂.toModuleCat
z : ↑S.X₁.toModuleCat
hy : (ConcreteCategory.hom S.g) (↑(Hom.hom S.f) z + x) = 0
e : (ConcreteCategory.hom D₂.p) (↑(Hom.hom S.f) z + x) = (ConcreteCategory.hom D₂.p) x
hz : ↑(Hom.hom S.f) z = ↑(Hom.hom S.f) z + x - x
⊢ (ConcreteCategory.hom S.g) x = 0
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
hf : Function.Injective ⇑f
a₁ a₂ : α
H : (mapMulHom f) ↑a₁ = (mapMulHom f) ↑a₂
⊢ ↑a₁ = ↑a₂

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
hf : Function.Injective ⇑f
a₁ a₂ : α
H : (mapMulHom f) ↑a₁ = (mapMulHom f) ↑a₂
⊢ a₁ = a₂
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
hf : Function.Injective ⇑f
a₁ a₂ : α
H : (mapMulHom f) ↑a₁ = (mapMulHom f) ↑a₂
⊢ ↑a₁ = ↑a₂

Tactic:
by simpa [hf.eq_iff] using H

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
x : M₁
⊢ f₂ (f₁ x) = x

Tactic:
simpa using

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
x : M₁
⊢ f₂ (f₁ x) = x
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
x : M₂
⊢ f₁ (f₂ x) = x

Tactic:
simpa using

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
x : M₂
⊢ f₁ (f₂ x) = x
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
e : j ⟶ k
⊢ Over.Hom.left (((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).map e ≫ Over.homMk (s.π.app k) ⋯) =
    Over.Hom.left (Over.homMk (s.π.app j) ⋯ ≫ F.map e)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
e : j ⟶ k
⊢ s.π.app k = s.π.app j ≫ Over.Hom.left (F.map e)
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
e : j ⟶ k
⊢ Under.Hom.right (F.map e ≫ Under.homMk (s.ι.app k) ⋯) =
    Under.Hom.right (Under.homMk (s.ι.app j) ⋯ ≫ ((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).map e)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
e : j ⟶ k
⊢ Under.Hom.right (F.map e) ≫ s.ι.app k = s.ι.app j
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.inverse.IsInvertible
H : ¬f.IsInvertible
⊢ Subsingleton M₂ ∧ Subsingleton M

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.inverse.IsInvertible
H : ¬f.IsInvertible
⊢ Subsingleton M₂ ∧ Subsingleton M
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ'
this : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
exact F.preservesColimitsOfShape_of_isCardinalAccessible κ J

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable X κ → IsCardinalPresentable (F.obj X) κ

Tactic:
· intro
    infer_instance

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

Goal state before:
pp: T : Type u
κ : Cardinal.{w}
hT : HasCardinalLT T κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (Arrow (WalkingParallelFamily T)) κ

Tactic:
simpa using

Goal state after:
T : Type u
κ : Cardinal.{w}
hT : HasCardinalLT T κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT T κ