mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.lt.h₁
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝² : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝¹ : e.NF
this✝ : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this : (e.oadd n a).repr < ω ^ e'.repr
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr

Tactic:
simp only [repr] at this

Goal state after:
case oadd.lt.h₁
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝² : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝¹ : e.NF
this✝ : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ e'.repr
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o a : Ordinal.{u}
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o

Tactic:
obtain h | h := lt_or_ge o (invVeblen₁ a)
  · rw [veblen_eq_of_lt_invVeblen₁ h]
    simpa
  · simpa [(lt_veblen_invVeblen₁ a).trans_le (veblen_left_monotone _ h)]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ x.powerset.rank ≤ succ x.rank

Tactic:
simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]

Goal state after:
case a
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank ≤ x.rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ⨆ i, (f i).rank ≤ (⋃ (i : α), f i).rank

Tactic:
exact Ordinal.iSup_le fun i => rank_mono (subset_iUnion f i)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.refine_1
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
⊢ a'.NFBelow (e - 1).repr

Tactic:
simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢
        refine IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <|
          (le_self_add (α := Ordinal) (b := m')).trans_lt ?_
        rw [← this, ← IH₂]
        exact h.snd'.repr_lt

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k : ℕ
⊢ ∀ (m : ℕ), (e.opowAux a0 a k m).NF

Tactic:
m

Goal state after:
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (e.opowAux a0 a k m).NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
| Tendsto (fun t ↦ f t ^ (exp - exp')) atTop (𝓝 0)

Tactic:
arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
| (fun t ↦ t ^ (-(exp' - exp))) ∘ f
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ f_exp + ε > f_exp

Tactic:
dsimp [ε]

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ g_exp + ε > g_exp

Tactic:
dsimp [ε]

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
t : ℝ
hx : 0 < b t
⊢ exp = f_exp + ε + (g_exp + ε)

Tactic:
dsimp [ε]

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
t : ℝ
hx : 0 < b t
⊢ exp = f_exp + (exp - f_exp - g_exp) / 2 + (g_exp + (exp - f_exp - g_exp) / 2)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
c : ℝ
⊢ (Multiseries.const basis_hd basis_tl c).Sorted

Tactic:
by
  simp only [Multiseries.const]
  exact const_sorted.cons_nil

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
n : ℕ
r : ℝ
⊢ (monomialRpow (basis_hd :: basis_tl) n r).seq = Multiseries.monomialRpow basis_hd basis_tl n r

Tactic:
by
  simp [monomialRpow]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
have h_equiv : Real.log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop]
      exps_hd • Real.log ∘ basis_hd :=
    (toLogFun_isEquivalent_of_nonzero_head h_basis h_nonzero.ne').congr_left
      (log_toFun_eq_toLogFun h_basis).symm
  suffices h_log : Tendsto (Real.log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl))
      atTop atTop by
    apply Filter.Tendsto.congr' _ (Real.tendsto_exp_atTop.comp h_log)
    apply (toFun_pos (m := (exps_hd :: exps_tl)) h_basis).mono
    intro x hx
    simp only [Function.comp_apply]
    exact Real.exp_log hx
  apply IsEquivalent.tendsto_atTop h_equiv.symm
  apply Filter.Tendsto.const_mul_atTop h_nonzero
  apply Tendsto.comp Real.tendsto_log_atTop
  exact h_basis.tendsto_atTop (by simp)

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_coef : t.coef = 0
⊢ t.toFun basis = 0

Tactic:
by
  simp [toFun, h_coef]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
⊢ s = t

Tactic:
suffices dist s t = 0 by simpa using this

Goal state after:
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
⊢ dist s t = 0
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case a
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 - 1 < n

Tactic:
obtain _ | n' := n
        · exact False.elim (h (by simp))
        · have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
          lia

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
⊢ ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.nil ∧
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ exp_1 coef_1 tl_1,
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp_1 coef_1 tl_1 ∧
        coef_1.Approximates ∧
          Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp_1 ∧
            motive
              (mk tl_1 (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp_1 * coef_1.toFun))

Tactic:
| cons exp coef tl g =>

Goal state after:
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑↑n / ↑↑d).num ∧ IsSquare (↑↑n / ↑↑d).den)

Tactic:
← Int.isSquare_natCast_iff (n := Rat.den _),

Goal state after:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑↑n / ↑↑d).num ∧ IsSquare ↑(↑↑n / ↑↑d).den)
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = b * x ^ d
⊢ x.Coprime y

Tactic:
simpa [hx'] using (show x'.natAbs.Coprime y from Rat.reduced q)

Goal state after:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ≥0
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
⊢ IsNNRat (sqrt x) sn sd

Tactic:
by
  obtain ⟨_, rfl⟩ := h
  refine ⟨?_, ?out⟩
  · apply invertibleOfNonzero
    rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]
    exact Invertible.ne_zero _
  · simp [← hn, ← hd, NNReal.sqrt_mul]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 0 = ∅

Tactic:
by simp only [Iio_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 1 = {0}

Tactic:
by simp only [Iio_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 2 = {0, 1}

Tactic:
by simp only [Iio_ofNat]

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = (UniformSpace.comap F (UniformFun.uniformSpace X α)).toTopologicalSpace ↔
    inst✝¹ = (UniformSpace.comap F (Pi.uniformSpace fun i ↦ α)).toTopologicalSpace

Tactic:
rw [F_eqcont.comap_uniformFun_eq]

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

Goal state before:
pp: case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
set 𝒢 : Filter S := comap (↑) (map F ℱ)

Goal state after:
case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (if (↑ab).2 ∈ {1} then e else 0) = f x

Tactic:
tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ (L (f (↑⟨(x, 1), ⋯⟩).1)) (if (↑⟨(x, 1), ⋯⟩).2 ∈ {1} then e else 0) = f x
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
⊢ LocallyCompactSpace (PontryaginDual H)

Tactic:
let Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
  have hVn : ∀ n x, x ∈ Vn n ↔ |Complex.arg x| < π / 2 ^ (n + 1) :=
    fun n x ↦ Circle.mem_centeredArc (z := x)
      (div_le_self pi_nonneg (one_le_pow₀ one_le_two))
  refine ContinuousMonoidHom.locallyCompactSpace_of_hasBasis Vn ?_ ?_
  · intro n x h1 h2
    rw [hVn] at h1 h2 ⊢
    rwa [Circle.coe_mul, Complex.arg_mul x.coe_ne_zero x.coe_ne_zero,
      ← two_mul, abs_mul, abs_two, ← lt_div_iff₀' two_pos, div_div, ← pow_succ] at h2
    apply Set.Ioo_subset_Ioc_self
    rw [← two_mul, Set.mem_Ioo, ← abs_lt, abs_mul, abs_two, ← lt_div_iff₀' two_pos]
    refine h1.trans_le ?_
    gcongr
    exact le_self_pow₀ one_le_two n.succ_ne_zero
  · simpa [Vn] using Circle.hasBasis_centeredArc_div_two_pow

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ IsOpen ↑I ↔ I ≠ ⊥

Tactic:
refine ⟨?_, IsDedekindDomain.isOpen_of_ne_bot⟩
  rintro H rfl
  have := discreteTopology_iff_isOpen_singleton_zero.mpr H
  exact hR (Finite.isField_of_domain R)

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ derivedSet a).Nonempty

Tactic:
exact ha

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
⊢ ∀ B ∈ C0, B.Nonempty

Tactic:
rintro B ⟨Q, hQ, rfl⟩

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
⊢ (X.str ⁻¹' Q).Nonempty
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
⊢ ∀ B ∈ C0, (AA ∩ B).Nonempty

Tactic:
rintro B ⟨Q, hQ, rfl⟩

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
⊢ (AA ∩ X.str ⁻¹' Q).Nonempty
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case inr
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
h : ∃ Q ∈ C0, P = AA ∩ Q
⊢ P.Nonempty

Tactic:
rcases h with ⟨Q, hQ, rfl⟩

Goal state after:
case inr
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
Q : Set (Ultrafilter X.A)
hQ : Q ∈ C0
hP : AA ∩ Q ∈ C2
⊢ (AA ∩ Q).Nonempty
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case inr
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
S : Set (Ultrafilter X.A)
hS : S ∈ T2
h : ∃ Q ∈ T0, S = AA ∩ Q
⊢ S.Nonempty

Tactic:
rcases h with ⟨Q, hQ, rfl⟩

Goal state after:
case inr
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
this : ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q
Q : Set (Ultrafilter X.A)
hQ : Q ∈ T0
hS : AA ∩ Q ∈ T2
⊢ (AA ∩ Q).Nonempty
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
by
  have := RelCWComplex.mapsTo n i
  simp_rw [empty_union] at this
  exact this

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mpr
X : Compactum
A : Set X.A
x✝ : X.A
F : Ultrafilter X.A
h1 : A ∈ F
h2 : ↑F ≤ 𝓝 x✝
⊢ x✝ ∈ cl A

Tactic:
exact ⟨F, h1, str_eq_of_le_nhds _ _ h2⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false) ∈ π C J

pp: case refine_2.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (iso_map C J) ⟨fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false, ?refine_2.refine_1⟩ = a

Tactic:
· rcases a with ⟨_, y, hy, rfl⟩
      exact ⟨y, hy, rfl⟩

Goal state after:
case refine_2.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (iso_map C J) ⟨fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false, ⋯⟩ = a
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
FF : Ultrafilter (Ultrafilter X)
x : X := (Ultrafilter.map Ultrafilter.lim FF).lim
c1 : x = (Ultrafilter.map Ultrafilter.lim FF).lim
c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen[inst✝²] U → U ∈ F
c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝²] U
this : Ultrafilter.lim ⁻¹' U ∈ FF
P : Ultrafilter X
hP : P ∈ Ultrafilter.lim ⁻¹' U
⊢ P ∈ {G | U ∈ G}

Tactic:
exact c2 U P hP hU

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    ext FF
    change Ultrafilter (Ultrafilter X) at FF
    set x := (Ultrafilter.map Ultrafilter.lim FF).lim with c1
    have c2 : ∀ (U : Set X) (F : Ultrafilter X), F.lim ∈ U → IsOpen U → U ∈ F := by
      intro U F h1 hU
      exact isOpen_iff_ultrafilter.mp hU _ h1 _ (Ultrafilter.le_nhds_lim _)
    have c3 : ↑(Ultrafilter.map Ultrafilter.lim FF) ≤ 𝓝 x := by
      rw [le_nhds_iff]
      intro U hx hU
      exact mem_coe.2 (c2 _ _ (by rwa [← c1]) hU)
    have c4 : ∀ U : Set X, x ∈ U → IsOpen U → { G : Ultrafilter X | U ∈ G } ∈ FF := by
      intro U hx hU
      suffices Ultrafilter.lim ⁻¹' U ∈ FF by
        apply mem_of_superset this
        intro P hP
        exact c2 U P hP hU
      exact @c3 U (IsOpen.mem_nhds hU hx)
    apply lim_eq
    rw [le_nhds_iff]
    exact c4

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j = ↑E

Tactic:
E.union'

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ E.carrier = ↑E
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h.false
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})

pp: case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true})

Tactic:
· refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)
      convert! C.2
      ext x
      simp

Goal state after:
case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true})