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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
⊢ s ∈ 𝔖 →
    ∀ (i : SetRel β β),
      i ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i →
        {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i} ∈ F

Tactic:
hs

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i →
      {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i} ∈ F
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹

Tactic:
by
  simp [← Ici_inter_Iio, ← Ioi_inter_Iic, inter_comm]

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure (b * a) = pure 1

Tactic:
← pure_mul_pure,

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure b * pure a = pure 1
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Iic a = Ici (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h

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

Goal state before:
pp: G : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : UniformSpace G
inst✝³ : UniformSpace H
inst✝² : IsUniformGroup H
inst✝¹ : FunLike hom G H
inst✝ : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun p ↦ p.1 / p.2

Tactic:
simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]

Goal state after:
G : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : UniformSpace G
inst✝³ : UniformSpace H
inst✝² : IsUniformGroup H
inst✝¹ : FunLike hom G H
inst✝ : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing ⇑f
⊢ UniformContinuous fun x ↦ f x.1 / f x.2
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z ℱ (g ∘ f)
⊢ ∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ

Tactic:
rw [mapClusterPt_comp] at h

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z (map f ℱ) g
⊢ ∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case pos
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst✝³] {0}

pp: case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst✝³] {0}

Tactic:
· obtain ⟨x, hx, hxW⟩ := H
    cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))

Goal state after:
case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen[inst✝³] {0}
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a : G
⊢ (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹

Tactic:
ext
  rfl

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a : G
⊢ (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹

Tactic:
ext
  rfl

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : connectedComponent 1 = {1}
g : G
⊢ g • {1} = {g * 1}

Tactic:
Set.smul_set_singleton,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : connectedComponent 1 = {1}
g : G
⊢ {g • 1} = {g * 1}
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s / t)

Tactic:
← iUnion_div_right_image

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (⋃ a ∈ t, (fun x ↦ x / a) '' s)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
s : Set α
⊢ (∀ i ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ {x | x.2⁻¹ * x.1 ∈ id i}}) ↔
    ∀ U ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U

Tactic:
simp [← preimage_smul_inv, preimage]

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
hs : s.Nonempty
⊢ f (sSup s) = ⨆ x ∈ s, f x

Tactic:
by
  rw [hf.map_sSup' hs, sSup_image]

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

Goal state before:
pp: case left
α : 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
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
⊢ (map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀)))).NeBot

pp: case right
α : 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
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
⊢ map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ≤
    𝓤 G

Tactic:
· apply NeBot.map
    apply comap_neBot
    intro U h
    rcases mem_closure_iff_nhds.1 ((de.prodMap df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩
    exists z
    simp_all

Goal state after:
case right
α : 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
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
⊢ map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ≤
    𝓤 G
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
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
h : Dense (range fun x ↦ 1 ^ x)
ha₀ : 1 ≤ 1
⊢ (range fun x ↦ 1 ^ x) = univ

pp: case inr.inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
⊢ (range fun x ↦ a ^ x) = univ

Tactic:
· simpa only [one_zpow, range_const, dense_iff_closure_eq, closure_singleton] using h

Goal state after:
case inr.inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
⊢ (range fun x ↦ a ^ x) = univ
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
    rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
    exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : ↑e.symm y = x
⊢ y = ↑e x

Tactic:
by rw [← e.right_inv hy, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : y = ↑e x
⊢ ↑e.symm y = x

Tactic:
← e.left_inv hx,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : y = ↑e x
⊢ ↑e.symm y = ↑e.symm (↑e x)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Tactic:
hs

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Tactic:
e.left_inv hx.1,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ x = ↑e'.symm (↑e x)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s, ⨅ (_ : a ∈ s ∧ ∃ a, s = Ioi a ∨ s = Iio a), 𝓟 s = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
@and_comm (a ∈ _),

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s, ⨅ (_ : (∃ a, s = Ioi a ∨ s = Iio a) ∧ a ∈ s), 𝓟 s = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f

Tactic:
ext
  rfl

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

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) =
    (ConcreteCategory.hom F'.m) 0

Tactic:
rw [F'.fac, map_zero]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) = 0
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
B : Type uB
inst✝⁴ : AddCommGroup B
inst✝³ : Module R A
inst✝² : Module R B
C : Type u_2
inst✝¹ : AddCommGroup C
inst✝ : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
⊢ dual (g ∘ₗ f) = dual f ∘ₗ dual g

Tactic:
ext
  rfl

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

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (c + c').toAddMonoidHom ⋯) x = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) x

Tactic:
refine x.induction_on ?_ ?_ ?_ <;> aesop

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ioc a (a + p)
⊢ ↑((equivIoc p a) ↑y) = y

Tactic:
have : equivIoc p a y = ⟨y, hy⟩ := (equivIoc p a).right_inv ⟨y, hy⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
y : 𝕜
hy : y ∈ Ioc a (a + p)
this : (equivIoc p a) ↑y = ⟨y, hy⟩
⊢ ↑((equivIoc p a) ↑y) = y
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝ : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
⊢ map (↑(AddAut.mulRight ((Units.mk0 p hp)⁻¹ * Units.mk0 q hq))) (zmultiples p) = zmultiples q

Tactic:
rw [AddMonoidHom.map_zmultiples, AddMonoidHom.coe_coe, AddAut.mulRight_apply, Units.val_mul,
      Units.val_mk0, Units.val_inv_eq_inv_val, Units.val_mk0, mul_inv_cancel_left₀ hp]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) = fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
funext x

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) = N

Tactic:
by
        convert!
          congr_arg LinearMap.range
            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1
        · have :
            (underlyingIso (ofHom N.subtype)).inv =
              ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
              ext x
              rfl
          rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]
        · exact (Submodule.range_subtype _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_2.h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) 0 ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) 0 ≫ MonObj.mul

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫ MonObj.mul

Tactic:
· simp only [comp_add, lift_fst, lift_snd, add_zero]
      convert! (MonObj.lift_comp_one_right _ 0).symm
      · simp
      · infer_instance

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫ MonObj.mul
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
constructor
  · intro _ A a
    exact ⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩
  · intro hf
    obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)
    rw [comp_id] at fac
    exact epi_of_epi_fac fac.symm

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g : Y ⟶ (forget (ModuleCat R)).obj M
⊢ freeHomEquiv.symm (f ≫ g) = (free R).map f ≫ freeHomEquiv.symm g

Tactic:
by ext; simp [freeHomEquiv]

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
A : C
z₂ z₂' : A ⟶ S.cycles
⊢ z₂ = S.liftCycles (z₂ ≫ S.iCycles) ⋯

Tactic:
simp [← cancel_mono S.iCycles]

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
A : C
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ z₂' = S.liftCycles (z₂' ≫ S.iCycles) ⋯

Tactic:
simp [← cancel_mono S.iCycles]

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.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.Exact

Tactic:
by
  rw [exact_iff_δlast]
  constructor <;> assumption

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₂), x₂ ≫ S.L₀.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
x₂

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₂
⊢ x₂ ≫ S.L₀.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
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₂), x₂ ≫ S.L₀'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f

Tactic:
x₂

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₂
⊢ x₂ ≫ S.L₀'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀'.f
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✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map 0)) x = 0

Tactic:
Functor.map_zero

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✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom 0) x = 0
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
⊢ Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f)

Tactic:
have := ((CategoryTheory.Functor.exact_tfae (ModuleCat.restrictScalars.{v} f)).out 1 3).mp
    (ModuleCat.restrictScalars_map_exact f)
  exact this.1

Goal state after: