mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsMeagre s ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
by
  rw [IsMeagre, mem_residual_iff, compl_bijective.surjective.image_surjective.exists]
  simp_rw [← and_assoc, ← forall_and, forall_mem_image, ← isClosed_isNowhereDense_iff_compl,
    sInter_image, ← compl_iUnion₂, compl_subset_compl, ← sUnion_eq_biUnion, and_assoc]
  refine ⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩
  · rw [← compl_compl_image S]; exact hc.image _
  · intro ⟨S, hS, hc, hsub⟩
    use closure '' S
    rw [forall_mem_image]
    exact ⟨fun s hs ↦ ⟨isClosed_closure, (hS s hs).closure⟩,
      (hc.image _).image _, hsub.trans (sUnion_mono_subsets fun s ↦ subset_closure)⟩

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ Nonempty (ConnectedComponents α) ↔ Nonempty α

Tactic:
nonempty_iff_nonempty

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
⊢ Nonempty α ↔ Nonempty α
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (s ∩ t)

Tactic:
by
  rw [inter_eq_iInter]
  apply dense_iInter_of_Gδ <;> simp [Bool.forall_bool, *]

Goal state after:
Module: Mathlib.Data.Rel.Cover

Goal state before:
pp: X : Type u_1
s N : Set X
⊢ IsCover univ s N ↔ s.Nonempty → N.Nonempty

Tactic:
simp [IsCover, Set.Nonempty]

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace α ↔ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
refine ⟨fun _ _ => isClopen_iff.mp, fun h ↦ ?_⟩
  refine preconnectedSpace_of_forall_constant fun f hf x y ↦ ?_
  have : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ := by
    rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]
  obtain (h | h) := h _ ((isClopen_discrete {true}).preimage hf) <;> simp_all

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x

Tactic:
exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ u '' univ ⊆ K

Tactic:
image_univ,

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ range u ⊆ K
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ ∀ (a b : α), a ∈ s → b ∈ s → f a ∈ t ∧ f b ∈ t

Tactic:
exact fun a b ha hb ↦ ⟨hst ha, hst hb⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
hdj :
  ∀ (b : Bool) (x : ↑(S b)) (y : ↑(S !b)),
    U b x ≤ U (!b) y → Disjoint (ball (↑x) (B (U b x))) (ball (↑y) (B (U (!b) y)))
x : ↑(S false)
y : ↑(S true)
⊢ Disjoint (ball (↑x) (B (U false x))) (ball (↑y) (B (U true y)))

Tactic:
exact (le_total (U false x) (U true y)).elim
      (fun h => hdj false x y h) (fun h => (hdj true y x h).symm)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
ha : UniformContinuous id
hb : UniformContinuous id
⊢ UniformContinuous fun p ↦ f p.1 p.2
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n ↦ F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n ↦ F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ u

Tactic:
refine Set.mem_of_mem_of_subset ?_ htmem

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n ↦ F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n ↦ F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ SetRel.comp t t
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z | (f x, f z) ∈ t} ∩ {z | (g x, g z) ∈ t}
u_open : IsOpen[inst✝] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r

Tactic:
hfg hx

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z | (f x, f z) ∈ t} ∩ {z | (g x, g z) ∈ t}
u_open : IsOpen[inst✝] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, g x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : (x : α) → x ∈ K → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝[K] x
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ y, ball x t ∩ K ⊆ U ↑y ⋯) → ∀ x ∈ K, ∃ y, ball x s ∩ K ⊆ U ↑y ⋯

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : α → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝[K] x
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ y, ball x t ∩ K ⊆ U y) → ∀ x ∈ K, ∃ y, ball x s ∩ K ⊆ U y

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy

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

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f • f') x = 0 x

Tactic:
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

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

Goal state before:
pp: case refine_1
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

Tactic:
exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ max a⁻¹ 1 = a⁻¹ * max a 1

Tactic:
eq_inv_mul_iff_mul_eq,

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a * max a⁻¹ 1 = max a 1
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx ↦ (toFun 𝔖) fx.1 fx.2) a ∈ SetRel.comp U U

Tactic:
filter_upwards [prod_mem_nhds (UniformOnFun.gen_mem_nhds _ _ _ hV hU)
    (inter_mem hVx <| hc <| UniformSpace.ball_mem_nhds _ hU)]
    with ⟨g, y⟩ ⟨hg, hyV, hy⟩ using ⟨toFun 𝔖 f y, hy, hg y hyV⟩

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

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

Tactic:
rw [disjoint_cocompact_right]

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

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
⊢ Tendsto (fun i ↦ f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
let : TopologicalSpace α := ⊥
  have : DiscreteTopology α := discreteTopology_bot α
  let : TopologicalSpace β := ⊥
  have : DiscreteTopology β := discreteTopology_bot β
  rw [← cocompact_eq_cofinite] at *
  exact tendsto_mul_cocompact_nhds_zero
    continuous_of_discreteTopology continuous_of_discreteTopology hf hg

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
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : g ∉ K * L⁻¹
a : G
ha : a ∈ K
h'a : a ∈ g • L
⊢ g ∈ K * L⁻¹

Tactic:
rcases h'a with ⟨b, bL, rfl⟩

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⁻¹
b : G
bL : b ∈ L
ha : (fun x ↦ g • x) b ∈ K
⊢ g ∈ K * L⁻¹
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
inst✝⁴ : Group G
inst✝³ : Monoid H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv G
f : G →* Hˣ
hf : Continuous[inst✝², inst✝¹] ⇑((Units.coeHom H).comp f)
⊢ Continuous[inst✝², instTopologicalSpaceMulOpposite] fun x ↦ op ↑(f x)⁻¹

Tactic:
← map_inv

Goal state after:
G : Type w
H : Type x
inst✝⁴ : Group G
inst✝³ : Monoid H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv G
f : G →* Hˣ
hf : Continuous[inst✝², inst✝¹] ⇑((Units.coeHom H).comp f)
⊢ Continuous[inst✝², instTopologicalSpaceMulOpposite] fun x ↦ op ↑(f x⁻¹)
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x ↦ (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun x ↦ (x, f x / g x)) a))

Tactic:
simp_rw [comp_apply, hga, div_zero]

Goal state after:
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x ↦ (x, f x / g x)) (𝓝 a) (𝓝 (↿h (a, 0)))
Module: Mathlib.Order.OrdContinuous

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

Tactic:
simp only [iSup, hf.map_sSup' (range_nonempty g), ← range_comp]

Goal state after:
α : Type u
β : Type v
ι : Sort x
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
inst✝ : Nonempty ι
g : ι → α
⊢ sSup (range (f ∘ g)) = sSup (range fun i ↦ f (g i))
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z : (i : ι) → α i
⊢ (Icc x z \ univ.pi fun i ↦ Ioc (y i) (z i)) ⊆ ⋃ i, Icc x (update z i (y i))

Tactic:
rintro a ⟨⟨hax, haz⟩, hay⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z a : (i : ι) → α i
hay : a ∉ univ.pi fun i ↦ Ioc (y i) (z i)
hax : x ≤ a
haz : a ≤ z
⊢ a ∈ ⋃ i, Icc x (update z i (y i))
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 : α ≃ β
⊢ ⇑e '' univ = univ

Tactic:
image_univ,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
⊢ range ⇑e = univ
Module: Mathlib.Topology.PartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : PartialHomeomorph X Y
e : X ≃ₜ Y
⊢ ⇑e '' univ = univ

Tactic:
image_univ,

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : PartialHomeomorph X Y
e : X ≃ₜ Y
⊢ range ⇑e = univ
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X Y
e : X ≃ₜ Y
⊢ ⇑e '' univ = univ

Tactic:
image_univ,

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X Y
e : X ≃ₜ Y
⊢ range ⇑e = univ
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[ts] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s

Tactic:
t.topology_eq_generate_intervals

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[Preorder.topology α] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case ht
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
⊢ IsOpen[ts] (⋂ a ∈ g, Iio a)

Tactic:
apply hg_fin.isOpen_biInter (fun i hi ↦ ?_)
      rw [h]
      exact isOpen_generateFrom_of_mem ⟨i, hgc hi, Or.inr rfl⟩

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

Goal state before:
pp: α : 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
⊢ induced f inst✝¹ = Preorder.topology α

Tactic:
let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
  refine le_antisymm (induced_topology_le_preorder hf) ?_
  refine le_of_nhds_le_nhds fun a => ?_
  simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]
  refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)
  · 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)
  · by_cases! h : ∃ x, ¬(f x < b)
    · 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 => (hf.2 hz).trans_le hyb)
    · exact le_principal_iff.2 (univ_mem' h)

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

Goal state before:
pp: case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl✝ : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : (AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a))) 1 = 0
⊢ a = 0

Tactic:
AddMonoidHom.coe_toIntLinearMap,

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a)) 1 = 0
⊢ a = 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | ∃ y, x ⋖ y}.Countable

Tactic:
by
  nontriviality α
  let s := { x : α | ∃ y, x ⋖ y }
  have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id
  choose! y hy using this
  have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x := fun x z hx => (hy x hx).le_of_lt
  suffices H : ∀ a : Set α, IsOpen a → Set.Countable { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } by
    have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by
      rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
      exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
    refine Set.Countable.mono this ?_
    refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_
    exact isOpen_of_mem_countableBasis ha
  intro a ha
  suffices H : Set.Countable { x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x } from
    H.of_sdiff (subsingleton_isBot α).countable
  simp only [and_assoc]
  let t := { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x }
  have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by
    intro x hx
    apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
    simpa only [IsBot, not_forall, not_le] using hx.right.right.right
  choose! z hz h'z using this
  have : PairwiseDisjoint t fun x => Ioc (z x) x := fun x xt x' x't hxx' => by
    rcases hxx'.lt_or_gt with (h' | h')
    · refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_
      refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')
    · refine disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_
      refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')
  refine this.countable_of_isOpen (fun x hx => ?_) fun x hx => ⟨x, hz x hx, le_rfl⟩
  suffices H : Ioc (z x) x = Ioo (z x) (y x) by rw [H]; exact isOpen_Ioo
  apply (Ioc_subset_Ioo_right (hy x hx.1).lt).antisymm
  simp_rw [subset_def, mem_Ioo, mem_Ioc]
  exact fun u hu ↦ ⟨hu.1, Hy _ _ hx.1 hu.2⟩

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)
inst✝ : Archimedean 𝕜
a : AddCircle p
⊢ ∃ b ∈ Ioc 0 p, ↑b = a

Tactic:
let b := QuotientAddGroup.equivIocMod hp.out 0 a
  exact ⟨b.1, by simpa only [zero_add] using b.2,
    (QuotientAddGroup.equivIocMod hp.out 0).symm_apply_apply a⟩

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
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0

Tactic:
by
  rw [← comp_τ₁, S.w₁₃, zero_τ₁]

Goal state after: