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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f

Tactic:
have hl₂ : l ≫ pullback.snd _ _ = p₂ := by simp [l]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁' i₁ i₂ = E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))

Tactic:
by
  rw [← Sieve.pullback_id (S := E.sieve₁' i₁ i₂),
    sieve₁_eq_pullback_sieve₁' _ _ _ pullback.condition]
  congr
  cat_disch

Goal state after:
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K (G.obj Z)

Tactic:
apply K.superset_covering ?_ (G.functorPushforward_imageSieve_mem _ (iZY ≫ iYX))

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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Sieve.functorPushforward G (G.imageSieve (iZY ≫ iYX)) ≤
    Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.s₁ (e.hom.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.hom_inv_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs₀ : (e.hom ≫ e.inv).s₀ = (𝟙 E).s₀
hh₀ : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (𝟙 E).h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), (e.hom ≫ e.inv).s₁ k = (congrIndexOneOfEq ⋯ ⋯) ((𝟙 E).s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).h₁ k = (𝟙 E).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 E).s₁ k)).inv ≫ eqToHom ⋯
⊢ e.inv.s₁ (e.hom.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ (proj K B).map (homMk (x✝¹.π.app x✝) ⋯) = x✝¹.π.app x✝

Tactic:
CostructuredArrow.proj_map,

Goal state after:
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ (homMk (x✝¹.π.app x✝) ⋯).left = x✝¹.π.app x✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ (𝟭 (WalkingMulticospan E.multicospanShape)).obj (WalkingMulticospan.right x✝) =
    (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).obj (WalkingMulticospan.right x✝)

Tactic:
by dsimp; congr; apply PreOneHypercover.I₁'.ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
i : WalkingMulticospan E.multicospanShape
⊢ ((Cone.postcompose
                (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                    (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
            (E.multifork G)).π.app
      i =
    (Iso.refl
          ((Cone.postcompose
                  (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                      (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
              (E.multifork G)).pt).hom ≫
      (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app i

Tactic:
induction i with

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

Goal state before:
pp: case refine_1
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
⊢ (E.map (Over.post F)).sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)

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₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
· dsimp [-Over.post_obj]
    rw [PreZeroHypercover.sieve₀_map, GrothendieckTopology.mem_over_iff,
      Sieve.functorPushforward_ofArrows, Sieve.overEquiv_ofArrows]
    exact E'.mem₀

Goal state after:
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₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this : ↑(F.sectionsPrecomp s₁) X.left = ↑(F.sectionsPrecomp s₂) X.left
⊢ ↑s₁ Y = ↑s₂ Y

Tactic:
have h₁ := s₁.property X.hom

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this : ↑(F.sectionsPrecomp s₁) X.left = ↑(F.sectionsPrecomp s₂) X.left
h₁ : (ConcreteCategory.hom (P.map X.hom)) (↑s₁ (F.obj X.left)) = ↑s₁ Y
⊢ ↑s₁ Y = ↑s₂ Y
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
⊢ ∃ a, ∀ (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = a

Tactic:
apply constant_of_preserves_morphisms'

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
⊢ ∀ (j₁ j₂ : CostructuredArrow F Y) (x : j₁ ⟶ j₂),
    (ConcreteCategory.hom (P.map j₁.hom)) (↑t j₁.left) = (ConcreteCategory.hom (P.map j₂.hom)) (↑t j₂.left)
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
⊢ ∃ a, ∀ (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = a

Tactic:
apply constant_of_preserves_morphisms'

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
⊢ ∀ (j₁ j₂ : StructuredArrow Y F) (x : j₁ ⟶ j₂),
    (F ⋙ P).ιColimitType j₁.right ∘ ⇑(ConcreteCategory.hom (P.map j₁.hom)) =
      (F ⋙ P).ιColimitType j₂.right ∘ ⇑(ConcreteCategory.hom (P.map j₂.hom))
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = ?m.15

pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.15 = Finset.univ.inf f

pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α

Tactic:
· exact
      (IsLimit.conePointUniqueUpToIso (limit.isLimit _)
          (finiteLimitCone (Discrete.functor f)).isLimit).to_eq

Goal state after:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ (finiteLimitCone (Discrete.functor f)).cone.pt = Finset.univ.inf f
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections

Tactic:
refine ⟨fun h U ↦ h.isSheafPreservesLimitPairwiseIntersections,
    fun h ↦ F.isSheaf_iff_isSheafPairwiseIntersections.mpr fun ι U ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))
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 X
U : Opens ↑Y
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ U
⊢ ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hx ≫ stalkPushforward C f F x =
    F.germ ((Opens.map f).obj U) x hx

Tactic:
by
  simp [germ, stalkPushforward]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    0 •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel a =
      0

Tactic:
rintro ⟨V, b⟩
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (leftToMax _ _) ?_
    dsimp
    simp only [map_zero, zero_smul]

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₁ M₁
inst✝⁷ : Module R₂ M₂
inst✝⁶ : RingHomSurjective σ₁₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : TopologicalSpace R₂
inst✝³ : ContinuousSMul R₁ M₁
inst✝² : ContinuousAdd M₁
inst✝¹ : ContinuousSMul R₂ M₂
inst✝ : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange ⇑f
s : Submodule R₁ M₁
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤

Tactic:
simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₁ M₁
inst✝⁷ : Module R₂ M₂
inst✝⁶ : RingHomSurjective σ₁₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : TopologicalSpace R₂
inst✝³ : ContinuousSMul R₁ M₁
inst✝² : ContinuousAdd M₁
inst✝¹ : ContinuousSMul R₂ M₂
inst✝ : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange ⇑f
s : Submodule R₁ M₁
hs : Dense ↑s
⊢ Dense ↑(Submodule.map (↑f) s)
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (algebraMap R S) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) r

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
hf : f.IsInvertible
N : M₂ ≃L[R] M₃
⊢ (↑N ∘SL f).IsInvertible

Tactic:
rcases hf with ⟨M, rfl⟩

Goal state after:
R : Type u_1
M✝ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
N : M₂ ≃L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (↑N ∘SL ↑M).IsInvertible
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₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
⊢ f.inverse = g

Tactic:
by
  have : f = ContinuousLinearEquiv.equivOfInverse' f g hf hg := rfl
  rw [this, inverse_equiv]
  rfl

Goal state after:
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₂
x : M
y : M₂
hf : f.IsInvertible
⊢ f.inverse y = x ↔ y = f x

Tactic:
rcases hf with ⟨M, rfl⟩

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₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ (↑M).inverse y = x ↔ y = ↑M x
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
v : M₃
hg : g.IsInvertible
⊢ (g ∘SL f).inverse v = f.inverse (g.inverse v)

Tactic:
simp only [hg.inverse_comp_of_left, comp_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse

Tactic:
rcases hf with ⟨M, rfl⟩

Goal state after:
R : Type u_1
M✝ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (g ∘SL ↑M).inverse = (↑M).inverse ∘SL g.inverse
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ (F.obj i).topologicalSpace ≤
    TopologicalSpace.induced (⇑(hom (c.ι.app i)))
      (TopologicalSpace.induced
        (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun s.1.topologicalSpace)

Tactic:
induced_compose,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ (F.obj i).topologicalSpace ≤
    TopologicalSpace.induced
      ((ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun ∘ ⇑(hom (c.ι.app i)))
      s.1.topologicalSpace
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j

Tactic:
IsIso.eq_inv_comp,

Goal state after:
J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ c.π.app i₀ ≫ h.coneπApp j = c.π.app j
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ s.1.topologicalSpace ≤
    TopologicalSpace.induced (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun
      (TopologicalSpace.induced (⇑(hom (c.π.app i))) (F.obj i).topologicalSpace)

Tactic:
induced_compose,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ s.1.topologicalSpace ≤
    TopologicalSpace.induced
      (⇑(hom (c.π.app i)) ∘ (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun)
      (F.obj i).topologicalSpace
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
X : StructuredArrow (L.obj Y) L
p : (MorphismProperty.structuredArrowObj L P).colimitsOfShape (Discrete PEmpty.{1}) X
⊢ MorphismProperty.structuredArrowObj L P X

Tactic:
let t : IsInitial X := (ObjectProperty.colimitsOfShape_isEmpty_iff _ _ _ |>.mp p).some

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
X : StructuredArrow (L.obj Y) L
p : (MorphismProperty.structuredArrowObj L P).colimitsOfShape (Discrete PEmpty.{1}) X
t : IsInitial X := ⋯.some
⊢ MorphismProperty.structuredArrowObj L P X
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
m : M
a : ↥(f.eqLocus g)
⊢ m ⊗ₜ[R] ↑a ∈ ((AlgebraTensorModule.lTensor S M) f).eqLocus ((AlgebraTensorModule.lTensor S M) g)

Tactic:
simp [show f a = g a from a.property]

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

Goal state before:
pp: case h.right.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p

Tactic:
convert! hr

Goal state after:
case e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ p = r
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case succ.nil
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
e : some a = ↑nil (k + 1)
⊢ C nil

Tactic:
injection e

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

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: (l₁ ++ l₂) ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)

Tactic:
cons_append_stream,

Goal state after:
α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: (l₁ ++ l₂ ++ₛ s) = a :: l₁ ++ₛ (l₂ ++ₛ s)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: (l₁ ++ l₂ ++ₛ s) = a :: l₁ ++ₛ (l₂ ++ₛ s)

Tactic:
cons_append_stream,

Goal state after:
α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: (l₁ ++ l₂ ++ₛ s) = a :: (l₁ ++ₛ (l₂ ++ₛ s))