mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this : Nonempty α
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
have : Nonempty β := ⟨b⟩

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this✝ : Nonempty α
this : Nonempty β
⊢ IsClosed (f ⁻¹' Iic b)
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Tactic:
rw [mem_closure_iff_iSup]
  constructor
  · rintro ⟨ι, _, f, hf, rfl⟩
    exact ⟨_, by simp, bfamilyOfFamily f, fun i hi ↦ hf .., bsup_eq_iSup f⟩
  · rintro ⟨o, ho, f, hf, rfl⟩
    exact ⟨_, by simpa, familyOfBFamily _ f, fun i ↦ hf .., iSup_eq_bsup f⟩

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

Goal state before:
pp: b o : Ordinal.{u_1}
| o

Tactic:
rw [← CNF.foldr b o]

Goal state after:
b o : Ordinal.{u_1}
| foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
x : Ordinal.{u_1}
⊢ b ^ a.1 * (coeff b o) a.1 + x = b ^ a.1 * a.2 + x

Tactic:
coeff_of_mem_CNF ha

Goal state after:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
x : Ordinal.{u_1}
⊢ b ^ a.1 * a.2 + x = b ^ a.1 * a.2 + x
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x y : ZFSet.{u}
h : x ≠ y
⊢ {x, y}.card = 2

Tactic:
by
  convert! card_insert (notMem_singleton.2 h)
  rw [card_singleton, one_add_one_eq_two]

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

Goal state before:
pp: case mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
induction eb : B b with | _ δ Δ
     =>  _ 

Goal state after:
case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.lt
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'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
rw [← add_assoc, @add_of_omega0_opow_le _ (repr e') (ω ^ repr e' * (n' : ℕ))]

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'
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr

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'
⊢ ω ^ e'.repr ≤ ω ^ e'.repr * ↑↑n'
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
⊢ x ∈ ⋃ (i : α), f i ↔ ∃ i, x ∈ f i

Tactic:
simp [iUnion]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (V_ o).IsTransitive

Tactic:
rw [vonNeumann]
  exact .iUnion fun ⟨a, _⟩ => (isTransitive_vonNeumann a).powerset

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

Goal state before:
pp: case inl
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z w
hyw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w

Tactic:
exact hyw

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n : ℕ
R : Type u_3
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : n.AtLeastTwo
a : A
⊢ n.rawCast • a = n.rawCast * a

Tactic:
simp [Nat.cast_smul_eq_nsmul]

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

Goal state before:
pp: β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = none
⊢ Seq.corec (fun a ↦ Option.map (fun x ↦ ((x.1, x.2.1), x.2.2)) (f a)) b = Seq.nil

Tactic:
Seq.corec_nil

Goal state after:
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = none
⊢ Seq.nil = Seq.nil

case h
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = none
⊢ Option.map (fun x ↦ ((x.1, x.2.1), x.2.2)) (f b) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
⊢ FriendlyOperation op

Tactic:
let motive' (op : Seq α → Seq α) : Prop :=
    ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
⊢ FriendlyOperation op
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons.rel.h.h_firstIsPos
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ FirstNonzeroIsPos ((exp2 - exp1) :: mul m2 (inv m1))

Tactic:
· apply FirstNonzeroIsPos.of_head
        grind

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

Goal state before:
pp: case succ.inl
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
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'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
s t : Stream'.Seq α
base : motive s t
step : s = t
⊢ dist s t ≤ 2⁻¹ ^ (n + 1)

pp: case succ.inr
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
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'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
hd : α
u v : Stream'.Seq α
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ dist (Seq.cons hd (op c u)) (Seq.cons hd (op c v)) ≤ 2⁻¹ ^ (n + 1)

Tactic:
· simp [step]

Goal state after:
case succ.inr
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
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'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
hd : α
u v : Stream'.Seq α
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ dist (Seq.cons hd (op c u)) (Seq.cons hd (op c v)) ≤ 2⁻¹ ^ (n + 1)
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: p q : AndKind
⊢ Ordering

Tactic:
cases p <;> cases q

Goal state after:
case and.and
⊢ Ordering

case and.iff
⊢ Ordering

case and.eq
⊢ Ordering

case iff.and
⊢ Ordering

case iff.iff
⊢ Ordering

case iff.eq
⊢ Ordering

case eq.and
⊢ Ordering

case eq.iff
⊢ Ordering

case eq.eq
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: p q : IProp
⊢ Ordering

Tactic:
cases p <;> cases q

Goal state after:
case var.var
a✝¹ a✝ : Nat
⊢ Ordering

case var.true
a✝ : Nat
⊢ Ordering

case var.false
a✝ : Nat
⊢ Ordering

case var.and'
a✝³ : Nat
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case var.or
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

case var.imp
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

case true.var
a✝ : Nat
⊢ Ordering

case true.true
⊢ Ordering

case true.false
⊢ Ordering

case true.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case true.or
a✝¹ a✝ : IProp
⊢ Ordering

case true.imp
a✝¹ a✝ : IProp
⊢ Ordering

case false.var
a✝ : Nat
⊢ Ordering

case false.true
⊢ Ordering

case false.false
⊢ Ordering

case false.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case false.or
a✝¹ a✝ : IProp
⊢ Ordering

case false.imp
a✝¹ a✝ : IProp
⊢ Ordering

case and'.var
a✝³ : AndKind
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case and'.true
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.false
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.and'
a✝⁵ : AndKind
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.or
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case and'.imp
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case or.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case or.true
a✝¹ a✝ : IProp
⊢ Ordering

case or.false
a✝¹ a✝ : IProp
⊢ Ordering

case or.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case or.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case or.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case imp.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case imp.true
a✝¹ a✝ : IProp
⊢ Ordering

case imp.false
a✝¹ a✝ : IProp
⊢ Ordering

case imp.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case imp.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case imp.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩

Goal state after:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℤ
hb : a = b * b
⊢ n = 0
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
refine ⟨fun h' ↦ by simp [h.1, h'], fun ⟨b, hb⟩ ↦ ?_⟩

Goal state after:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℚ
hb : a = b * b
⊢ n = 0
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case pos
d : ℕ
q : ℚ
hq : 0 ≤ q
ha : ↑1 / ↑0 = q ^ d
⊢ ∃ x, 1 = x ^ d

Tactic:
use 1

Goal state after:
case h
d : ℕ
q : ℚ
hq : 0 ≤ q
ha : ↑1 / ↑0 = q ^ d
⊢ 1 = 1 ^ d
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ False

Tactic:
div_eq_div_iff

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a * ↑y ^ d = ↑x ^ d * ↑b
⊢ False

case neg.hb
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ ↑b ≠ 0

case neg.hd
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ ↑y ^ d ≠ 0
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioo 1 2 = ∅

Tactic:
by simp only [Ioo_ofNat_ofNat]

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

Goal state before:
pp: ⊢ Ioo 1 3 = {2}

Tactic:
by simp only [Ioo_ofNat_ofNat]

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

Goal state before:
pp: ⊢ Ioo 1 4 = {2, 3}

Tactic:
by simp only [Ioo_ofNat_ofNat]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
use etaFn G origin

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⋯
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := ⋯
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ etaFn G origin ∈ U ∩ Set.range (etaFn G)
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✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
⊢ CompactSpace ↑(closure[inst✝¹] s)

Tactic:
have : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous (eval x ∘ F) := fun K hK x hx ↦
    UniformOnFun.uniformContinuous_eval_of_mem _ _ hx hK |>.continuous.comp F_clemb.continuous

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous[inst✝¹, inst✝².toTopologicalSpace] (eval x ∘ F)
⊢ CompactSpace ↑(closure[inst✝¹] s)
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ (DenseRange fun x_1 ↦ x ^ x_1) ↔ DenseRange fun x_1 ↦ x ^ x_1

Tactic:
by
  simp only [DenseRange, dense_iff_closure_eq, closure_range_zpow_eq_pow]

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

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
this : (c * c ^ k) • w ∈ c • V
⊢ c ^ k • w ∈ V

Tactic:
mul_smul,

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
this : c • c ^ k • w ∈ c • V
⊢ c ^ k • w ∈ V
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:
rintro H rfl

Goal state after:
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
H : IsOpen ↑⊥
⊢ False
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
⊢ IsClosed[t] A

Tactic:
by
    apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell
      (subset_trans hA (subset_complex (C := C) E)) h.2
    intro n _ j
    by_cases hj : j ∈ E.I n
    · exact Or.intro_right _ (h.1 n ⟨j, hj⟩)
    · exact Or.intro_left _ ((disjoint_openCell_subcomplex_of_not_mem E hj).symm.mono_left hA)

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x : ↑(π C fun x ↦ x ∈ s)
a : I
hx : ↑x a = true
⊢ e (π C fun x ↦ x ∈ s) a ∈ factors C s x

Tactic:
rcases x with ⟨_, z, hz, rfl⟩
  simp only [factors, List.mem_map, Finset.mem_sort]
  refine ⟨a, ?_, if_pos hx⟩
  aesop (add simp Proj)

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

Goal state before:
pp: case right
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ IsClosed[t] D

Tactic:
exact isClosedBase C

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

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 1

pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 0

Tactic:
· simp only [List.map_map]
    apply List.prod_eq_one
    simp only [List.mem_map, Function.comp_apply]
    rintro _ ⟨i, hi, rfl⟩
    exact if_pos (h i hi)

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
⊢ isGood (π C fun x ↦ ord I x < o) l ↔ ∃ o' < o, isGood (π C fun x ↦ ord I x < o') l

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨o', ⟨ho', hl⟩⟩ ↦ isGood_mono C (le_of_lt ho') hl⟩
  use Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a))
  have hslt : Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) < o := by
    simp only [Finset.sup_lt_iff ho.bot_lt, List.mem_toFinset]
    exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)
  refine ⟨hslt, fun he ↦ h ?_⟩
  have hlt : ∀ i ∈ l.val, ord I i < Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) := by
    intro i hi
    simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]
    exact ⟨i, hi, le_rfl⟩
  rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]

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

Goal state before:
pp: case hDA
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
this : D ⊆ E
⊢ IsClosed[t] D

Tactic:
exact isClosedBase C

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case neg
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ ⋂ n, dissipate C n = ∅
f : ∃ n, dissipate C n ∉ S
⊢ ∃ n, dissipate C n = ∅

Tactic:
obtain ⟨n, hn⟩ := f
      exact ⟨n, by simpa [hn] using this.1 n⟩

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
x✝¹ : f.NeBot
x✝ : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
a : E
ha : a ∈ A
hxa : MapClusterPt a atTop x
⊢ ∃ a ∈ A, ClusterPt a f

Tactic:
exact ⟨a, ha, hxa.clusterPt.mono hx⟩

Goal state after: