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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀),
    nhdsWithin_univ]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ 𝓤 (α →ᵤ β) ≤ 𝓤 (α →ᵤ β)

Tactic:
refine
      (UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
      (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
        |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
        ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x✝ : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  (f, g) ∈
    (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun p ↦ ((⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.1, (⇑ofFun ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑toFun) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2
⊢ (toFun (f, g).1 x, toFun (f, g).2 x) ∈ U
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
a : α
b : β
⊢ map₂ m (pure a) (pure b) = pure (m a b)

Tactic:
rw [map₂_pure_right, map_pure]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
  rfl

Goal state after:
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))
⊢ ∀ i ∈ 𝔖,
    ∀ (i_1 : SetRel β β),
      i_1 ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i_1 →
        {g_1 | ∀ x ∈ i, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i_1} ∈ F

Tactic:
intro s hs U ⟨hU, hUc⟩

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 ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
⊢ {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id U} ∈ F
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
⊢ x ∈ Icc a b * Icc c d

Tactic:
obtain hxbc | hbcx := le_total x (b * c)

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hxbc : x ≤ b * c
⊢ x ∈ Icc a b * Icc c d

case inr
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hbcx : b * c ≤ x
⊢ x ∈ Icc a b * Icc c d
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
⊢ ∃ a, ↑u = pure a ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩

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 * a) = pure 1
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid γ
inst✝ : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ tendsto_map.comp H⟩

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid γ
inst✝ : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
H : Tendsto (c • m) f (c • g)
⊢ Tendsto m f g
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} • s ∈ 𝓝 (a • b)

Tactic:
singleton_smul,

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ a • s ∈ 𝓝 (a • b)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst✝²] K ⊆ K * closure[inst✝²] {1}

Tactic:
have : IsClosed (K * (closure {1} : Set G)) :=
      IsClosed.smul_left_of_isCompact isClosed_closure hK
    rw [IsClosed.closure_subset_iff this]
    exact subset_mul_closure_one K

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * (x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)

Tactic:
mul_comm x.2.2⁻¹,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * (x.2.1 * x.1.1⁻¹ * x.2.2⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
⊢ ∃ g, Disjoint K (g • L)

Tactic:
refine ⟨g, ?_⟩

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
⊢ Disjoint K (g • L)
Module: Mathlib.Topology.Algebra.Group.GroupTopology

Goal state before:
pp: α : Type u
inst✝ : Group α
f g : GroupTopology α
h : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g

Tactic:
by
    cases f
    cases g
    congr

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)

Tactic:
simp [Homeomorph.comap_nhds_eq]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
⊢ IsLocalMax f⁻¹ a

Tactic:
by
  filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv₀ h4 h2.self_of_nhds).mpr h3

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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 ↑1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
⊢ CompleteSpace (G ⧸ N)

Tactic:
QuotientGroup.mk_one

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Topology.PartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
e' : PartialEquiv X Y
h : e.toPartialEquiv = e'
⊢ e.replacePartialEquiv e' h = e

Tactic:
by
  cases e
  subst e'
  rfl

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
e' : PartialEquiv X Y
h : e.toPartialEquiv = e'
⊢ e.replacePartialEquiv e' h = e

Tactic:
by
  cases e
  subst e'
  rfl

Goal state after:
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:
rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' ∅ = e.target ∩ e'.target

Tactic:
ht.inter_eq,

Goal state after:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' ∅ = ∅
Module: Mathlib.Topology.Order.Basic

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

Tactic:
rw [OrderTopology.topology_eq_generate_intervals (α := α), nhds_generateFrom]
  simp_rw [mem_ofPred_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]

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

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

Tactic:
simp [liftIco, equivIco_coe_eq hx]

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

Goal state before:
pp: case h
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 (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j ↦ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift (AddEquiv.ulift.symm (χ ((Quot.ι F j) x))) = χ ((Quot.ι F j) x)

Tactic:
rw [AddEquiv.apply_symm_apply]

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

Goal state before:
pp: case refine_2
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
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
⊢ a ∈ Ioi (sSup (f ⁻¹' Iic z))

Tactic:
apply lt_of_le_of_ne

Goal state after:
case refine_2.a
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
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
⊢ sSup (f ⁻¹' Iic z) ≤ a

case a
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
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
⊢ sSup (f ⁻¹' Iic z) ≠ a
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a % ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p) + ↑(↑(a % ↑n) * p / ↑n)

pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ 0 ≤ a % ↑n

Tactic:
mul_div_right_comm,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a % ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p) + ↑(↑(a % ↑n) / ↑n * p)

case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ 0 ≤ a % ↑n
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
x✝ :
  (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⊗
    (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
⊢ Multiplicative.toAdd ((ConcreteCategory.hom μ) x✝) =
    (Hom.hom (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X)))
        ((ConcreteCategory.hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X)))
          (Multiplicative.toAdd x✝.1, Multiplicative.toAdd x✝.2)) +
      (Hom.hom (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X)))
        ((ConcreteCategory.hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X)))
          (Multiplicative.toAdd x✝.1, Multiplicative.toAdd x✝.2))

Tactic:
rw [dsimp% [types_tensorObj_def, types_tensorUnit_def] μ_forget_apply]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
x✝ :
  (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⊗
    (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
⊢ Multiplicative.toAdd ((ConcreteCategory.hom μ) x✝) =
    (Hom.hom (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X)))
        (Multiplicative.toAdd x✝.1, Multiplicative.toAdd x✝.2) +
      (Hom.hom (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X)))
        (Multiplicative.toAdd x✝.1, Multiplicative.toAdd x✝.2)
Module: Mathlib.Algebra.Homology.ExactSequence

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

Tactic:
rintro ⟨h, h'⟩
    refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
    · simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.toIsComplex.zero i
      · exact h'.toIsComplex.zero 0
    · simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.exact i
      · exact h'.exact 0

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.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✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ IsEmpty (ToType X)

Tactic:
by
  rw [← Types.initial_iff_empty]
  exact Nonempty.map (IsInitial.isInitialObj (forget C) _) h

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ X₃ : ModuleCat R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (moduleCatMkOfKerLERange f g ⋯).Exact

Tactic:
by
  simpa only [moduleCat_exact_iff_range_eq_ker] using! hfg

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
⊢ ∀ (s : Cone I.multicospan) (m : s.pt ⟶ K.pt), (∀ (j : WalkingMulticospan J), m ≫ K.π.app j = s.π.app j) → m = lift s

Tactic:
by
      rintro E m hm
      apply uniq
      intro i
      apply hm

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ (comparisonAdjunction adj).unit.app B ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)) =
    limit.lift (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (unitFork adj B) ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A))

Tactic:
change
    equalizer.lift ((adj.homEquiv B _) (𝟙 _)) _ ≫ equalizer.ι _ _ =
      equalizer.lift _ _ ≫ equalizer.ι _ _

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ equalizer.lift ((adj.homEquiv B (F.obj B)) (𝟙 (F.obj B))) ⋯ ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)) =
    equalizer.lift (adj.unit.app B) ⋯ ≫ equalizer.ι (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsLimit (unitFork adj Y)

Tactic:
have : IsCoreflexivePair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) := by
        apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
        · rw [← G.map_comp, ← G.map_id]
          exact congr_arg G.map (adj.left_triangle_components Y)
        · rw [← G.map_id]
          simp

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this✝ : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
this : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))
⊢ IsLimit (unitFork adj Y)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

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

Tactic:
by
  obtain ⟨x₀, x₁, x₂, f, f', rfl⟩ := mk₂_surjective f
  obtain ⟨y₀, y₁, y₂, g, g', rfl⟩ := mk₂_surjective g
  obtain rfl : x₀ = y₀ := congr_arg Arrow.leftFunc.obj h₀₁
  obtain rfl : x₁ = y₁ := congr_arg Arrow.rightFunc.obj h₀₁
  obtain rfl : x₂ = y₂ := congr_arg Arrow.rightFunc.obj h₁₂
  obtain rfl : f = g := by rwa [← Arrow.mk_inj]
  obtain rfl : f' = g' := by rwa [← Arrow.mk_inj]
  rfl

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

Goal state before:
pp: A : Type u_2
inst✝³ : CommSemiring A
C : Type u_4
inst✝² : Semiring C
inst✝¹ : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst✝ : p.IsPrime
hPp : ↑p = ⇑(algebraMap A C) ⁻¹' ↑𝔓
⊢ Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓

Tactic:
simpa only [Algebra.algebraMapSubmonoid, primeCompl, hPp, ← le_compl_iff_disjoint_left]
    using! Set.subset_compl_comm.mp (by simp)

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
left✝ : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n • ⊤ ≤ T
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
⊢ x✝¹ ∈ S ⊓ T ∨ ∃ n, r✝ ^ n • ⊤ ≤ S ⊓ T

Tactic:
simp_rw [← mem_colon_iff_le, ← Ideal.mem_radical_iff, inf_colon, Ideal.radical_inf,
    top_coe, h, inf_idem, mem_inf, and_or_right] at hS hT ⊢

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
left✝ : T ≠ ⊤
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ r ∈ (T.colon Set.univ).radical
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (T.colon Set.univ).radical
⊢ (x✝¹ ∈ S ∨ r✝ ∈ (T.colon Set.univ).radical) ∧ (x✝¹ ∈ T ∨ r✝ ∈ (T.colon Set.univ).radical)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ (∀ (n : ℕ) (x : R), x ^ n ∈ Ideal.span {y} → x ∈ Ideal.span {y}) ↔ (Ideal.span {y}).IsRadical

Tactic:
exact forall_comm.trans (forall_congr' fun r => exists_imp.symm)

Goal state after: