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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : U₁ ∈ comap (⇑e) (𝓝 x₀)
V₁ : Set δ
V₁_nhds : V₁ ∈ comap (⇑f) (𝓝 y₀)
H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'

Tactic:
obtain ⟨y₁, y₁_in⟩ : V₁.Nonempty := (df.comap_nhds_neBot _).nonempty_of_mem V₁_nhds

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : U₁ ∈ comap (⇑e) (𝓝 x₀)
V₁ : Set δ
V₁_nhds : V₁ ∈ comap (⇑f) (𝓝 y₀)
H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case inr.inl
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : b < a ^ (m - 1)
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty

Tactic:
refine ⟨b * a * a, hm', ?_⟩
    simpa only [zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, lt_div_iff_mul_lt,
      mul_lt_mul_iff_right] using hlt

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p (x * ε)

Tactic:
rw [← comap_mulLeft_nhdsGT_zero hx]
  exact h.comap fun ε => x * ε

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ ∀ u ∈ {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}, IsOpen[ts] u

pp: case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}} ⊆
    {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}

Tactic:
· rintro u ⟨f, g, hfc, hgc, hf_fin, hg_fin, rfl⟩
    apply IsOpen.inter
    · apply hf_fin.isOpen_biInter (fun i hi ↦ ?_)
      rw [h]
      exact isOpen_generateFrom_of_mem ⟨i, hfc hi, Or.inl rfl⟩
    · apply hg_fin.isOpen_biInter (fun i hi ↦ ?_)
      rw [h]
      exact isOpen_generateFrom_of_mem ⟨i, hgc hi, Or.inr rfl⟩

Goal state after:
case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}} ⊆
    {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : 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
⊢ {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable

Tactic:
let t := { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x }

Goal state after:
α : 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}
⊢ {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
⊢ liftIoc p a f = liftIco p a f

Tactic:
ext q
  obtain ⟨x, hx, rfl⟩ := by simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q
  rw [liftIco_coe_apply hx]
  obtain (⟨rfl, -⟩ | h) := by rwa [mem_Ico, le_iff_eq_or_lt, or_and_right] at hx
  · rw [← coe_add_period, liftIoc_coe_apply (by simp [hp.out]), hf]
  · exact liftIoc_coe_apply ⟨h.1, h.2.le⟩

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 : ShortComplex C
⊢ Epi S.toCycles ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
epi_iff_surjective_up_to_refinements

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ (ConcreteCategory.hom (freeDesc f)) (freeMk x) = (ConcreteCategory.hom f) x

Tactic:
dsimp [freeDesc]

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ (ConcreteCategory.hom (↟((Finsupp.lift (↑M) R X) ⇑(ConcreteCategory.hom f)))) (freeMk x) = (ConcreteCategory.hom f) x
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h : { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.Exact
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements] at h

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.g = 0 →
      ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
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:
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.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃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

Tactic:
hy₂

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : 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: case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd b')))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left (J.snd b'))) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b')

pp: case right.right.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.right b)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b)

Tactic:
· dsimp
          exact (x.2 b').symm

Goal state after:
case right.right.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.right b)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MulticospanShape
⊢ ∀ {X Y : WalkingMulticospan J} (f : X.Hom Y), (Hom.id X).comp f = f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)

Goal state after:
case left.left.id
J : MulticospanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.fst a✝))).comp (Hom.fst a✝) = Hom.fst a✝

case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (left (J.snd a✝))).comp (Hom.snd a✝) = Hom.snd a✝

case right.right.id
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MulticospanShape
⊢ ∀ {X Y : WalkingMulticospan J} (f : X.Hom Y), f.comp (Hom.id Y) = f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)

Goal state after:
case left.left.id
J : MulticospanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MulticospanShape
a✝ : J.R
⊢ (Hom.fst a✝).comp (Hom.id (right a✝)) = Hom.fst a✝

case left.right.snd
J : MulticospanShape
a✝ : J.R
⊢ (Hom.snd a✝).comp (Hom.id (right a✝)) = Hom.snd a✝

case right.right.id
J : MulticospanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ ∀ {X Y : WalkingMultispan J} (f : X.Hom Y), (Hom.id X).comp f = f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)

Goal state after:
case left.left.id
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.fst a✝) = Hom.fst a✝

case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.snd a✝) = Hom.snd a✝

case right.right.id
J : MultispanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ ∀ {X Y : WalkingMultispan J} (f : X.Hom Y), f.comp (Hom.id Y) = f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)

Goal state after:
case left.left.id
J : MultispanShape
a✝ : J.L
⊢ (Hom.id (left a✝)).comp (Hom.id (left a✝)) = Hom.id (left a✝)

case left.right.fst
J : MultispanShape
a✝ : J.L
⊢ (Hom.fst a✝).comp (Hom.id (right (J.fst a✝))) = Hom.fst a✝

case left.right.snd
J : MultispanShape
a✝ : J.L
⊢ (Hom.snd a✝).comp (Hom.id (right (J.snd a✝))) = Hom.snd a✝

case right.right.id
J : MultispanShape
a✝ : J.R
⊢ (Hom.id (right a✝)).comp (Hom.id (right a✝)) = Hom.id (right a✝)
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.pOpcycles ≫ S.moduleCatOpcyclesIso.hom = ModuleCat.ofHom (ModuleCat.Hom.hom S.f).range.mkQ

Tactic:
by
  simp [moduleCatOpcyclesIso]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ sigmaπ I = π I b

Tactic:
rw [sigmaπ, ← Category.assoc, Iso.comp_inv_eq, isoCoequalizer]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    π I b ≫
      (colimit.isoColimitCocone
          {
            cocone :=
              I.multicoforkEquivSigmaCofork.inverse.obj (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap)),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial I.multicoforkEquivSigmaCofork.inverse
                (colimit.isColimit (parallelPair I.fstSigmaMap I.sndSigmaMap)) }).hom
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ eqToHom h₀ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom h₀ ≫ G.map (homOfLE ⋯)

Tactic:
eqToHom_trans,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ eqToHom h₀ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯ = eqToHom h₀ ≫ G.map (homOfLE ⋯)
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
⊢ PreservesFiniteLimits (tensorLeft M)

Tactic:
by
  rw [← iff_preservesFiniteLimits_tensorLeft]
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : CommSemiring Rp
inst✝⁵ : Algebra R Rp
inst✝⁴ : AddCommMonoid Mp
inst✝³ : Module R Mp
inst✝² : Module Rp Mp
inst✝¹ : IsScalarTower R Rp Mp
inst✝ : Flat R M
S : Submonoid R
⊢ Flat (Localization S) (LocalizedModule S M)

Tactic:
apply Flat.isBaseChange (R := R) (S := Localization S)
    (f := LocalizedModule.mkLinearMap S M)

Goal state after:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : CommSemiring Rp
inst✝⁵ : Algebra R Rp
inst✝⁴ : AddCommMonoid Mp
inst✝³ : Module R Mp
inst✝² : Module Rp Mp
inst✝¹ : IsScalarTower R Rp Mp
inst✝ : Flat R M
S : Submonoid R
⊢ IsBaseChange (Localization S) (LocalizedModule.mkLinearMap S M)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ c.ι.app j ≫ (liftedCocone D c t).pt.a ≫ T.map (t.desc (T.forget.mapCocone s)) =
    c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a

Tactic:
by
          dsimp
          rw [← Category.assoc, ← Category.assoc, t.fac, newCocone_ι_app, t.fac,
            Functor.mapCocone_ι_app, Category.assoc, ← Functor.map_comp, t.fac]
          apply (s.ι.app j).h

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ g.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_364✝ _proof_365✝

Tactic:
by rw [map'_inv_eq_inv_map' (by valid) app₃ app₄ w₃]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
⊢ CreatesLimit K R

Tactic:
letI A := Comonad.comparison (comonadicAdjunction R)
  letI B := Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))
  let i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _ ≅ K ⋙ R :=
    Functor.associator _ _ _ ≪≫
      isoWhiskerLeft K (Comonad.comparisonForget (comonadicAdjunction R))
  letI : PreservesLimit ((K ⋙ A) ⋙ Comonad.forget
    (Adjunction.toComonad (comonadicAdjunction R)))
      (Adjunction.toComonad (comonadicAdjunction R)).toFunctor := by
    dsimp
    exact preservesLimit_of_iso_diagram _ i.symm
  letI : PreservesLimit
    (((K ⋙ A) ⋙ Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))) ⋙
      (Adjunction.toComonad (comonadicAdjunction R)).toFunctor)
      (Adjunction.toComonad (comonadicAdjunction R)).toFunctor := by
    dsimp
    exact preservesLimit_of_iso_diagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm
  letI : CreatesLimit (K ⋙ A) B := CategoryTheory.Comonad.forgetCreatesLimit _
  letI : CreatesLimit K (A ⋙ B) := CategoryTheory.compCreatesLimit _ _
  let e := Comonad.comparisonForget (comonadicAdjunction R)
  apply createsLimitOfNatIso e

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_364✝ _proof_453✝

Tactic:
by rw [map'_inv_eq_inv_map' (by valid) app₃ app₄ w₃]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ (s⁻¹ * (s * g * s⁻¹)) • x - s⁻¹ • x ∈ s⁻¹ • P

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ (s⁻¹ * (s * g) * s⁻¹) • x - s⁻¹ • x ∈ s⁻¹ • P