mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
nhds_iInf

Goal state after:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) ((⨅ i, 𝓝 x₀) ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
⊢ Equicontinuous F ↔ Equicontinuous ((fun x ↦ u ∘ x) ∘ F)

Tactic:
congrm ∀ x, ?_

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
x : X
⊢ EquicontinuousAt F x ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuousOn (u ∘ Subtype.val) univ
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ UniformEquicontinuousOn (u ∘ Subtype.val) univ

Tactic:
exact hA.closure' (Pi.continuous_domRestrict _ |>.comp hu)

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
⊢ UniformContinuousOn f S

Tactic:
intro U hU; rw [mem_map]
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [h₂ V hV, mem_inf_of_right (mem_principal_self _)]
  rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩
  exact hVU <| hVclosed.mem_of_tendsto ((h₁ x hxS).prodMk_nhds (h₁ y hyS)) <|
    Eventually.of_forall hxy

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]

Tactic:
by
  simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iio, h]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ c * x) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iio, h]

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

Goal state before:
pp: M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
b : Bool
⊢ ContinuousSMul M X

Tactic:
cases b

Goal state after:
case false
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X

case true
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
b : Bool
⊢ IsUniformGroup G

Tactic:
cases b

Goal state after:
case false
G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

case true
G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
⊢ l ≤ (𝓝 0).coprod (𝓝 0)

Tactic:
rw [l_def, ← coprod_cocompact]

Goal state after:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝⁴ : TopologicalSpace M
inst✝³ : MulZeroClass M
inst✝² : ContinuousMul M
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
⊢ map (Prod.map f g) ((cocompact α).coprod (cocompact β)) ≤ (𝓝 0).coprod (𝓝 0)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M

Tactic:
cases b

Goal state after:
case false
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

case true
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
⊢ tᶜ * closure[inst✝²] {1} ⊆ tᶜ

Tactic:
rintro - ⟨x, hx, g, hg, rfl⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure[inst✝²] {1}
⊢ (fun x1 x2 ↦ x1 * x2) x g ∈ tᶜ
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
b : Bool
⊢ ContinuousInv G

Tactic:
cases b

Goal state after:
case false
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

case true
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 ↦ x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto (fun x_1 ↦ u x_1 / x) l (𝓝 1)

Tactic:
by simpa using h.div' A

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ interior ((fun x ↦ g₀ * g⁻¹ * x) ⁻¹' V)

Tactic:
refine preimage_interior_subset_interior_preimage (by fun_prop) ?_

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x ↦ g₀ * g⁻¹ * x) ⁻¹' interior V
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
b : Bool
⊢ IsTopologicalGroup G

Tactic:
cases b

Goal state after:
case false
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

case true
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, MulOpposite.op x⁻¹ • y ∈ K
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
MulOpposite.op_inv,

Goal state after:
G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, (MulOpposite.op x)⁻¹ • y ∈ K
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Type u_2
inst✝ : Group H
f : H →* G
hf : Function.Injective ⇑f
hf' : IsDiscrete ↑f.range
⊢ Tendsto (⇑f) cofinite (cocompact G)

Tactic:
by
  replace hf : Function.Injective f.rangeRestrict := by simpa
  exact (f.range.tendsto_coe_cofinite_of_discrete hf').comp hf.tendsto_cofinite

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
let Nx := 𝓝 x₀

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W'
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
⊢ (∀ a' < 1, ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ a' > 1, ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'

Tactic:
refine ⟨fun x hx => ?_, fun x hx => ?_⟩
  · obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
        max_lt hx one_half_lt_one⟩
    filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
    exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2
  · filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
    exact inv_lt_of_inv_lt₀ (by positivity) hy

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
x : α
hx : x ∈ s
⊢ e.symm (e x) ∈ s

Tactic:
rwa [e.symm_apply_apply]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.trans e.symm ≈ ofSet e.source

Tactic:
have A : (e.trans e.symm).source = e.source := by mfld_set_tac

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
⊢ e.trans e.symm ≈ ofSet e.source
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ z ≫ S.iCycles = S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.iCycles

Tactic:
liftCycles_i

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ z ≫ S.iCycles = z ≫ S.iCycles
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
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ S.liftCycles x₂ hx₂ = x₁ ≫ S.toCycles

Tactic:
simp [liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, ← cancel_mono S.iCycles]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : Type u
⊢ (λ_ ((free R).obj X)).hom = (εIso R).hom ▷ (free R).obj X ≫ (μIso R (𝟙_ (Type u)) X).hom ≫ (free R).map (λ_ X).hom

Tactic:
by
        rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id]
        aesop

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₂
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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ (π₂ ≫ z) ≫ S₁.g = 0

Tactic:
assoc,

Goal state after:
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
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ π₂ ≫ z ≫ S₁.g = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ single f r ≫ single g s = single (f ≫ g) (r * s)

Tactic:
dsimp +instances [CategoryTheory.categoryFree]
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
⊢ (x₂ ≫ S.v₀₁.τ₂) ≫ S.L₁.g = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
⊢ x₂ ≫ S.v₀₁.τ₂ ≫ S.L₁.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
⊢ (x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃) ≫ S.L₁.g = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
⊢ x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.L₁.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃) ≫ S.δ = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ p ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        (S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁) ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        (S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁) ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.fst S.L₁.g S.v₀₁.τ₃ ≫
        (S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.fst S.L₁.g S.v₀₁.τ₃ ≫
        (S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.fst S.L₁.g S.v₀₁.τ₃ ≫
        S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: case mp
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
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono f → Mono ((forget₂ C Ab).map f)

Tactic:
intro
    infer_instance

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

Goal state before:
pp: case mp
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
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Epi f → Epi ((forget₂ C Ab).map f)

Tactic:
intro
    infer_instance

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ (F.map' i (i + k) ⋯ ⋯ ≫ F.map' (i + k) (i + k + 1) ⋯ hj') ≫ app ⟨i + k + 1, ⋯⟩ =
    app ⟨i, ⋯⟩ ≫ G.map' i (i + k) ⋯ ⋯ ≫ G.map' (i + k) (i + k + 1) ⋯ hj'

Tactic:
assoc,

Goal state after:
case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ F.map' i (i + k) ⋯ ⋯ ≫ F.map' (i + k) (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ =
    app ⟨i, ⋯⟩ ≫ G.map' i (i + k) ⋯ ⋯ ≫ G.map' (i + k) (i + k + 1) ⋯ hj'