mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)

Tactic:
let _ := generateFrom (Ioi '' s ∪ Iio '' s)

Goal state after:
case refine_2.inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
x✝ : TopologicalSpace α := generateFrom (Ioi '' s ∪ Iio '' s)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)

Tactic:
let _ := generateFrom (Ioi '' s ∪ Iio '' s)

Goal state after:
case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
x✝ : TopologicalSpace α := generateFrom (Ioi '' s ∪ Iio '' s)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
⊢ (Disjoint on fun x ↦ Ioc (z x) x) x x'

Tactic:
refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_
      refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
⊢ c.ι.app j ≫ (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ) =
    c.ι.app j ≫ (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)

Tactic:
ext x

Goal state after:
case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((Hom.hom (c.ι.app j ≫ (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ))) x).down =
    ((Hom.hom (c.ι.app j ≫ (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ))) x).down
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp

Goal state before:
pp: A : GrpCat
⊢ CartesianMonoidalCategory.lift (↾fun x ↦ x⁻¹)
        (𝟙 (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X) ≫
      μ =
    SemiCartesianMonoidalCategory.toUnit (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X ≫ η

Tactic:
ext x

Goal state after:
A : GrpCat
x : (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X
⊢ (ConcreteCategory.hom
          (CartesianMonoidalCategory.lift (↾fun x ↦ x⁻¹)
              (𝟙 (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X) ≫
            μ)).toFun
      x =
    (ConcreteCategory.hom
          (SemiCartesianMonoidalCategory.toUnit (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X ≫
            η)).toFun
      x
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp

Goal state before:
pp: A : GrpCat
⊢ CartesianMonoidalCategory.lift (𝟙 (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X)
        (↾fun x ↦ x⁻¹) ≫
      μ =
    SemiCartesianMonoidalCategory.toUnit (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X ≫ η

Tactic:
ext x

Goal state after:
A : GrpCat
x : (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X
⊢ (ConcreteCategory.hom
          (CartesianMonoidalCategory.lift (𝟙 (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X)
              (↾fun x ↦ x⁻¹) ≫
            μ)).toFun
      x =
    (ConcreteCategory.hom
          (SemiCartesianMonoidalCategory.toUnit (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X ≫
            η)).toFun
      x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ ContinuousWithinAt f (Iic x) x

Tactic:
by
  rw [ContinuousWithinAt, OrderTopology.topology_eq_generate_intervals (α := Y)]
  simp_rw [TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_nhdsWithin]
  rintro V ⟨z, rfl | rfl⟩ hxz
  -- The case `V = Ioi z`.
  · obtain hz | ne := em' (f ⁻¹' Iic z).Nonempty
    · exact ⟨univ, isOpen_univ, mem_univ _, fun a ha ↦ not_le.mp fun h ↦ hz ⟨a, h⟩⟩
    have bdd : BddAbove (f ⁻¹' Iic z) := ⟨x, fun a ha ↦ (hf.mono.reflect_lt (ha.trans_lt hxz)).le⟩
    have u_eq : Ioi (sSup (f ⁻¹' Iic z)) = f ⁻¹' Ioi z := by
      refine Set.ext fun a ↦ ⟨fun ha ↦ ?_, fun ha ↦ ?_⟩
      · exact not_le.mp fun h ↦ ha.not_ge (le_csSup bdd h)
      · apply lt_of_le_of_ne
        · exact csSup_le ne fun b hb ↦ (hf.mono.reflect_lt (hb.trans_lt ha)).le
        · have : sSup (f '' f ⁻¹' Iic z) ≤ z := csSup_le (.image _ ne) fun _ ⟨b, hb, heq⟩ ↦ heq ▸ hb
          exact fun h ↦ this.not_gt ((h ▸ ha).trans_eq (hf.map_csSup ne bdd))
    exact ⟨f ⁻¹' Ioi z, u_eq ▸ isOpen_Ioi, hxz, fun _ h ↦ h.1⟩
  -- The case `V = Iio z`.
  · exact ⟨univ, isOpen_univ, trivial, fun a ha ↦ (hf.mono ha.2).trans_lt hxz⟩

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Shrink

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F G : C ⥤ GrpCat
τ : F ⟶ G
inst✝¹ : ∀ (X : C), Small.{w, w'} ↑(F.obj X)
inst✝ : ∀ (X : C), Small.{w, w'} ↑(G.obj X)
X Y : C
f : X ⟶ Y
⊢ (shrinkFunctor.{w, w', v, u} F).map f ≫
      ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app Y))).comp Shrink.mulEquiv.toMonoidHom) =
    ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom) ≫
      (shrinkFunctor.{w, w', v, u} G).map f

Tactic:
ext x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F G : C ⥤ GrpCat
τ : F ⟶ G
inst✝¹ : ∀ (X : C), Small.{w, w'} ↑(F.obj X)
inst✝ : ∀ (X : C), Small.{w, w'} ↑(G.obj X)
X Y : C
f : X ⟶ Y
x : ↑((shrinkFunctor.{w, w', v, u} F).obj X)
⊢ (Hom.hom
        ((shrinkFunctor.{w, w', v, u} F).map f ≫
          ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app Y))).comp Shrink.mulEquiv.toMonoidHom)))
      x =
    (Hom.hom
        (ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom) ≫
          (shrinkFunctor.{w, w', v, u} G).map f))
      x
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv

Tactic:
ext x

Goal state after:
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
x : ↑(of R ↥N)
⊢ (Hom.hom (underlyingIso (↟N.subtype)).inv) x = (Hom.hom (↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv)) x
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case i.right.hf
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), (Hom.hom S.arrow) c ∈ (Hom.hom S.arrow).range

Tactic:
exact LinearMap.mem_range_self _

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

Goal state before:
pp: case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) ⋯).toModuleIso.hom ≫
      ↟((fun S ↦ (Hom.hom S.arrow).range) S).subtype =
    S.arrow

Tactic:
ext x

Goal state after:
case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
x : ↑(underlying.obj S)
⊢ (Hom.hom
        ((LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯)
                ⋯).toModuleIso.hom ≫
          ↟((fun S ↦ (Hom.hom S.arrow).range) S).subtype))
      x =
    (Hom.hom S.arrow) x
Module: Mathlib.Algebra.Category.ModuleCat.AB

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
X Y : ModuleCat R
f g : X ⟶ Y
h : ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R), (Hom.hom f) ((Hom.hom h) x) = (Hom.hom g) ((Hom.hom h) x)
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
X Y : ModuleCat R
f g : X ⟶ Y
h : ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R), (Hom.hom f) ((Hom.hom h) x) = (Hom.hom g) ((Hom.hom h) x)
x : ↑X
⊢ (Hom.hom f) x = (Hom.hom g) x
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

Tactic:
rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero 0
      exact h.exact 0 (by lia)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
⊢ Mono (homologyMap φ)

Tactic:
· rw [Preadditive.mono_iff_cancel_zero]
    intro A γ hγ
    obtain ⟨A₁, π₁, hπ₁, z, hz, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ
    rw [← cancel_epi π₁, fac, comp_zero]
    replace hγ := π₁ ≫= hγ
    simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_zero, comp_homologyπ_eq_zero_iff_up_to_refinements] at hγ
    obtain ⟨A₂, π₂, hπ₂, y, hy⟩ := hγ
    replace hy := hy =≫ S₂.iCycles
    simp only [assoc, liftCycles_i, toCycles_i] at hy
    obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ :=
      h (π₂ ≫ z) (by rw [assoc, hz, comp_zero]) y (by simpa)
    rw [liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
    exact ⟨A₃, π₃ ≫ π₂, epi_comp _ _, x₁, by simpa⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ Epi (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
rw [epi_iff_surjective_up_to_refinements]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms 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
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w : ∀ (n : ToType N), (hom g) ((hom (cokernel.π f)) n) = (hom h) ((hom (cokernel.π f)) n)
⊢ g = h

Tactic:
ext x

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms 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
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w : ∀ (n : ToType N), (hom g) ((hom (cokernel.π f)) n) = (hom h) ((hom (cokernel.π f)) n)
x : CC N
⊢ (hom (coequalizer.π f 0 ≫ g)) x = (hom (coequalizer.π f 0 ≫ h)) x
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂

Tactic:
have := abCyclesIso_inv_apply_iCycles (S.map (forget₂ C Ab)) ⟨x₂, hx₂⟩

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    ↑⟨x₂, hx₂⟩
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.mapCyclesIso (forget₂ C Ab)).hom)
        ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩)) =
    x₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case id
J : MultispanShape
a : J.L
h : ¬a = a
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case id
J : MultispanShape
a : J.R
h : ¬a = a
⊢ False

Tactic:
simp at h

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
⊢ (↑eL.symm ∘ₗ g ∘ₗ ↑eN) ∘ₗ (↑eN.symm ∘ₗ f) ∘ₗ ↑eM = 0

Tactic:
ext x

Goal state after:
R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
x : M
⊢ ((↑eL.symm ∘ₗ g ∘ₗ ↑eN) ∘ₗ (↑eN.symm ∘ₗ f) ∘ₗ ↑eM) x = 0 x
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv) ∘ₗ ↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑ULift.moduleEquiv =
    LinearMap.id

Tactic:
ext x

Goal state after:
R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
x : ULift.{max uA uM uB, uB} B
⊢ (((↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑ULift.moduleEquiv) ∘ₗ ↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑ULift.moduleEquiv)
        x).down =
    (LinearMap.id x).down
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ (↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑ULift.moduleEquiv) ∘ₗ ↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv =
    LinearMap.id

Tactic:
ext x

Goal state after:
R : Type u
A : Type uA
M : Type uM
B : Type uB
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : AddCommGroup B
inst✝³ : AddCommGroup M
inst✝² : Module R A
inst✝¹ : Module R B
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
x : ULift.{max uA uM uB, uA} A
⊢ (((↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑ULift.moduleEquiv) ∘ₗ ↑ULift.moduleEquiv.symm ∘ₗ j ∘ₗ ↑ULift.moduleEquiv)
        x).down =
    (LinearMap.id x).down
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (adj.unit.app (G.obj B)) ≫ F.map (G.map (adj.counit.app B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))

Tactic:
rw [← F.map_comp, adj.right_triangle_components]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (𝟙 (G.obj B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
⊢ ∀ ⦃X Y : WalkingMultispan J⦄ (f : X ⟶ Y),
    (I.multispan.map f ≫
        match Y with
        | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
        | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) =
      (match X with
        | WalkingMultispan.left a_1 => c.inj a_1 ≫ I.fstSigmaMapOfIsColimit d hc ≫ a.π
        | WalkingMultispan.right a_1 => d.inj a_1 ≫ a.π) ≫
        ((Functor.const (WalkingMultispan J)).obj a.pt).map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)
        · simp
        · simp
        · simp [a.condition]
        · simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_246 _proof_247)
⊢ mk₂ f f' = mk₂ f g'

Tactic:
obtain rfl : f' = g' := by rwa [← Arrow.mk_inj]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247)
⊢ mk₂ f f' = mk₂ f f'
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ = 𝟙 F

Tactic:
ext x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app x = (𝟙 F).app x
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ = 𝟙 G

Tactic:
ext x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app x = (𝟙 G).app x
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H = mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯

Tactic:
ext x

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
x : WalkingReflexivePair
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app x = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app x
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))
⊢ comap (algebraMap R S) P = p

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ x ∈ comap (algebraMap R S) P ↔ x ∈ p
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
P : Ideal B
p : Ideal A
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
⊢ Subgroup.map (MulAction.stabilizer G P).subtype (stabilizerHom P p G).ker = inertia G P

Tactic:
simp [ker_stabilizerHom, Ideal.inertia_le_stabilizer]

Goal state after: