Theorem: InDown_eq_DownIn (src/MainTheorem.lean)

State before:
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
⊢ ⇑(AffineIsometryEquiv.VSubconst ℝ x) '' (Subtype.val ⁻¹' S) = Subtype.val ⁻¹' (S -ᵥ {↑x})
Tactic:
ext y
State after:
case h
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ y ∈ ⇑(AffineIsometryEquiv.VSubconst ℝ x) '' (Subtype.val ⁻¹' S) ↔ y ∈ Subtype.val ⁻¹' (S -ᵥ {↑x})

State before:
case h
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ y ∈ ⇑(AffineIsometryEquiv.VSubconst ℝ x) '' (Subtype.val ⁻¹' S) ↔ y ∈ Subtype.val ⁻¹' (S -ᵥ {↑x})
Tactic:
simp only [AffineIsometryEquiv.coe_VSubconst, Set.vsub_singleton, Set.mem_image, Set.mem_preimage,
  Set.mem_image, Subtype.exists, exists_and_left]
State after:
case h
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) ↔ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y

State before:
case h
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) ↔ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y
Tactic:
constructor
State after:
case h.mp
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) → ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y

case h.mpr
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y) → ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y

State before:
case h.mp
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y) → ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y
Tactic:
rintro ⟨ v, hvmemS, ⟨ hvmemp, rfl ⟩ ⟩
State after:
case h.mp.intro.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)

State before:
case h.mp.intro.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ ∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)
Tactic:
refine ⟨ v, hvmemS, ?_ ⟩
State after:
case h.mp.intro.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ v -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)

State before:
case h.mp.intro.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
v : P
hvmemS : v ∈ S
hvmemp : v ∈ p
⊢ v -ᵥ ↑x = ↑({ val := v, property := ⋯ } -ᵥ x)
Tactic:
simp only [hvmemS, AffineSubspace.coe_vsub]
State after:
no goals

State before:
case h.mpr
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
⊢ (∃ x_1 ∈ S, x_1 -ᵥ ↑x = ↑y) → ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
rintro ⟨ v, hvmemS, h ⟩
State after:
case h.mpr.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y

State before:
case h.mpr.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
have := y.2
State after:
case h.mpr.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : ↑y ∈ AffineSubspace.direction p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y

State before:
case h.mpr.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : ↑y ∈ AffineSubspace.direction p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
rw [← h, AffineSubspace.vsub_right_mem_direction_iff_mem x.2] at this
State after:
case h.mpr.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : v ∈ p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y

State before:
case h.mpr.intro.intro
E✝ : Type
inst✝⁹ : NormedAddCommGroup E✝
inst✝⁸ : InnerProductSpace ℝ E✝
inst✝⁷ : CompleteSpace E✝
E P : Type
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor E P
inst✝¹ : FiniteDimensional ℝ E
p : AffineSubspace ℝ P
inst✝ : Nonempty ↥p
S : Set P
x : ↥p
y : ↥(AffineSubspace.direction p)
v : P
hvmemS : v ∈ S
h : v -ᵥ ↑x = ↑y
this : v ∈ p
⊢ ∃ a ∈ S, ∃ (x_1 : a ∈ p), { val := a, property := ⋯ } -ᵥ x = y
Tactic:
exact ⟨ v, hvmemS, this, Subtype.val_injective ((AffineSubspace.coe_vsub _ _ x) ▸ h) ⟩
State after:
no goals