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

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS

Goal state after:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V
hxS : x ∈ S
⊢ ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖))

Tactic:
rw [uniformContinuous_iff_le_comap]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
inf_uniformity

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ) ⊓ 𝓤 (α →ᵤ[𝔖] β × γ)
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:
rw [← pure_mul_pure, ← ha, ← hb]

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
⊢ ↑u⁻¹ * ↑u = pure 1
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
f✝ g : C(α, β)
I : Type u_5
A : Type u_6
X : I → Type u_7
inst✝¹ : TopologicalSpace A
inst✝ : (i : I) → TopologicalSpace (X i)
f : (i : I) → C(X i, A)
⊢ Continuous[instTopologicalSpaceSigma, inst✝¹] fun ig ↦ (f ig.fst) ig.snd

Tactic:
continuity

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Tactic:
← comap_principal,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑𝒰 ≤ comap f (𝓟 K)
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y : X
⊢ ContinuousMap.mulRight (x * y) = (ContinuousMap.mulRight y).comp (ContinuousMap.mulRight x)

Tactic:
by
  ext; simp [mul_assoc]

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

Goal state before:
pp: X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y : X
⊢ ContinuousMap.mulLeft (x * y) = (ContinuousMap.mulLeft x).comp (ContinuousMap.mulLeft y)

Tactic:
by
  ext; simp [mul_assoc]

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
c a : G
⊢ map (fun x ↦ x * c) (𝓝[≠] a) = 𝓝[≠] (a * c)

Tactic:
by
  convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

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

Goal state before:
pp: G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x * b) l (𝓝 (c * b)) → Tendsto f l (𝓝 c)

Tactic:
convert! Tendsto.mul_const b⁻¹ using 3 <;> rw [mul_inv_cancel_right]

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ x * c) (𝓝[>] a) = 𝓝[>] (a * c)

Tactic:
by
  convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ x * c) (𝓝[<] a) = 𝓝[<] (a * c)

Tactic:
by
  convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ ↑n

Tactic:
by
    simp_rw [zpow_natCast]
    exact hf.pow_const _

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
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (𝓝 x).HasBasis p fun i ↦ {y | y / x ∈ s i}

Tactic:
rw [← nhds_translation_mul_inv]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (Filter.comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i ↦ {y | y / x ∈ s i}
Module: Mathlib.Order.Filter.AtTopBot.Group

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
l : Filter α
f : G → α
⊢ Tendsto (fun x ↦ f x⁻¹) atTop l ↔ Tendsto f atBot l

Tactic:
by
  simp [← Function.comp_def, Tendsto, ← map_map, map_inv_atTop]

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

Goal state before:
pp: G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun k ↦ b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, Filter.Tendsto.const_div' b⟩

Goal state after:
G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k ↦ b / f k) l (𝓝 (b / c))
⊢ Tendsto f l (𝓝 c)
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 : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_of_neg, hr]

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f g : α → G₀
inst✝ : TopologicalSpace α
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous[inst✝, inst✝³] (f / g)

Tactic:
simpa only [div_eq_mul_inv] using! hf.mul (hg.inv₀ h₀)

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f g : α → G₀
inst✝ : TopologicalSpace α
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous[inst✝, inst✝³] fun x ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using! hf.mul (hg.inv₀ h₀)

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

Goal state before:
pp: R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 * p.2

Tactic:
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_ <;>
      simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
simp only [iSup, hf.map_csSup (range_nonempty _) hg, ← range_comp]

Goal state after:
α : Type u
β : Type v
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ sSup (range (f ∘ g)) = sSup (range fun i ↦ f (g i))
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: 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, a ^ m ∈ Ioo b (b * a * a)

Tactic:
have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩

Goal state after:
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
hne : (Ioo b (b * a * a)).Nonempty
⊢ ∃ m, a ^ m ∈ Ioo b (b * a * a)
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
this : {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x | IsTop x}
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
apply Countable.mono this

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := ⋯
H : t.Countable
this : {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x | IsTop x}
⊢ (t ∪ {x | IsTop x}).Countable
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
by
  rw [mem_nhdsGT_iff_exists_Ioo_subset]
  constructor
  · rintro ⟨u, au, as⟩
    rcases exists_between au with ⟨v, hv⟩
    exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
  · rintro ⟨u, au, as⟩
    exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩

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 𝕜
a : 𝕜
ha : a < 0
⊢ Ioo a 0 = ((fun i ↦ Inv.inv '' Iio i) ∘ Inv.inv) a

Tactic:
simp [inv_Iio₀ (inv_neg''.2 ha)]

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)
⊢ EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)

Tactic:
← h.image_eq

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)
⊢ EqOn (↑e.symm) (↑e'.symm) (↑e '' (e.source ∩ s))
Module: Mathlib.Topology.Order.Basic

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

Tactic:
mem_ofPred_eq,

Goal state after:
α : 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)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ x ∈ {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
mem_ofPred_eq,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIcoMod hp a x = toIocMod hp a x
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
⊢ χ = ψ

pp: case refine_2
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)
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ

Tactic:
· apply AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv.injective
    apply ofHom_injective
    refine hc.hom_ext (fun j ↦ ?_)
    ext x
    erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ← Quot.ι_desc _ c j x]
    exact DFunLike.congr_fun eq (Quot.ι F j x)

Goal state after:
case refine_2
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)
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ
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 : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ liftIoc p a f x = liftIco p a f x

Tactic:
rw [x_eq_b, liftIco_coe_apply (equivIco p a x).coe_prop]

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ liftIoc p a f ↑↑((equivIco p a) x) = f ↑((equivIco p a) x)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
⊢ atTop.IsCountablyGenerated

Tactic:
by
  obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty {x : α | IsTop x}
  · obtain ⟨s, s_count, hs⟩ := exists_countable_dense α
    have : atTop = generate (Ici '' s) := by
      refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_
      simp only [eq_empty_iff_forall_notMem, IsTop, mem_ofPred_eq, not_forall, not_le] at h
      obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)
      exact (hx hy).not_gt hxy
    rw [this]
    exact ⟨_, s_count.image _, rfl⟩
  · rw [atTop_eq_pure_of_isTop hx]
    exact isCountablyGenerated_pure x

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₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ app' e.hom i ⋯ ≫ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
← NatTrans.naturality_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ S₁.map (homOfLE ⋯) ≫ e.hom.app ⟨i + 1, ⋯⟩ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0
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
hS : S.Exact
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS
  exact hS x₂ hx₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case mp
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃

Tactic:
exact ⟨h.w, fun x₁ y₁ ⟨h₁, h₂⟩ ↦ ext_of_isPullback h h₁ h₂, exists_of_isPullback h⟩

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 v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : ToType (widePushout B X f)
⊢ (∃ y, (hom (head f)) y = x) ∨ ∃ i y, (hom (ι f i)) y = x

Tactic:
obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x

Goal state after:
case none
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y

case some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case inr
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : ToType (X i)
⊢ ∃ i_1 y_1, (hom (ι f i_1)) y_1 = (hom (ι f i)) y

Tactic:
use i, y

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.g))

Tactic:
← Preadditive.epi_iff_surjective

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Epi S.g
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
x y : ↑S.X₂
h : (ConcreteCategory.hom S.pOpcycles) x = (ConcreteCategory.hom S.pOpcycles) y
⊢ Submodule.Quotient.mk x = Submodule.Quotient.mk y

Tactic:
simpa using congr(S.moduleCatOpcyclesIso.hom $h)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝ : Category.{v, u} J✝
D : J✝ ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J✝), m ≫ (liftedCone D c t).π.app j = s.π.app j
⊢ m.f = { f := t.lift (T.forget.mapCone s), h := ⋯ }.f

Tactic:
apply t.hom_ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝ : Category.{v, u} J✝
D : J✝ ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J✝), m ≫ (liftedCone D c t).π.app j = s.π.app j
⊢ ∀ (j : J✝), m.f ≫ c.π.app j = { f := t.lift (T.forget.mapCone s), h := ⋯ }.f ≫ c.π.app j