mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
R' : Type u_3
S' : Type u_4
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
flat : f.Flat
qR : R →+* R'
qS : S →+* S'
g : R' →+* S'
surjR : Function.Surjective ⇑qR
surjS : Function.Surjective ⇑qS
comm : qS.comp f = g.comp qR
sq0 : ker qR ^ 2 = ⊥
eqmap : ker qS = Ideal.map f (ker qR)
smoothq : g.FormallySmooth
algInst✝⁴ : Algebra R S := f.toAlgebra
algInst✝³ : Algebra R R' := qR.toAlgebra
algInst✝² : Algebra S S' := qS.toAlgebra
algInst✝¹ : Algebra R' S' := g.toAlgebra
algInst✝ : Algebra R S' := (qS.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝¹ : Module.Flat R S
algebraizeInst✝ : Algebra.FormallySmooth R' S'
x✝ : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq' comm
⊢ f.FormallySmooth

Tactic:
exact Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat surjR surjS eqmap sq0 ‹_›

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

Goal state before:
pp: o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ > a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
case =>

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

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
⊢ (match Ordering.eq, e₁, e₂ with
    | Ordering.lt, a, b => a < b
    | Ordering.eq, a, b => a = b
    | Ordering.gt, a, b => b < a) →
    (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
case =>

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ (insert x y).card ≤ y.card + 1

Tactic:
rw [← lift_le.{u + 1}]
  simpa [← cardinalMk_coe_sort] using! mk_insert_le

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

Tactic:
have := (h₁.below_of_lt ee).repr_lt
        simp only [repr] at this
        cases he' : e' <;>
          simp only [he', zero_def, opow_zero, repr, repr_zero, gt_iff_lt] at this ⊢ <;>
          exact lt_of_le_of_lt le_self_add this

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

Goal state before:
pp: ⊢ Function.Injective2 pair

Tactic:
intro x x' y y' H

Goal state after:
x x' y y' : ZFSet.{u_1}
H : x.pair y = x'.pair y'
⊢ x = x' ∧ y = y'
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ z✝ ∈ ⋃₀ x

Tactic:
rw [mem_sUnion]

Goal state after:
x z : PSet.{u_1}
a✝¹ : z ∈ x
z✝ : PSet.{u_1}
a✝ : z✝ ∈ z
⊢ ∃ z ∈ x, z✝ ∈ z
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x z : ZFSet.{u_1}
a✝¹ : z ∈ x
x✝ : ZFSet.{u_1}
a✝ : x✝ ∈ z
⊢ x✝ ∈ ⋃₀ x

Tactic:
rw [mem_sUnion]

Goal state after:
x z : ZFSet.{u_1}
a✝¹ : z ∈ x
x✝ : ZFSet.{u_1}
a✝ : x✝ ∈ z
⊢ ∃ z ∈ x, x✝ ∈ z
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
have IH : repr (mul _ _) = _ := @repr_mul _ _ h₁ h₂.snd

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
p : (e.oadd n a).split' = (o', m)
⊢ o'.NF ∧ (e.oadd n a).repr = ω * o'.repr + ↑m

Tactic:
by_cases e0 : e = 0 <;>
      simp only [split', e0, ↓reduceIte, Prod.mk.injEq, repr, repr_zero, opow_zero, one_mul] at p ⊢

Goal state after:
case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ ↑n = m
⊢ o'.NF ∧ ↑↑n + a.repr = ω * o'.repr + ↑m

case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a b : A
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
simp [ha, hb]

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

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : m = 0
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, One.one, *]

Goal state after:
case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
h : m = 0
⊢ (zero.oadd ⟨1, ⋯⟩ zero).NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case cons.inr
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
h :
  ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
exact .trans (by grind) h_comp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
⊢ ∃ f,
    ∀ (b : β),
      match F b with
      | none => f b = nil
      | some (a, c, b') => f b = Seq.cons a (op c (f b'))

Tactic:
obtain ⟨f, hf⟩ := exists_fixed_point_of_contractible T hT

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
⊢ ∃ f,
    ∀ (b : β),
      match F b with
      | none => f b = nil
      | some (a, c, b') => f b = Seq.cons a (op c (f b'))
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
have aa : repr (a' + ofNat m) = repr a' + m := by
      simp only [ONote.repr_ofNat, ONote.repr_add]

Goal state after:
case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ (fun a ↦ m.inv.toFun basis a) =ᶠ[atTop] fun a ↦ (fun a ↦ m.toFun basis a)⁻¹ a

Tactic:
simp only [toFun, inv, Pi.inv_apply]

Goal state after:
m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) m) basis).prod) =ᶠ[atTop] fun a ↦
    (List.zipWith (fun exp b ↦ b a ^ exp) m basis).prod⁻¹
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
lhs; lhs; rw [eq_mk ms]

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| mk ms.seq ms.toFun
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.h_Pairwise.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
h_comp : Multiseries.nil.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk Multiseries.nil 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk Multiseries.nil 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef Multiseries.nil) 0).seq

Tactic:
exact Seq.Pairwise_cons_nil

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl : tl.Sorted
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
cases h_tl with

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

Goal state before:
pp: case step.left.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h : motive (Seq.cons (exp, coef) Seq.nil)
h_tl : (tl_exp, tl_coef) ∈ Seq.nil.head
h_step : leadingExp Seq.nil < ↑exp
⊢ tl_exp < exp

Tactic:
simp [leadingExp, head] at h_tl h_step

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

Goal state before:
pp: case step.left.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x✝ : ℝ × MultiseriesExpansion basis_tl
s✝ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x✝ s✝))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x✝ s✝).head
h_step : leadingExp (Seq.cons x✝ s✝) < ↑exp
⊢ tl_exp < exp

Tactic:
simp [leadingExp, head] at h_tl h_step

Goal state after:
case step.left.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x✝ : ℝ × MultiseriesExpansion basis_tl
s✝ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x✝ s✝))
h_tl : x✝ = (tl_exp, tl_coef)
h_step : x✝.1 < exp
⊢ tl_exp < exp
Module: Mathlib.Tactic.DeriveEncodable

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

Tactic:
unfold S.encode
      rw [← h, Nat.pair_unpair]

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

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
h_neg : (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).leadingExp < 0
h_approx : (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).Approximates
⊢ Tendsto (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).toFun atTop (𝓝 0)

Tactic:
obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
    simp only [leadingExp_def, mk_seq, Multiseries.leadingExp_cons, WithBot.coe_lt_zero] at h_neg
    exact Majorized.tendsto_zero_of_neg h_neg h_maj

Goal state after:
Module: Mathlib.Tactic.ITauto

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

Tactic:
case =>

Goal state after:
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: ⊢ Ordering

Tactic:
case =>

Goal state after:
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: ap : AndKind
p₁ p₂ : IProp
aq : AndKind
q₁ q₂ : IProp
⊢ Ordering

Tactic:
case =>

Goal state after:
Module: Mathlib.Tactic.ITauto

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

Tactic:
case =>

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

Goal state before:
pp: a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
⊢ ¬IsSquare a

Tactic:
rw [ha.neg_to_eq rfl rfl]
  rintro ⟨q, hq⟩
  refine absurd hq (ne_of_lt ?_)
  calc
    -(n / d : ℚ) < 0 := by rw [Left.neg_neg_iff]; apply div_pos <;> simpa [Nat.pos_iff_ne_zero]
    _ ≤ q * q := mul_self_nonneg _

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

Goal state before:
pp: case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_odd : Odd d
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
· contrapose hq
    rw [← h_odd.pow_nonneg_iff, ← hq]
    positivity

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✝ : 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)
cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K
cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ closure[inst✝¹] s ⊆ {i | F i x ∈ Q}
K : Set X
hK : K ∈ 𝔖
x : X
hx : x ∈ K
Q : Set α
hQ : IsCompact Q ∧ closure[inst✝¹] s ⊆ {i | F i x ∈ Q}
⊢ ∀ (i : ↑(closure[inst✝¹] s)), F (↑i) x ∈ Q

Tactic:
simpa using! hQ.2

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✝ : 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
⊢ IsCompact (closure[inst✝¹] s)

Tactic:
rw [isCompact_iff_compactSpace]
  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
  have cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ ((↑) : closure s → ι)) K :=
    fun K hK ↦ (s_eqcont K hK).closure' <| show Continuous (K.domRestrict ∘ F) from
      continuous_pi fun ⟨x, hx⟩ ↦ this K hK x hx
  have cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ closure s ⊆ {i | F i x ∈ Q} :=
    fun K hK x hx ↦ (s_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, closure_minimal hQ.2 <|
      hQ.1.isClosed.preimage (this K hK x hx)⟩
  exact ArzelaAscoli.compactSpace_of_isClosedEmbedding 𝔖_compact
    (F_clemb.comp isClosed_closure.isClosedEmbedding_subtypeVal) cls_eqcont
    fun K hK x hx ↦ (cls_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, by simpa using! hQ.2⟩

Goal state after:
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 y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
tfae_4_to_1 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → MapClusterPt x atTop fun x ↦ y ^ x
⊢ (MapClusterPt x atTop fun x ↦ y ^ x) → ClusterPt x (𝓟 (range fun x ↦ y ^ x))

Tactic:
exact (ClusterPt.mono · (le_principal_iff.2 range_mem_map))

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ TopologicalSpace.induced (⇑e.symm.toHomeomorph) inst =
    TopologicalSpace.induced (fun x1 x2 ↦ (B' x1) x2) Pi.topologicalSpace

Tactic:
apply congr(TopologicalSpace.induced e.symm $(hB.eq_induced)).trans

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ TopologicalSpace.induced (⇑e.symm) (TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace) =
    TopologicalSpace.induced (fun x1 x2 ↦ (B' x1) x2) Pi.topologicalSpace
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
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
Vn : ℕ → Set Circle := ⋯
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ (↑x).arg + (↑x).arg ∈ Set.Ioo (-π) π

Tactic:
rw [← two_mul, Set.mem_Ioo, ← abs_lt, abs_mul, abs_two, ← lt_div_iff₀' two_pos]

Goal state after:
case refine_1
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
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑x * ↑x).arg| < π / 2 ^ (n + 1)
⊢ |(↑x).arg| < π / 2
Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ LocallyPathConnectedSpace X

Tactic:
rw [← IsGeneratedBy.generatedBy_eq (X := fun n ↦ Fin n → ℝ) (Y := X),
    generatedBy_eq_coinduced]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ LocallyPathConnectedSpace X
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
Q : Set X.A
hQ : Q ∈ F
q : X.A
hq1 : q ∈ Q
P : Ultrafilter X.A
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q

Tactic:
rw [← hq3] at hq1

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
q : X.A
P : Ultrafilter X.A
hq1 : X.str P ∈ Q
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: ⊢ CreatesLimits (forget Profinite)

Tactic:
change CreatesLimits (profiniteToCompHaus ⋙ forget _)
  infer_instance

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
⊢ ⇑(eval (π C J) l) ∘ ProjRestrict C J = ⇑(eval C l)

Tactic:
by
  ext x
  dsimp only [ProjRestrict, Function.comp_apply]
  rw [Products.eval_eq, Products.eval_eq]
  simp +contextual [h, Proj]

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun a ↦ if ord I i = o then true else a i

Tactic:
apply Continuous.comp'

Goal state after:
case hg
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (ite (ord I i = o) true)

case hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x ↦ x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

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

Tactic:
rintro ⟨⟩

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

case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑C
⊢ (Products.eval C ↑l) x✝ = ((πs C o) (eval (π C fun x ↦ ord I x < o) l)) x✝

Tactic:
← Products.eval_πs C (Products.prop_of_isGood _ _ l.prop)

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑C
⊢ ((πs C o) (Products.eval (π C fun x ↦ ord I x < o) ↑l)) x✝ = ((πs C o) (eval (π C fun x ↦ ord I x < o) l)) x✝
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ Disjoint (↑(skeletonLT C n)) (openCell m j)

Tactic:
← iUnion_openCell_eq_skeletonLT,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ Disjoint (D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j) (openCell m j)