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

Goal state before:
pp: case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
⊢ x ∈ K → ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
hx

Goal state after:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun x ↦ x * b) ∘ fun x ↦ x * a) (cocompact M) (cocompact M)

Tactic:
simp only [comp_mul_right, ha, mul_one]

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x ↦ x) (cocompact M) (cocompact M)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
⊢ x ∈ t → ContinuousWithinAt (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t x

Tactic:
hx

Goal state after:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
⊢ (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b ↦ (Multiset.map (fun c ↦ f c b) s).prod) x (𝓝 (Multiset.map a s).prod)

Tactic:
rcases s with ⟨l⟩

Goal state after:
case mk
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b ↦ (Multiset.map (fun c ↦ f c b) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) x
      (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι)) l)).prod)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
⊢ (∀ i ∈ s, Continuous[inst✝³, inst✝²] (f i)) → Continuous[inst✝³, inst✝²] fun a ↦ (Multiset.map (fun i ↦ f i a) s).prod

Tactic:
rcases s with ⟨l⟩

Goal state after:
case mk
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Continuous[inst✝³, inst✝²] (f i)) →
    Continuous[inst✝³, inst✝²] fun a ↦ (Multiset.map (fun i ↦ f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
⊢ (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a ↦ (Multiset.map (fun i ↦ f i a) s).prod) t

Tactic:
rcases s with ⟨l⟩

Goal state after:
case mk
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, ContinuousOn (f i) t) →
    ContinuousOn (fun a ↦ (Multiset.map (fun i ↦ f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) t
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
x : X
⊢ (∀ i ∈ s, f i x = g i x) → (∏ i ∈ s, f i) x = (∏ i ∈ s, g i) x

Tactic:
hx

Goal state after:
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
x : X
hx : ∀ i ∈ s, f i x = g i x
⊢ (∏ i ∈ s, f i) x = (∏ i ∈ s, g i) x
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x ℱ

Tactic:
rw [← clusterPt_lift'_closure_iff]

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (ℱ.lift' closure[inst✝¹])
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

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst✝²] (K * closure[inst✝²] {1})
⊢ closure[inst✝²] K ⊆ K * closure[inst✝²] {1}
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
⊢ K * closure[inst✝²] {1} = closure[inst✝²] K

Tactic:
by
  apply Subset.antisymm ?_ ?_
  · calc
    K * (closure {1} : Set G) ⊆ closure K * (closure {1} : Set G) :=
      smul_subset_smul_right subset_closure
    _ ⊆ closure (K * ({1} : Set G)) := smul_set_closure_subset _ _
    _ = closure K := by simp
  · 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.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
⊢ x ∈ closure[inst✝²] U → x ∈ U * U

Tactic:
hx

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : x ∈ closure[inst✝²] U
⊢ x ∈ U * U
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : V ∈ 𝓝 1
hUV : image2 HMul.hMul U V ⊆ s
⊢ closure[inst✝²] U ⊆ s

Tactic:
calc
    closure U ⊆ closure U * interior V := subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
    _ = U * interior V := isOpen_interior.closure_mul U
    _ ⊆ U * V := mul_subset_mul_left interior_subset
    _ ⊆ s := hUV

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
H : Type u_1
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
⊢ IsInducing ⇑f ↔ 𝓝 1 = comap (⇑f) (𝓝 1)

Tactic:
by
  rw [Topology.isInducing_iff_nhds]
  refine ⟨(map_one f ▸ · 1), fun hf x ↦ ?_⟩
  rw [← nhds_translation_mul_inv, ← nhds_translation_mul_inv (f x), Filter.comap_comap, hf,
    Filter.comap_comap]
  congr 1
  ext; simp

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

Goal state before:
pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
⊢ x ∈ K → ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
hx

Goal state after:
case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
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
⊢ ∃ g, Disjoint K (g • L)

Tactic:
have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ

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, Disjoint K (g • L)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map (fun x_1 ↦ x * x_1) (map (fun x ↦ x * y) (𝓝 1 * 𝓝 1)) = map₂ (fun a b ↦ x * (a * b * y)) (𝓝 1) (𝓝 1)

Tactic:
rw [← map₂_mul, map_map₂, map_map₂]

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

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f g : A →ₜ* B
h : f.toContinuousMap = g.toContinuousMap
⊢ ∀ (x : A), f x = g x

Tactic:
convert! DFunLike.ext_iff.1 h

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

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f g : A →ₜ* B
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (x : A), f x = g x

Tactic:
convert! DFunLike.ext_iff.1 h

Goal state after:
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
x : α
⊢ x ∈ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} → x ∈ t ∪ {x | IsTop x}

Tactic:
hx

Goal state after:
α : 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
x : α
hx : x ∈ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}
⊢ x ∈ t ∪ {x | IsTop x}
Module: Mathlib.Topology.Algebra.Order.Field

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

Tactic:
filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
y : 𝕜
hy : y ∈ Ioi x⁻¹
⊢ y⁻¹ < x
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 ∈ ⇑e '' s
⊢ e.symm x ∈ s

Tactic:
rcases hx with ⟨x, hx, rfl⟩

Goal state after:
α : 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
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
x : α
⊢ |f x| ≤ C → (abs ∘ fun x ↦ f x * g x) x ≤ |C * g x|

Tactic:
hx

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
x : α
hx : |f x| ≤ C
⊢ (abs ∘ fun x ↦ f x * g x) x ≤ |C * g 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)
⊢ EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)

Tactic:
rw [← 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.Logic.Equiv.PartialEquiv

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
⊢ x ∈ (e.trans f).source → ↑(e.trans f) x = ↑(e'.trans f') x

Tactic:
hx

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (e.trans f).source
⊢ ↑(e.trans f) x = ↑(e'.trans f') x
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
⊢ x ∈ (e.restr s).source → ↑(e.restr s) x = ↑(e'.restr s) x

Tactic:
hx

Goal state after:
case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ (e.restr s).source
⊢ ↑(e.restr s) x = ↑(e'.restr s) x
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) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) =
    (ConcreteCategory.hom F'.m) 0

Tactic:
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.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
by_cases! h : ∃ x, ¬(b < f x)
    · rcases h with ⟨x, hx⟩
      rcases H₁ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz))
    · exact le_principal_iff.2 (univ_mem' h)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
⊢ x < ⊤ → ∀ᶠ (a : α) in l, g a ∈ Ioi x

Tactic:
hx

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p x : 𝕜
⊢ ↑x + ↑p = ↑x

Tactic:
← eq_sub_iff_add_eq',

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p x : 𝕜
⊢ ↑p = ↑x - ↑x
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
r : R
c : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (r • c).toAddMonoidHom ⋯) 0 = ((RingHom.id R) r • liftAddHom c.toAddMonoidHom ⋯) 0

Tactic:
map_zero

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

Goal state before:
pp: case pos
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
a : A
h : addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat 2)) 0 = 0

Tactic:
map_zero

Goal state after:
case pos
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
a : A
h : addOrderOf a = 0
⊢ 0 = 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
x : α
⊢ x ∈ t → ∃ z < x, Ioc z x ⊆ a

Tactic:
hx

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
x : α
hx : x ∈ t
⊢ ∃ z < x, Ioc z x ⊆ a
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
x : β
⊢ x ∈ s → ∀ ⦃b : β⦄, b ∈ s → x < b → f x < f b

Tactic:
hx

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
x : β
hx : x ∈ s
⊢ ∀ ⦃b : β⦄, b ∈ s → x < b → f x < f b
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 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x✝ : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
x : 𝕜
⊢ x ∈ Ioo a (a + p) → ↑x ∈ {↑a}ᶜ

Tactic:
hx

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
p : 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x✝ : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
x : 𝕜
hx : x ∈ Ioo a (a + p)
⊢ ↑x ∈ {↑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 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x✝ : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
x : AddCircle p
⊢ x ∈ {↑a}ᶜ → ↑((equivIco p a) x) ∈ Ioo a (a + p)

Tactic:
hx

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
p : 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x✝ : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
x : AddCircle p
hx : x ∈ {↑a}ᶜ
⊢ ↑((equivIco p a) x) ∈ Ioo a (a + p)
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
⊢ zmultiples ((AddAut.mulRight ((Units.mk0 p hp)⁻¹ * Units.mk0 q hq)) p) = zmultiples q

Tactic:
AddAut.mulRight_apply,

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝ : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
⊢ zmultiples (p * ↑((Units.mk0 p hp)⁻¹ * Units.mk0 q hq)) = zmultiples q
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)

Tactic:
← addOrderOf_pos_iff,

Goal state after:
case h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ 0 < addOrderOf ↑(p / ↑n)
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 * ↑n) * p / ↑n + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑k

Tactic:
Int.cast_mul,

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) * ↑↑n * p / ↑n + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑k
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
this : IsEmpty { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
exact Nat.card_of_isEmpty

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

Goal state before:
pp: case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ ∀ (hx : x ∈ Icc a (a + p)),
    x ≠ a + p →
      Quot.mk (EndpointIdent p a)
          (Set.inclusion ⋯ ((equivIco p a) ((Quot.mk (EndpointIdent p a) ⟨x, hx⟩).liftOn (fun x ↦ ↑↑x) ⋯))) =
        Quot.mk (EndpointIdent p a) ⟨x, hx⟩

Tactic:
hx

Goal state after:
case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
⊢ x ≠ a + p →
    Quot.mk (EndpointIdent p a)
        (Set.inclusion ⋯ ((equivIco p a) ((Quot.mk (EndpointIdent p a) ⟨x, hx⟩).liftOn (fun x ↦ ↑↑x) ⋯))) =
      Quot.mk (EndpointIdent p a) ⟨x, hx⟩
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_2.h₁.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
· infer_instance

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

Goal state before:
pp: case h₂.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
· infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.GrpWithZero

Goal state before:
pp: α β : GrpWithZero
e : α.carrier ≃* β.carrier
x✝ : β.carrier
⊢ (ConcreteCategory.hom (ofHom (MonoidWithZeroHom.ofClass e.symm) ≫ ofHom (MonoidWithZeroHom.ofClass e))) x✝ =
    (ConcreteCategory.hom (𝟙 β)) x✝

Tactic:
exact e.apply_symm_apply _

Goal state after: