awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
this_1 : CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)
this : CompleteSpace.{u_2} (↑(↑q : Set E) : Type u_2)
⊢ Continuous (X := ↥p × ↥q) (Y := E) (⇑(prodEquivOfIsCompl p q h) : (a : ↥p × ↥q) → E)

Tactic:
exact (p.subtypeL.coprod q.subtypeL).continuous

Premises used: Submodule.subtypeL, ContinuousLinearMap.continuous, ContinuousLinearMap.coprod
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
⊢ Eq (α := (a : ↥p × ↥q) → E) (⇑(prodEquivOfClosedCompl p q h hp hq) : (a : ↥p × ↥q) → E)
    (⇑(prodEquivOfIsCompl p q h) : (a : ↥p × ↥q) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
⊢ Eq (α := (a : E) → ↥p × ↥q) (⇑(prodEquivOfClosedCompl p q h hp hq).symm : (a : E) → ↥p × ↥q)
    (⇑(prodEquivOfIsCompl p q h).symm : (a : E) → ↥p × ↥q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
⊢ (↑(linearProjOfClosedCompl p q h hp hq) : E →ₗ[𝕜] ↥p) = projectionOnto p q h

Tactic:
rfl

Premises used: Set.Mem, Submodule.projectionOnto, rfl
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
⊢ Eq (α := (a : E) → ↥p) (⇑(linearProjOfClosedCompl p q h hp hq) : (a : E) → ↥p)
    (⇑(projectionOnto p q h) : (a : E) → ↥p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
⊢ ClosedComplemented p

Tactic:
⟨p.linearProjOfClosedCompl q h hp hq, Submodule.projectionOnto_apply_left h⟩

Premises used: Submodule.linearProjOfClosedCompl, Submodule.ClosedComplemented, Submodule.projectionOnto_apply_left, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
p : Subspace 𝕜 E
⊢ ClosedComplemented p ↔ IsClosed (↑p : Set E) ∧ ∃ (q : Submodule 𝕜 E), IsClosed (↑q : Set E) ∧ IsCompl p q

Tactic:
⟨fun h => ⟨h.isClosed, h.exists_isClosed_isCompl⟩,
    fun ⟨hp, ⟨_, hq, hpq⟩⟩ => .of_isCompl_isClosed hpq hp hq⟩

Premises used: Submodule.ClosedComplemented.exists_isClosed_isCompl, _private.0.Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl.match_1, Submodule.ClosedComplemented, Submodule.ClosedComplemented.isClosed, And.intro, Iff.intro, Submodule.ClosedComplemented.of_isCompl_isClosed
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformContinuousConstSMul 𝕜 E
⊢ Eq.{u_2 + 1} (α := (a : E) → Completion E) (⇑toComplₗᵢ : (a : E) → Completion E) coe'

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformContinuousConstSMul 𝕜 E
⊢ Eq.{u_2 + 1} (α := (a : E) → Completion E) (⇑toComplL : (a : E) → Completion E) coe'

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
⊢ norm.{u_4} (E := E →L[𝕜] Completion E) toComplL = 1

Tactic:
(toComplₗᵢ : E →ₗᵢ[𝕜] Completion E).norm_toContinuousLinearMap

Premises used: UniformSpace.Completion.toComplL, LinearIsometry.norm_toContinuousLinearMap, UniformSpace.Completion.toComplₗᵢ
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
hp : Continuous (Y := ℝ) fun (b : Completion A × Completion A) ↦ ‖b.1 * b.2‖
hp₁ : Continuous (Y := ℝ) fun (b : Completion A × Completion A) ↦ ‖b.1‖ * ‖b.2‖
⊢ IsClosed.{u_3} (X := Completion A × Completion A) {x : Completion A × Completion A | ‖x.1 * x.2‖ ≤ ‖x.1‖ * ‖x.2‖}

Tactic:
apply isClosed_le

Premises used: isClosed_le
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
⊢ Continuous (Y := ℝ) fun (b : Completion A × Completion A) ↦ ‖b.1 * b.2‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
⊢ Continuous (Y := ℝ) fun (b : Completion A × Completion A) ↦ ‖b.1‖ * ‖b.2‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
x y : A
⊢ ‖HMul.hMul (α := Completion A) (↑x : Completion A) (↑y : Completion A)‖ ≤
    norm (E := Completion A) (↑x : Completion A) * norm (E := Completion A) (↑y : Completion A)

Tactic:
simpa only [← coe_mul, norm_coe] using norm_mul_le x y

Premises used: UniformSpace.Completion.norm_coe, UniformSpace.Completion.coe_mul, norm_mul_le
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : SeminormedRing A
x y : Completion A
hp : IsClosed.{u_3} (X := Completion A × Completion A) {x : Completion A × Completion A | ‖x.1 * x.2‖ ≤ ‖x.1‖ * ‖x.2‖}
ih :
  ∀ (x y : A),
    ‖HMul.hMul (α := Completion A) (↑x : Completion A) (↑y : Completion A)‖ ≤
      norm (E := Completion A) (↑x : Completion A) * norm (E := Completion A) (↑y : Completion A)
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖

Tactic:
induction x, y using induction_on₂ with
    | hp => apply isClosed_le <;> fun_prop
    | ih x y => simpa only [← coe_mul, norm_coe] using norm_mul_le x y

Premises used: isClosed_le, UniformSpace.Completion.norm_coe, UniformSpace.Completion.coe_mul, norm_mul_le
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : NormedField A
inst_1 : CompletableTopField A
x y : Completion A
⊢ Continuous (Y := ℝ) fun (x : Completion A × Completion A) ↦ ‖x.1 * x.2‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : NormedField A
inst_1 : CompletableTopField A
x y : Completion A
⊢ Continuous (Y := ℝ) fun (x : Completion A × Completion A) ↦ ‖x.1‖ * ‖x.2‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Module.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst : NormedField A
inst_1 : CompletableTopField A
x y : Completion A
⊢ ∀ (a b : A),
    ‖HMul.hMul (α := Completion A) (↑a : Completion A) (↑b : Completion A)‖ =
      norm (E := Completion A) (↑a : Completion A) * norm (E := Completion A) (↑b : Completion A)

Tactic:
simp [← coe_mul]

Premises used: UniformSpace.Completion.coe_mul
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
⊢ Nontrivial E

Tactic:
have : Nontrivial E := (rank_pos_iff_nontrivial (R := ℝ)).1 (zero_lt_one.trans h)
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
⊢ sᶜ.Nonempty

Tactic:
(hs.dense_compl ℝ).nonempty

Premises used: Real, Dense.nonempty, Set.Countable.dense_compl
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
obtain : ∀ (a : E) (ha : a ∈ sᶜ), IsPathConnected sᶜ
⊢ IsPathConnected sᶜ

Tactic:
obtain ⟨a, ha⟩ : sᶜ.Nonempty := (hs.dense_compl ℝ).nonempty

Premises used: Real, Compl.compl, Dense.nonempty, Set.Countable.dense_compl, Set.Nonempty
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
⊢ IsPathConnected sᶜ

Tactic:
⟨a, ha, ?_⟩

Premises used: IsPathConnected, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
refine : ∀ ⦃y : E⦄, y ∈ sᶜ → JoinedIn sᶜ a y
⊢ IsPathConnected sᶜ

Tactic:
refine ⟨a, ha, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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ᶜ
inl : ∀ (hb : a ∈ sᶜ), JoinedIn sᶜ a a
inr : ∀ (hab : a ≠ b), JoinedIn sᶜ a b
⊢ JoinedIn sᶜ a b

Tactic:
rcases eq_or_ne a b with rfl | hab

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha hb : a ∈ sᶜ
⊢ JoinedIn sᶜ a a

Tactic:
JoinedIn.refl ha

Premises used: JoinedIn.refl
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha hb : a ∈ sᶜ
⊢ JoinedIn sᶜ a a

Tactic:
exact JoinedIn.refl ha

Premises used: JoinedIn.refl
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
simp : HSMul.hSMul (α := ℝ) 2⁻¹ (a + b) - HSMul.hSMul (α := ℝ) 2⁻¹ (b - a) = a
⊢ c - x = a

Tactic:
simp only [c, x]
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (a + b) - HSMul.hSMul (α := ℝ) 2⁻¹ (b - a) = a

Tactic:
module
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
⊢ c - x = a

Tactic:
have Ia : c - x = a := by
    simp only [c, x]
    module
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
simp : HSMul.hSMul (α := ℝ) 2⁻¹ (a + b) + HSMul.hSMul (α := ℝ) 2⁻¹ (b - a) = b
⊢ c + x = b

Tactic:
simp only [c, x]
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (a + b) + HSMul.hSMul (α := ℝ) 2⁻¹ (b - a) = b

Tactic:
module
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
⊢ c + x = b

Tactic:
have Ib : c + x = b := by
    simp only [c, x]
    module
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
⊢ x ≠ 0

Tactic:
simpa [x] using sub_ne_zero.2 hab.symm

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
⊢ x ≠ 0

Tactic:
have x_ne_zero : x ≠ 0 := by simpa [x] using sub_ne_zero.2 hab.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
⊢ ∃ (y : E), LinearIndependent ℝ ![x, y]

Tactic:
exists_linearIndependent_pair_of_one_lt_rank h x_ne_zero

Premises used: exists_linearIndependent_pair_of_one_lt_rank
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
apply :
  Pairwise (α := ℝ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s)
⊢ Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}

Tactic:
apply countable_setOf_nonempty_of_disjoint _ (fun t ↦ inter_subset_right) hs

Premises used: Set.countable_setOf_nonempty_of_disjoint, Set.inter_subset_right
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 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'
apply :
  Eq.{u_1 + 1} (α := Set E)
    ((fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t') ∅
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint (fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t t'

Tactic:
apply disjoint_iff_inter_eq_empty.2

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 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 only [singleton_inter_eq_empty, mem_compl_iff, Ib] using hb

Premises used: Set.singleton_inter_eq_empty, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 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:
have N : {c + x} ∩ s = ∅ := by
      simpa only [singleton_inter_eq_empty, mem_compl_iff, Ib] using hb
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 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'
N : {c + x} ∩ s = ∅
rw : [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ∩ s ⊆ {c + x} ∩ s
⊢ Eq.{u_1 + 1} (α := Set E)
    ((fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t ∩ (fun (t : ℝ) ↦ [c + x -[ℝ] c + t • y] ∩ s) t') ∅

Tactic:
rw [inter_assoc, inter_comm s, inter_assoc, inter_self, ← inter_assoc, ← subset_empty_iff, ← N]

Premises used: Set.inter_self, Set.inter_comm, Set.subset_empty_iff, Set.inter_assoc
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 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'
N : {c + x} ∩ s = ∅
H : [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ⊆ {c + x}
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ∩ s ⊆ {c + x} ∩ s

Tactic:
apply inter_subset_inter_left

Premises used: Set.inter_subset_inter_left
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 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'
N : {c + x} ∩ s = ∅
H : [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] = {c + x}
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ⊆ {c + x}

Tactic:
apply Eq.subset

Premises used: Eq.subset
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 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'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] = {c + x}

Tactic:
apply segment_inter_eq_endpoint_of_linearIndependent_of_ne hy htt'.symm

Premises used: segment_inter_eq_endpoint_of_linearIndependent_of_ne, Ne.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
⊢ Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}

Tactic:
have A : Set.Countable {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty} := by
    apply countable_setOf_nonempty_of_disjoint _ (fun t ↦ inter_subset_right) hs
    intro t t' htt'
    apply disjoint_iff_inter_eq_empty.2
    have N : {c + x} ∩ s = ∅ := by
      simpa only [singleton_inter_eq_empty, mem_compl_iff, Ib] using hb
    rw [inter_assoc, inter_comm s, inter_assoc, inter_self, ← inter_assoc, ← subset_empty_iff, ← N]
    apply inter_subset_inter_left
    apply Eq.subset
    apply segment_inter_eq_endpoint_of_linearIndependent_of_ne hy htt'.symm
-- Module: Mathlib.Analysis.Normed.Module.Connected
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : 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 := HSMul.hSMul (α := ℝ) 2⁻¹ (a + b)
x : E := HSMul.hSMul (α := ℝ) 2⁻¹ (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : Set.Countable (α := ℝ) {t : ℝ | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}
apply :
  Pairwise (α := ℝ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (t : ℝ) ↦ [c - x -[ℝ] c + t • y] ∩ s)
⊢ Set.Countable (α := ℝ) {t : ℝ | ([c - x -[ℝ] c + t • y] ∩ s).Nonempty}

Tactic:
apply countable_setOf_nonempty_of_disjoint _ (fun t ↦ inter_subset_right) hs

Premises used: Set.countable_setOf_nonempty_of_disjoint, Set.inter_subset_right