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

Goal state before:
pp: case succ.refine_1
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
⊢ ω0 ^ ↑k * (α' * ↑m) + R < (ω ^ a0.repr) ^ succ ↑(k + 1)

Tactic:
← opow_mul _ _ (succ k.succ)

Goal state after:
case succ.refine_1
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
⊢ ω0 ^ ↑k * (α' * ↑m) + R < ω ^ (a0.repr * succ ↑k.succ)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
next : β
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = some (exp, coef, next)
⊢ corec f b = cons exp coef (corec f next)

Tactic:
simp only [corec, cons]
  rw [Seq.corec_cons]
  simpa

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

Goal state before:
pp: case cons.cons.cons.cons
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
m2 : List ℝ
h2 : (exp1 :: m2).length = (basis_hd :: basis_tl).length
h : List.Lex (fun x1 x2 ↦ x1 < x2) m1 m2
⊢ toFun (exp1 :: m1) (basis_hd :: basis_tl) =o[atTop] toFun (exp1 :: m2) (basis_hd :: basis_tl)

Tactic:
simp only [toFun_cons]
    apply IsBigO.mul_isLittleO (isBigO_refl _ _)
    exact isLittleO_of_lt h_basis.tail (by simpa using h1) (by simpa using h2) h

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

Goal state before:
pp: case hbc
α : 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 : ℕ
hd : α
u v : Stream'.Seq α
ih : dist u v ≤ 2⁻¹ ^ n
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ dist (op c u) (op c v) ≤ dist u v

Tactic:
exact (FriendlyOperationClass.friend _).dist_le

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

Goal state before:
pp: m b : ℕ
hk₁ : m + 1 ≤ b
hk₂ : b ^ 2 ≤ m ^ 2 + 2 * m
⊢ False

Tactic:
← Nat.pow_le_pow_iff_left two_ne_zero

Goal state after:
m b : ℕ
hk₁ : (m + 1) ^ 2 ≤ b ^ 2
hk₂ : b ^ 2 ≤ m ^ 2 + 2 * m
⊢ False
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
⊢ jacobiSymNat a b = 0

Tactic:
refine jacobiSym.eq_zero_iff.mpr
    ⟨ne_of_gt ((Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb₀)).trans_le (Nat.div_le_self b 2)),
      fun hf => ?_⟩
  have h : 2 ∣ a.gcd b := Nat.dvd_gcd (Nat.dvd_of_mod_eq_zero ha) (Nat.dvd_of_mod_eq_zero hb₁)
  change 2 ∣ (a : ℤ).gcd b at h
  rw [hf, ← even_iff_two_dvd] at h
  exact Nat.not_even_one h

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

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

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

Tactic:
· apply not_power_rat_of_num_aux h_coprime ha hq

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
⊢ ↑a / ↑b ≠ q ^ d
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m c : ℕ
⊢ (a.pow b).mod m = c → (a.pow (2 * b + 1)).mod m = (c.mul ((c.mul a).mod m)).mod m

Tactic:
rintro rfl
    change a ^ (2 * b + 1) % m = (a ^ b % m) * ((a ^ b % m * a) % m) % m
    rw [pow_add, two_mul, pow_add, pow_one, Nat.mul_mod (a ^ b % m) a, Nat.mod_mod,
      ← Nat.mul_mod (a ^ b) a, ← Nat.mul_mod, mul_assoc]

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b) = ↑((a ^ b).mod n)

Tactic:
CharP.natCast_eq_natCast_mod α n

Goal state after:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b % n) = ↑((a ^ b).mod n)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ x = y

Tactic:
· rwa [List.applyId_eq_self, List.applyId_eq_self] at h <;> assumption

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst xs ~ map Sigma.snd xs) (hnodup : (map Sigma.snd xs).Nodup),
    Injective (mapToSelf xs hperm hnodup).apply

Tactic:
hxs

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
h : EquicontinuousAt (fun f ↦ ⇑↑f) 1
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
by
  replace h := equicontinuous_of_equicontinuousAt_one _ h
  obtain ⟨W, hWo, hWV, hWc⟩ := local_compact_nhds hV
  let S1 : Set (X →* Y) := {f | Set.MapsTo f U W}
  let S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U W}
  let S3 : Set C(X, Y) := (↑) '' S2
  let S4 : Set (X → Y) := (↑) '' S3
  replace h : Equicontinuous ((↑) : S1 → X → Y) :=
    h.comp (Subtype.map _root_.id fun f hf ↦ hf.mono_right hWV)
  have hS4 : S4 = (↑) '' S1 := by
    ext
    constructor
    · rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩
      exact ⟨f, hf, rfl⟩
    · rintro ⟨f, hf, rfl⟩
      exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩
  replace h : Equicontinuous ((↑) : S3 → X → Y) := by
    rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢
    rwa [← hS4] at h
  replace hS4 : S4 = Set.pi U (fun _ ↦ W) ∩ Set.range ((↑) : (X →* Y) → (X → Y)) := by
    simp_rw [hS4, Set.ext_iff, Set.mem_image, S1, Set.mem_ofPred_eq]
    exact fun f ↦ ⟨fun ⟨g, hg, hf⟩ ↦ hf ▸ ⟨hg, g, rfl⟩, fun ⟨hg, g, hf⟩ ↦ ⟨g, hf ▸ hg, hf⟩⟩
  replace hS4 : IsClosed S4 :=
    hS4.symm ▸ (isClosed_set_pi (fun _ _ ↦ hWc.isClosed)).inter (MonoidHom.isClosed_range_coe X Y)
  have hS2 : (interior S2).Nonempty := by
    let T : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U (interior W)}
    have h1 : T.Nonempty := ⟨1, fun _ _ ↦ mem_interior_iff_mem_nhds.mpr hWo⟩
    have h2 : T ⊆ S2 := fun f hf ↦ hf.mono_right interior_subset
    have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOfPred_mapsTo hU isOpen_interior)
    exact h1.mono (interior_maximal h2 h3)
  exact TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
    ⟨⟨S2, (isInducing_toContinuousMap X Y).isCompact_iff.mpr
      (ArzelaAscoli.isCompact_of_equicontinuous S3 hS4.isCompact h)⟩, hS2⟩

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

Goal state before:
pp: 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 := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : ↑origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((diagram G).map M_to_Na)) ↑origin ∈ fJ a

Tactic:
rw [horigin]

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 := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : ↑origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((diagram G).map M_to_Na)) (spc m) ∈ fJ a
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H✝ : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
⊢ ∃ n, n ≠ 0 ∧ ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s

Tactic:
exact ⟨n₁ ⊔ n₂ ⊔ 1, by simp, fun u h₁ h₂ ↦ H u
      (Ideal.pow_le_pow_right (by simp) h₁)
      (Ideal.pow_le_pow_right (by simp) h₂)⟩

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
⊢ π C J = C

Tactic:
ext x
  refine ⟨fun ⟨y, hy, h⟩ ↦ ?_, fun h ↦ ⟨x, h, ?_⟩⟩
  · rwa [← h, proj_eq_self]; exact (hh · y hy)
  · rw [proj_eq_self]; exact (hh · x h)

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

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
h : eval {fun x ↦ false} nil ∈ Submodule.span ℤ (eval {fun x ↦ false} '' {m | m < nil})
⊢ False

Tactic:
simp [Products.eval, Products.nil] at h

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a b : α
inst✝¹ : Fact (a ≤ b)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
x : α
hx : x ∈ Icc a b
⊢ (IccExtendCM f) x = f ⟨x, hx⟩

Tactic:
simp [IccExtendCM, projIccCM, projIcc, hx.1, hx.2]

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑U),
    (∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ IsGeneratedBy X ↑U

Tactic:
constructor
    rw [continuous_def]
    exact fun _ hV ↦ this _ (fun a ↦
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)).isOpen_preimage _ hV)

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
⊢ IsGeneratedBy X ↑F

Tactic:
let g (a) : W a → F := F.restrictPreimage a.2

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
⊢ IsGeneratedBy X ↑F
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case succ
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
by_cases h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : ¬(logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
n : ℕ
⊢ (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n

Tactic:
induction n with
  | zero => simp [cantorSequence]
  | succ n ih => rw [cantorSequence_get_succ, ih, Finset.sum_range_succ]; ring

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

Goal state before:
pp: case a
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := ⋯
l : ℕ := ⋯
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ (logSizeBallSeq J hJ a c l).radius

Tactic:
exact one_le_radius_logSizeBallSeq hJ ha l

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } ∈ Ω^ N X x

Tactic:
rintro y ⟨i, iH | iH⟩ <;> cases Unique.eq_default i

Goal state after:
case inl.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 0
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

case inr.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 1
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } ∈ Ω^ N X x

Tactic:
by
      rintro y ⟨i, iH | iH⟩ <;> cases Unique.eq_default i <;> apply (congr_arg p iH).trans
      exacts [p.source, p.target]

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

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ ∃ x₀, J = {x₀}

Tactic:
← Finset.card_eq_one

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ #J = 1
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < externalCoveringNumber ε A ↔ A.Nonempty

Tactic:
rw [← not_iff_not]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < coveringNumber ε A ↔ A.Nonempty

Tactic:
rw [← not_iff_not]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < coveringNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < packingNumber ε A ↔ A.Nonempty

Tactic:
rw [← not_iff_not]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < packingNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)

Tactic:
refine Isometry.of_dist_eq fun a b => ?_

Goal state after:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
⊢ ∃ f, Isometry f

Tactic:
rcases (univ : Set α).eq_empty_or_nonempty with h | h
  · use fun _ => 0; intro x; exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)
  · -- We construct a map x : ℕ → α with dense image
    rcases h with ⟨basepoint⟩
    have : Inhabited α := ⟨basepoint⟩
    have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α
    rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩
    rcases Set.countable_iff_exists_subset_range.1 S_countable with ⟨x, x_range⟩
    -- Use embeddingOfSubset to construct the desired isometry
    exact ⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set X
⊢ C ⊆ A → IsCover ε A C → ⨅ C, ⨅ (_ : C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) C), C.encard ≤ C.encard

Tactic:
hC_subset

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set X
hC_subset : C ⊆ A
⊢ IsCover ε A C → ⨅ C, ⨅ (_ : C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) C), C.encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
⊢ C ⊆ f '' A → IsCover ε (f '' A) C → ⨅ C, ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ C.encard

Tactic:
hC_subset

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
hC_subset : C ⊆ f '' A
⊢ IsCover ε (f '' A) C → ⨅ C, ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r f), ↑i < b
x₁ x₂ : X
hx : ¬x₁ = x₂
b : ℝ≥0∞
hb : 0 < b
C : ℝ≥0
hC : HolderWith C r f
hC' : ↑C < b / edist x₁ x₂ ^ ↑r
⊢ edist (f x₁) (f x₂) < b

Tactic:
exact lt_of_le_of_lt (hC x₁ x₂) <| ENNReal.mul_lt_of_lt_div hC'

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ 0 < s.einfsep

Tactic:
by_cases hs : s.Nontrivial

Goal state after:
case pos
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
⊢ 0 < s.einfsep

case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep

Tactic:
not_nontrivial_iff

Goal state after:
case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Subsingleton
⊢ 0 < s.einfsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞

Tactic:
infsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep.toReal = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ∞

Tactic:
infsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.einfsep.toReal ↔ 0 < s.einfsep ∧ s.einfsep < ∞
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : ¬s.Nontrivial
⊢ ¬0 < s.infsep

Tactic:
not_nontrivial_iff

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ ¬0 < s.infsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.infsep ≤ (min (edist x y) (edist y x)).toReal

Tactic:
infsep,

Goal state after:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep.toReal ≤ (min (edist x y) (edist y x)).toReal
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
infsep,

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
⊢ {x, y}.einfsep.toReal = (edist x y).toReal