mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : (ℕ → Bool) → 𝕜
f_inj : Injective f
⊢ 𝔠 ≤ #𝕜

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : (ℕ → Bool) → 𝕜
f_inj : Injective f
⊢ 𝔠 ≤ #𝕜
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ x + c ^ n ∈ U ∩ Set.univ

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ x + c ^ n ∈ U
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ c ≠ 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
x✝ : x ∈ Set.univ
U : Set 𝕜
hU : U ∈ 𝓝 x
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < 1
A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 x)
B : ∀ᶠ (n : ℕ) in atTop, x + c ^ n ∈ U
n : ℕ
hn : x + c ^ n ∈ U
⊢ ¬c = 0
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
⊢ lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜

Tactic:
simpa using

Goal state after:
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
⊢ 𝔠 ≤ #𝕜
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: 𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
A : lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜
⊢ 𝔠 ≤ #E

Tactic:
simpa using

Goal state after:
𝕜 : Type u
E : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial E
A : lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜
⊢ 𝔠 ≤ #E
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x < 1 ↔ w x < 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x < 1 ↔ w x < 1
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ 1 < v x ↔ 1 < w x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ 1 < v x ↔ 1 < w x
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x ≤ 1 ↔ w x ≤ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x ≤ 1 ↔ w x ≤ 1
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ 1 ≤ v x ↔ 1 ≤ w x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ 1 ≤ v x ↔ 1 ≤ w x
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x = 1 ↔ w x = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : PartialOrder S
v w : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : Nontrivial R
h : v.IsEquiv w
x : R
⊢ v x = 1 ↔ w x = 1
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ⇑g ⁻¹' s
⊢ s ∈ 𝓝 (g 0)

Tactic:
simpa using

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
g : E ≃ₜ E := Homeomorph.addLeft x
t : Set E := ⇑g ⁻¹' s
⊢ s ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝²] s
h's : s.Nonempty
⊢ 𝔠 ≤ #↑s

Tactic:
simpa using

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝²] s
h's : s.Nonempty
⊢ 𝔠 ≤ #E
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
⊢ Tendsto (fun n ↦ (v i) (c n)) atTop atTop

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
⊢ Tendsto (fun n ↦ (v i) a ^ n * (v i) b) atTop atTop
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
j : ι
hj : j ≠ i
⊢ Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
j : ι
hj : j ≠ i
⊢ Tendsto (fun n ↦ (v j) a ^ n * (v j) b) atTop (𝓝 0)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
j : ι
hj : j ≠ i
⊢ Set.Iio 1 ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
j : ι
hj : j ≠ i
⊢ ∃ a, Set.Iio 1 = Set.Ioi a ∨ Set.Iio 1 = Set.Iio a
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
⊢ HasFPowerSeriesOnBall g p x p.radius

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
⊢ HasFPowerSeriesOnBall g p x p.radius
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
⊢ x ≠ 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
⊢ ¬b - a = 0
Module: Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall g p x p.radius
⊢ AnalyticOnNhd 𝕜 g (Metric.eball x p.radius)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
f : 𝕜 → 𝕜
x : 𝕜
r : ENNReal
hr_pos : 0 < r
h : AnalyticOnNhd 𝕜 f (Metric.eball x r)
p : FormalMultilinearSeries 𝕜 𝕜 𝕜 := FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial
hr : r ≤ p.radius
g : 𝕜 → 𝕜 := fun t ↦ p.sum (t - x)
hg : HasFPowerSeriesOnBall g p x p.radius
⊢ AnalyticOnNhd 𝕜 g (Metric.eball x p.radius)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
rₙ : (j : ι) → j ≠ i → ℕ
hrₙ : ∀ (j : ι) (hj : j ≠ i) (b : ℕ), rₙ j hj ≤ b → (v j) (c b) ∈ Set.Iio 1
this : Fintype ι
r : ℕ := Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h
j : ι
hj : j ≠ i
⊢ (v j) (c r) < 1

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : w a = 1
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ a ^ n * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (a : ℕ), r₁ ≤ a → 2 ≤ (v i) (c a)
rₙ : (j : ι) → j ≠ i → ℕ
hrₙ : ∀ (j : ι) (hj : j ≠ i) (b : ℕ), rₙ j hj ≤ b → (v j) (c b) ∈ Set.Iio 1
this : Fintype ι
r : ℕ := Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h
j : ι
hj : j ≠ i
⊢ (v j) (c r) < 1
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
⊢ {c + x} ∩ s = ∅

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
⊢ b ∉ s
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
this : (v i) a⁻¹ < 1
⊢ Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
this : (v i) a⁻¹ < 1
⊢ Tendsto (fun n ↦ ((v i) (1 + (a ^ n)⁻¹))⁻¹ * (v i) b) atTop (𝓝 ((v i) b))
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
j : ι
hj : j ≠ i
this : 1 < (v j) a⁻¹
⊢ Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
j : ι
hj : j ≠ i
this : 1 < (v j) a⁻¹
⊢ Tendsto (fun n ↦ ((v j) (1 + (a ^ n)⁻¹))⁻¹ * (v j) b) atTop (𝓝 0)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcⱼ : ∀ (j : ι), j ≠ i → Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)
this : w a⁻¹ < 1
⊢ Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcⱼ : ∀ (j : ι), j ≠ i → Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)
this : w a⁻¹ < 1
⊢ Tendsto (fun n ↦ (w (1 + (a ^ n)⁻¹))⁻¹ * w b) atTop (𝓝 (w b))
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
⊢ {c - x} ∩ s = ∅

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
⊢ a ∉ s
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcₙ : Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (b : ℕ), r₁ ≤ b → 1 < (v i) (c b)
j : ι
hj : j ≠ i
⊢ Set.Iio 1 ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcₙ : Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (b : ℕ), r₁ ≤ b → 1 < (v i) (c b)
j : ι
hj : j ≠ i
⊢ ∃ a, Set.Iio 1 = Set.Ioi a ∨ Set.Iio 1 = Set.Iio a
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
hr : 0 ≤ 0
⊢ IsPathConnected (sphere x 0)

Tactic:
simpa using

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
hr : 0 ≤ 0
⊢ IsPathConnected {x}
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
y : E
hy : y ∈ {0}ᶜ
⊢ ‖id y‖ ≠ 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
y : E
hy : y ∈ {0}ᶜ
⊢ ¬y = 0
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
⊢ f '' {0}ᶜ = sphere x r

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := ⋯
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
⊢ f '' {0}ᶜ ⊆ sphere x r

case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := ⋯
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
⊢ sphere x r ⊆ f '' {0}ᶜ