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

Goal state before:
pp: 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
⊢ s = t

Tactic:
have := (isSheaf_iff_isSheaf_of_type _ _).mp
    ((Presheaf.isSheaf_iff_isSheaf_forget (C := Opens X) (A' := A) _ F (forget _)).mp hF)

Goal state after:
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)
⊢ s = t
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
h : F.IsSheaf
⊢ Nonempty (IsLimit (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U (iSup U))).arrows.cocone.op))

Tactic:
apply (Presheaf.isSheaf_iff_isLimit _ _).mp h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
h : F.IsSheaf
⊢ Sieve.generate (presieveOfCoveringAux U (iSup U)) ∈ (Opens.grothendieckTopology ↑X) (iSup U)
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
i : U ⟶ V
⊢ F.map ((OpenNhds.inclusion y).map i.unop).op ≫ colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop V), ⋯⟩) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop U), ⋯⟩) ≫ 𝟙 (F.stalk x)

Tactic:
Category.comp_id

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
i : U ⟶ V
⊢ F.map ((OpenNhds.inclusion y).map i.unop).op ≫ colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop V), ⋯⟩) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop U), ⋯⟩)
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
⊢ Dense ↑s ↔ s.topologicalClosure = ⊤

Tactic:
rw [← SetLike.coe_set_eq, dense_iff_closure_eq]

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
⊢ closure[inst✝⁴] ↑s = Set.univ ↔ ↑s.topologicalClosure = ↑⊤
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ s.topologicalClosure = s → IsClosed[inst✝⁴] ↑s

Tactic:
exact fun h ↦ h ▸ isClosed_closure

Goal state after:
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)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.obj V sf
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t

Tactic:
· use s
      apply G.eq_of_locally_eq' V U iVU V_cover
      intro x
      rw [← ConcreteCategory.comp_apply, ← f.1.naturality, ConcreteCategory.comp_apply, s_spec, heq]

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)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ 1 •
      Quot.mk (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
        ⟨V, b⟩ =
    Quot.mk (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
      ⟨V, b⟩

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (rightToMax _ _) ?_

Goal state after:
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)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map (𝟙 (IsFiltered.max ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst ⟨V, b⟩.fst))))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst ⟨V, b⟩.fst)))
          ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map (rightToMax ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst V))) b
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
r : ↑(RingCat.FilteredColimits.colimit R)
U : C
a : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U
⊢ Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨U, a⟩ • 0 =
    0

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (rightToMax _ _) ?_

Goal state after:
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
r : ↑(RingCat.FilteredColimits.colimit R)
U : C
a : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map (𝟙 (IsFiltered.max ⟨U, a⟩.fst ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst))))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst)))
          ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map (rightToMax ⟨U, a⟩.fst ⟨⋯.some, 0⟩.fst))) ⟨⋯.some, 0⟩.snd
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_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₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective ⇑g
h : g ∘SL f₁ = g ∘SL f₂
⊢ f₁ = f₂

Tactic:
ext x
  exact hg congr($h x)

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

Goal state before:
pp: R₁ : Type u_1
inst✝³ : Semiring R₁
M₁ : Type u_4
inst✝² : TopologicalSpace M₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
T : M₁ →L[R₁] M₁
hT : IsUnit T
⊢ IsHomeomorph ⇑T

Tactic:
by
  obtain ⟨T, rfl⟩ := hT
  exact (homeomorphOfUnit T).isHomeomorph

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.mul_one
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.mul one) = descFunLift F s x

Tactic:
| mul_one x =>

Goal state after:
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))
⊢ ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
ext r

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r =
    (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case mpr
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₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ f.IsInvertible → (↑e ∘SL f).IsInvertible

Tactic:
rintro ⟨M, rfl⟩

Goal state after:
case mpr
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₃
e : M₂ ≃L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (↑e ∘SL ↑M).IsInvertible
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case mpr
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₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ f.IsInvertible → (f ∘SL ↑e).IsInvertible

Tactic:
rintro ⟨M, rfl⟩

Goal state after:
case mpr
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₃
e : M₃ ≃L[R] M✝
M : M✝ ≃L[R] M₂
⊢ (↑M ∘SL ↑e).IsInvertible
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ((if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
      if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0).Nodup

Tactic:
split_ifs with h₁ h₂

Goal state after:
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

case neg
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} + 0).Nodup

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
⊢ (0 + {eqToHom ⋯ ≫ Hom.snd b}).Nodup

case neg
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
⊢ (0 + 0).Nodup
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ((if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0) +
      if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0).Nodup

Tactic:
split_ifs with h₁ h₂

Goal state after:
case pos
J : MultispanShape
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 a = b
h₂ : J.snd a = b
⊢ ({Hom.fst a ≫ eqToHom ⋯} + {Hom.snd a ≫ eqToHom ⋯}).Nodup

case neg
J : MultispanShape
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 a = b
h₂ : ¬J.snd a = b
⊢ ({Hom.fst a ≫ eqToHom ⋯} + 0).Nodup

case pos
J : MultispanShape
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 a = b
h✝ : J.snd a = b
⊢ (0 + {Hom.snd a ≫ eqToHom ⋯}).Nodup

case neg
J : MultispanShape
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 a = b
h✝ : ¬J.snd a = b
⊢ (0 + 0).Nodup
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
⊢ f.IsInvertible

Tactic:
by
  by_contra H
  obtain ⟨_, _⟩ : Subsingleton M₂ ∧ Subsingleton M := by simpa [inverse, H] using hf
  simp_all [Subsingleton.elim f 0]

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
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 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₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ i₃ (ι₃ x) = 0

Tactic:
← i₃.comp_apply,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
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 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₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ (i₃ ∘ₗ ι₃) x = 0
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : N₁
H : G (π₁ x) = 0
y : M₂
hy : i₂ y = g₁ x
⊢ i₃ (f₂ y) = 0

Tactic:
← i₃.comp_apply,

Goal state after:
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : N₁
H : G (π₁ x) = 0
y : M₂
hy : i₂ y = g₁ x
⊢ (i₃ ∘ₗ f₂) y = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none.none.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
⊢ Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        none = a →
          none = a_1 →
            WidePullbackShape.Hom.id none ≍ x →
              (Option.rec B (fun val ↦ (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val ↦ (F.obj { as := val }).left) none))
        (fun X h ↦
          Eq.rec (motive := fun x x_1 ↦
            none = x →
              WidePullbackShape.Hom.id none ≍ 𝟙 x →
                (Option.rec B (fun val ↦ (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val ↦ (F.obj { as := val }).left) none))
            (fun h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : none ⟶ x) →
                  f ≍ 𝟙 none →
                    (Option.rec B (fun val ↦ (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) none)) ⋯
                (WidePullbackShape.Hom.id none))
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ none) →
              none = none →
                f ≍ WidePullbackShape.Hom.term j →
                  (Option.rec B (fun val ↦ (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val ↦ (F.obj { as := val }).left) none))
            (fun f h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some j ⟶ x) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ (WidePullbackShape.Hom.id none))
        (WidePullbackShape.Hom.id none) ⋯ ⋯ ⋯

Tactic:
Category.comp_id

Goal state after:
case none.none.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
⊢ Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case some.some.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        some val✝ = a →
          some val✝ = a_1 →
            WidePullbackShape.Hom.id (some val✝) ≍ x →
              (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
        (fun X h ↦
          Eq.rec (motive := fun x x_1 ↦
            some val✝ = x →
              WidePullbackShape.Hom.id (some val✝) ≍ 𝟙 x →
                (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
            (fun h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some val✝ ⟶ x) →
                  f ≍ 𝟙 (some val✝) →
                    (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝))) ⋯
                (WidePullbackShape.Hom.id (some val✝)))
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ some val✝) →
              some val✝ = none →
                f ≍ WidePullbackShape.Hom.term j →
                  (Option.rec B (fun val ↦ (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
            (fun f h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some j ⟶ x) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ (WidePullbackShape.Hom.id (some val✝)))
        (WidePullbackShape.Hom.id (some val✝)) ⋯ ⋯ ⋯

Tactic:
Category.comp_id

Goal state after:
case some.some.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝)