-- Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
theorem exists_continuousLinearEquiv_apply_eq [ContinuousSMul R V]
    {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ A : V ≃L[R] V, A x = y

Proof state:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ A, A x = y

Tactic:
obtain ⟨G, Gx, Gy⟩ : ∃ G : V →L[R] R, G x = 1 ∧ G y ≠ 0 :=
  exists_eq_one_ne_zero_of_ne_zero_pair hx hy

Result:
case intro.intro
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
⊢ ∃ A, A x = y

Proof state:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (((G y)⁻¹ * G z) • x - ((G y)⁻¹ * G z) • y) + (((G y)⁻¹ * G z) • y - ((G y)⁻¹ * G z) • x) = z

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (G z • y - G z • x) + (G z • x - G z • y) = z

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ { toFun := fun z => z + G z • (y - x), map_add' := ⋯, map_smul' := ⋯ }.toFun
      ((fun z => z + ((G y)⁻¹ * G z) • (x - y)) z) =
    z

Tactic:
simp only [map_add, map_smulₛₗ _, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx,
  smul_eq_mul, mul_sub, mul_one]

Result:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + ((G y)⁻¹ * G z) • (x - y) + (G z + ((G y)⁻¹ * G z - (G y)⁻¹ * G z * G y)) • (y - x) = z

Proof state:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + ((G y)⁻¹ * G z) • (x - y) + (G z + ((G y)⁻¹ * G z - 1 * G z)) • (y - x) = z

Tactic:
simp only [smul_sub, one_mul, add_sub_cancel]

Result:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (((G y)⁻¹ * G z) • x - ((G y)⁻¹ * G z) • y) + (((G y)⁻¹ * G z) • y - ((G y)⁻¹ * G z) • x) = z

Proof state:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + G z • (y - x) + ((G y)⁻¹ * (G z * G y)) • (x - y) = z

Tactic:
rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]

Result:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + G z • (y - x) + (1 * G z) • (x - y) = z

Proof state:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + G z • (y - x) + (1 * G z) • (x - y) = z

Tactic:
simp only [smul_sub, one_mul]

Result:
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + (G z • y - G z • x) + (G z • x - G z • y) = z

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
⊢ ∃ A, A x = y

Tactic:
let A : V ≃L[R] V :=
{ toFun := fun z ↦ z + G z • (y - x)
  invFun := fun z ↦ z + ((G y) ⁻¹ * G z) • (x - y)
  map_add' := fun a b ↦ by simp [add_smul]; abel
  map_smul' := by simp [smul_smul]
  left_inv := fun z ↦ by
    simp only [id_eq, eq_mpr_eq_cast, RingHom.id_apply, smul_eq_mul, AddHom.toFun_eq_coe,
      AddHom.coe_mk, map_add, map_smulₛₗ _, map_sub, Gx, mul_sub, mul_one, add_sub_cancel]
    rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]
    simp only [smul_sub, one_mul]
    abel
  right_inv := fun z ↦ by
      simp only [map_add, map_smulₛₗ _, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx,
      smul_eq_mul, mul_sub, mul_one]
    rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel₀ Gy]
    simp only [smul_sub, one_mul, add_sub_cancel]
    abel
  continuous_toFun := continuous_id.add (G.continuous.smul continuous_const)
  continuous_invFun :=
    continuous_id.add ((continuous_const.mul G.continuous).smul continuous_const) }

Result:
case intro.intro
R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : V →L[R] R
Gx : G x = 1
Gy : G y ≠ 0
A : V ≃L[R] V :=
  { toFun := fun z => z + G z • (y - x), map_add' := ⋯, map_smul' := ⋯,
    invFun := fun z => z + ((G y)⁻¹ * G z) • (x - y), left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ ∃ A, A x = y