mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this✝ : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ (C
        (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) -
            a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
          nthRemainder p n bs (truncateFun (n + 1) a₂))).degree <
    (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree

Tactic:
apply lt_of_le_of_lt degree_C_le

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this✝ : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 0 < (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inl
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : y.length ≤ x.length
⊢ y ∈ ↑T

pp: case inr
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : x.length ≤ y.length
⊢ y ∈ ↑T

Tactic:
· rw [mem_pullSub_short h'] at h; exact mem_of_prefix h.1 (by simpa using h.2)

Goal state after:
case inr
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : x.length ≤ y.length
⊢ y ∈ ↑T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : List A
⊢ pullSub (subAt T x) x ≤ T

Tactic:
intro y (h : y ∈ pullSub _ x); rcases le_total y.length x.length with h' | h'
  · rw [mem_pullSub_short h'] at h; exact mem_of_prefix h.1 (by simpa using h.2)
  · rw [mem_pullSub_long h'] at h; obtain ⟨_, h, rfl⟩ := h; exact h

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ f (lfpApprox f x a) ≤ lfpApprox f x b

Tactic:
nth_rw 2 [lfpApprox]
  exact le_sup_of_le_right <| le_iSup₂_of_le a h le_rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : l₂ ~ l₃
⊢ atom a ~ l₃

Tactic:
rwa [← equiv_atom.1 h₁] at h₂

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

Goal state before:
pp: case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : ↑a = ↑b
⊢ False

Tactic:
Subtype.coe_inj

Goal state after:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : a = b
⊢ False
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (map Prod.toSigma (CNF b o)).keys.Nodup

Tactic:
List.keys,

Goal state after:
b o : Ordinal.{u_1}
⊢ (map Sigma.fst (map Prod.toSigma (CNF b o))).Nodup
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
h : IsMin a
⊢ 𝓝 a = pure a

Tactic:
rw [nhds_eq_pure, isSuccLimit_iff]
  tauto

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

Goal state before:
pp: o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ IsClosedBelow (⋂₀ S) o

Tactic:
by
  rw [isClosedBelow_iff]
  exact fun p plto pAcc C CmemS ↦ (h C CmemS).forall_lt p plto <|
    AccPt.mono pAcc (monotone_principal (sInter_subset_of_mem CmemS))

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
⊢ veblenWith f o₁ a = a

Tactic:
obtain rfl | h := h.eq_or_lt

Goal state after:
case inl
f : Ordinal.{u} → Ordinal.{u}
o₁ a : Ordinal.{u}
hf : IsNormal f
h : o₁ ≤ o₁
h' : veblenWith f o₁ a = a
⊢ veblenWith f o₁ a = a

case inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h✝ : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
h : o₁ < o₂
⊢ veblenWith f o₁ a = a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case mpr.inl
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a b : Ordinal.{u}
ha : veblenWith f b a = a
hb : b < b + 1
⊢ a ∈ Function.fixedPoints (veblenWith f ↑⟨b, hb⟩)

Tactic:
rw [Function.mem_fixedPoints_iff, ha]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ 0 < veblenWith f o₁ (veblenWith f o₂ 0)

Tactic:
veblenWith_lt_veblenWith_iff_right hf

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ 0 < veblenWith f o₂ 0
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
a' : Ordinal.{0}
e0 : e.repr ≠ 0
h : a' < ω ^ e.repr
aa : a.repr = a'
n : ℕ+
⊢ (ω ^ e.repr * ↑↑n + a') ^ ω = (ω ^ e.repr) ^ ω

Tactic:
by
  subst aa
  have No := Ne.oadd n (Na.below_of_lt' h)
  have := omega0_le_oadd e n a
  rw [repr] at this
  refine le_antisymm ?_ (opow_le_opow_left _ this)
  apply (opow_le_of_isSuccLimit ((opow_pos _ omega0_pos).trans_le this).ne' isSuccLimit_omega0).2
  intro b l
  have := (No.below_of_lt (lt_succ _)).repr_lt
  rw [repr] at this
  apply (opow_le_opow_left b <| this.le).trans
  rw [← opow_mul, ← opow_mul]
  rcases le_or_gt ω (repr e) with h | h
  · grw [le_succ b, succ_eq_add_one, add_mul_succ _ (one_add_of_omega0_le h)]
    · gcongr
      · exact omega0_pos
      · exact succ_le_iff.2 <| by gcongr; exact isSuccLimit_omega0.succ_lt l
    · exact omega0_pos
  · grw [show _ * _ < _ from isPrincipal_mul_omega0 (isSuccLimit_omega0.succ_lt h) l]
    · simpa using mul_le_mul_left (one_le_iff_ne_zero.2 e0) ω
    · exact omega0_pos

Goal state after:
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 * g) =o[atTop] (b ^ exp)

Tactic:
specialize hf (f_exp + ε) (by dsimp [ε]; linarith)

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 + ε))
⊢ (f * g) =o[atTop] (b ^ 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 + (exp - f_exp - g_exp) / 2 + (g_exp + (exp - f_exp - g_exp) / 2)

Tactic:
ring_nf

Goal state after:
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 : ℝ → ℝ
⊢ mk ms.seq ms.toFun = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
mk_eq_mk_iff

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ ms.seq = s ∧ ms.toFun = f ↔ ms.seq = s ∧ ms.toFun = f
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
h_allZero : AllZero (exps_hd :: exps_tl)
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 1)

Tactic:
simp at h_allZero

Goal state after:
case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
f : ℝ → ℝ
h_coef : coef.Sorted
⊢ (mk (Multiseries.cons exp coef Multiseries.nil) f).Sorted

Tactic:
simp [Multiseries.Sorted.cons_nil h_coef]

Goal state after:
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

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

case a.succ
n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
⊢ (Nat.unpair (n' + 1)).1 - 1 < n' + 1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.none.succ
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ 1 * ↑m' + 1 + 1 = succ (1 * ↑m' + 1) ∧ ((oadd 0 (m' + 1).succPNat 0).NF → (oadd 0 m'.succPNat 0).NF)

Tactic:
exact ⟨rfl, inferInstance⟩

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

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ (a'.oadd i.succPNat 0).repr < ω ^ a.repr

Tactic:
repr,

Goal state after:
case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat + repr 0 < ω ^ a.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ((f i).oadd 1 0).repr < ω ^ a.repr

Tactic:
repr,

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ (f i).repr * ↑↑1 + repr 0 < ω ^ a.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.some.refine_1
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr

Tactic:
repr,

Goal state after:
case oadd.inl.some.refine_1
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ ω ^ a.repr * ↑↑m + b.repr = succ (a.oadd m b').repr
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = as₁.reverseAux as → (mk as✝).implies p as as₁.length → p
as₁ : List Prop
⊢ as✝ = as₁.reverseAux (a :: as) → (mk as✝).implies p (a :: as) as₁.length → p

Tactic:
refine fun e H ↦ @ih (a::as₁) e (H ?_)

Goal state after:
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = as₁.reverseAux as → (mk as✝).implies p as as₁.length → p
as₁ : List Prop
e : as✝ = as₁.reverseAux (a :: as)
H : (mk as✝).implies p (a :: as) as₁.length
⊢ mk as✝ as₁.length ↔ a
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 ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
⊢ CompactSpace ι

Tactic:
by
  -- By equicontinuity, we know that the topology on `ι` is also the one induced by
  -- `domRestrict (⋃₀ 𝔖) ∘ F`.
  have : IsInducing (domRestrict (⋃₀ 𝔖) ∘ F) := by
    rwa [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont] at F_ind
  -- Thus, we just have to check that the range of this map is compact.
  rw [← isCompact_univ_iff, this.isCompact_iff, image_univ]
  -- But then we are working in a product space, where compactness can easily be proven using
  -- Tykhonov's theorem! More precisely, for each `x ∈ ⋃₀ 𝔖`, choose a compact set `Q x`
  -- containing all `F i x`s.
  rw [← forall_sUnion] at F_pointwiseCompact
  choose! Q Q_compact F_in_Q using F_pointwiseCompact
  -- Notice that, since the range of `F` is closed in `X →ᵤ[𝔖] α`, equicontinuity ensures that
  -- the range of `(⋃₀ 𝔖).domRestrict ∘ F` is still closed in the product topology.
  -- But it's contained in the product of the `Q x`s, which is compact by Tykhonov, hence
  -- it is compact as well.
  refine IsCompact.of_isClosed_subset (isCompact_univ_pi fun x ↦ Q_compact x x.2)
    (EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' 𝔖_compact F_eqcont F_cl)
    (range_subset_iff.mpr fun i x _ ↦ F_in_Q x x.2 i)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DivInvMonoid G
inst✝ : TopologicalSpace G
x y : G
⊢ ClusterPt x (map (fun x ↦ y ^ ↑x) atTop) ↔ ClusterPt x (map (fun x ↦ y ^ x) atTop)

Tactic:
zpow_natCast

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
x : G
x✝¹ : x ∈ Set.univ
y : G
x✝ : y ∈ Set.univ
hxy : x ≠ y
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v) x y

Tactic:
obtain ⟨V, dxy⟩ := exists_openSubgroup_separating hxy

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
x : G
x✝¹ : x ∈ Set.univ
y : G
x✝ : y ∈ Set.univ
hxy : x ≠ y
V : OpenSubgroup G
dxy : Disjoint (x • ↑V) (y • ↑V)
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v
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
inst✝ : FiniteDimensional C
E : Subcomplex C
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell (↑E) n)

Tactic:
by
    filter_upwards [FiniteDimensional.eventually_isEmpty_cell (C := C) (D := D)] with n hn
    simp [isEmpty_subtype]

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ (1 - e (π C fun x ↦ x ∈ s) b) x = 1

Tactic:
LocallyConstant.sub_apply,

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ 1 x - (e (π C fun x ↦ x ∈ s) b) x = 1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ (1 - { toFun := fun f ↦ if ↑f a = true then 1 else 0, isLocallyConstant := ⋯ }) y = 0

Tactic:
LocallyConstant.sub_apply,

Goal state after:
case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 1 y - { toFun := fun f ↦ if ↑f a = true then 1 else 0, isLocallyConstant := ⋯ } y = 0
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
x : I → Bool
⊢ x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C

Tactic:
simp only [C0, C1, Set.mem_union, Set.mem_inter_iff, Set.mem_ofPred_eq,
    ← and_or_left, and_iff_left_iff_imp, Bool.dichotomy (x (term I ho)), implies_true]

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

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
x : ↑{fun x ↦ false}
⊢ x = default

Tactic:
by simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]

Goal state after:
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}
hC : IsClosed C
hsC✝ : contained C (Order.succ o)
ho✝ : o < Ordinal.type fun x1 x2 ↦ x1 < x2
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (sum_to C ho) = GoodProducts C

Tactic:
by rw [sum_to_range C ho, union_succ C hsC ho]

Goal state after:
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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
this : ord I (↑↑l).head! ≤ o
⊢ ord I (↑↑l).head! = o

Tactic:
refine eq_of_le_of_not_lt this (not_lt.mpr ?_)

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
this : ord I (↑↑l).head! ≤ o
⊢ o ≤ ord I (↑↑l).head!
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
⊢ (⋂ i, s i).Nonempty

Tactic:
let s' := fun i ↦ if s i ∈ S then s i else s n

Goal state after:
case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
⊢ (⋂ i, s i).Nonempty
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f) (⋃₀ s) (⋃₀ t)

Tactic:
rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, hs⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ ∀ (i : Set X × Set Y),
    (match (x, y) with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
(Ux, Uy)

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
⊢ (match (x, y) with
    | (x, y) =>
      match (Ux, Uy) with
      | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
    ContractibleSpace
      ↑(match (Ux, Uy) with
        | (Ux, Uy) => Ux ×ˢ Uy)
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy
this✝ : ContractibleSpace ↑Ux
this : ContractibleSpace ↑Uy
⊢ ContractibleSpace
    ↑(match (Ux, Uy) with
      | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
exact (Homeomorph.Set.prod Ux Uy).contractibleSpace

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
⊢ (Finset.range #J).biUnion (pairSetSeq J a c) ⊆ J ×ˢ J

Tactic:
rw [Finset.biUnion_subset_iff_forall_subset]

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
⊢ ∀ x ∈ Finset.range #J, pairSetSeq J a c x ⊆ J ×ˢ J