awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ e.trans e.symm = refl R E

Tactic:
ext e.symm_apply_apply

Premises used: LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.ext
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ e.symm.trans e = refl R₂ E₂

Tactic:
ext e.apply_symm_apply

Premises used: LinearIsometryEquiv.apply_symm_apply, LinearIsometryEquiv.ext
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Eq.{u_5 + 1} (α := E → E) (comp.{u_5 + 1, u_6 + 1, u_5 + 1} (β := E₂) (⇑e.symm : (a : E₂) → E) (⇑e : (a : E) → E₂)) id

Tactic:
funext e.symm_apply_apply

Premises used: funext, LinearIsometryEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Eq.{u_6 + 1} (α := E₂ → E₂) (comp.{u_6 + 1, u_5 + 1, u_6 + 1} (β := E) (⇑e : (a : E) → E₂) (⇑e.symm : (a : E₂) → E))
    id

Tactic:
e.symm.symm_comp_self

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.symm_comp_self
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
inst_5 : RingHomInvPair σ₁₃ σ₃₁
inst_6 : RingHomInvPair σ₃₁ σ₁₃
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomInvPair σ₃₂ σ₂₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_11 : SeminormedAddCommGroup E
inst_12 : SeminormedAddCommGroup E₂
inst_13 : SeminormedAddCommGroup E₃
inst_14 : Module R E
inst_15 : Module R₂ E₂
inst_16 : Module R₃ E₃
e₁ : E ≃ₛₗᵢ[σ₁₂] E₂
e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃
⊢ Eq (α := E₃ ≃ₛₗᵢ[σ₃₁] E) (symm (e₁.trans e₂)) (e₂.symm.trans e₁.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearIsometryEquiv.trans, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
inst_5 : RingHomInvPair σ₁₃ σ₃₁
inst_6 : RingHomInvPair σ₃₁ σ₁₃
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomInvPair σ₃₂ σ₂₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_11 : SeminormedAddCommGroup E
inst_12 : SeminormedAddCommGroup E₂
inst_13 : SeminormedAddCommGroup E₃
inst_14 : Module R E
inst_15 : Module R₂ E₂
inst_16 : Module R₃ E₃
e₁ : E ≃ₛₗᵢ[σ₁₂] E₂
e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃
⊢ Eq (α := (a : E₃) → E) (⇑(symm (e₁.trans e₂)) : (a : E₃) → E)
    (comp.{u_7 + 1, u_6 + 1, u_5 + 1} (β := E₂) (⇑e₁.symm : (a : E₂) → E) (⇑e₂.symm : (a : E₃) → E₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_4 : RingHomInvPair σ₁₂ σ₂₁
inst_5 : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
inst_8 : RingHomInvPair σ₂₃ σ₃₂
inst_9 : RingHomInvPair σ₃₂ σ₂₃
inst_10 : RingHomInvPair σ₁₄ σ₄₁
inst_11 : RingHomInvPair σ₄₁ σ₁₄
inst_12 : RingHomInvPair σ₂₄ σ₄₂
inst_13 : RingHomInvPair σ₄₂ σ₂₄
inst_14 : RingHomInvPair σ₃₄ σ₄₃
inst_15 : RingHomInvPair σ₄₃ σ₃₄
inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst_18 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_19 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_20 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_21 : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst_22 : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst_23 : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst_24 : SeminormedAddCommGroup E
inst_25 : SeminormedAddCommGroup E₂
inst_26 : SeminormedAddCommGroup E₃
inst_27 : SeminormedAddCommGroup E₄
inst_28 : Module R E
inst_29 : Module R₂ E₂
inst_30 : Module R₃ E₃
inst_31 : Module R₄ E₄
eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂
eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃
eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄
⊢ Eq (α := E ≃ₛₗᵢ[σ₁₄] E₄) (eEE₂.trans (eE₂E₃.trans eE₃E₄)) (trans (eEE₂.trans eE₂E₃) eE₃E₄)

Tactic:
rfl

Premises used: LinearIsometryEquiv.trans, LinearEquiv.toEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq.{u_5 + 1} (α := (a : E) → E) (⇑1 : (a : E) → E) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e e' : E ≃ₗᵢ[R] E
⊢ Eq (α := (a : E) → E) (⇑(e * e') : (a : E) → E) (comp (β := E) (⇑e : (a : E) → E) (⇑e' : (a : E) → E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e : E ≃ₗᵢ[R] E
⊢ Eq (α := (a : E) → E) (⇑e⁻¹ : (a : E) → E) (⇑e.symm : (a : E) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq (α := E ≃ₗᵢ[R] E) 1 (refl R E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e e' : E ≃ₗᵢ[R] E
⊢ e * e' = e'.trans e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e : E ≃ₗᵢ[R] E
⊢ e⁻¹ = e.symm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq.{u_5 + 1} (α := E ≃L[R] E) (↑1 : E ≃L[R] E) 1

Tactic:
rfl

Premises used: ContinuousLinearEquiv.refl, LinearEquiv.refl, LinearIsometryEquiv.toContinuousLinearEquiv, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e e' : E ≃ₗᵢ[R] E
⊢ (↑(e * e') : E ≃L[R] E) = (↑e : E ≃L[R] E) * (↑e' : E ≃L[R] E)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.trans, LinearIsometryEquiv.toContinuousLinearEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e : E ≃ₗᵢ[R] E
⊢ (↑e⁻¹ : E ≃L[R] E) = (↑e : E ≃L[R] E)⁻¹

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, LinearIsometryEquiv.toContinuousLinearEquiv, rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ e.trans 1 = e

Tactic:
trans_refl _

Premises used: LinearIsometryEquiv.trans_refl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ trans 1 e = e

Tactic:
refl_trans _

Premises used: LinearIsometryEquiv.refl_trans
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e : E ≃ₗᵢ[R] E
⊢ refl R E * e = e

Tactic:
trans_refl _

Premises used: LinearIsometryEquiv.trans_refl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
e : E ≃ₗᵢ[R] E
⊢ e * refl R E = e

Tactic:
refl_trans _

Premises used: LinearIsometryEquiv.refl_trans
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ e.toLinearIsometry.toContinuousLinearMap = (↑(↑e : E ≃SL[σ₁₂] E₂) : E →SL[σ₁₂] E₂)

Tactic:
rfl

Premises used: rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Eq (α := (a : E) → E₂) (⇑(↑(↑e : E ≃SL[σ₁₂] E₂) : E →SL[σ₁₂] E₂) : (a : E) → E₂) (⇑e : (a : E) → E₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Eq.{u_6 + 1} (α := E₂) ((e : (a : E) → E₂) 0 : E₂) (0 : E₂)

Tactic:
e.1.map_zero

Premises used: LinearEquiv.map_zero, LinearIsometryEquiv.toLinearEquiv
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ (e : (a : E) → E₂) (x + y) = HAdd.hAdd (α := E₂) (β := E₂) ((e : (a : E) → E₂) x : E₂) ((e : (a : E) → E₂) y : E₂)

Tactic:
e.1.map_add x y

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.map_add
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ (e : (a : E) → E₂) (x - y) = HSub.hSub (α := E₂) (β := E₂) ((e : (a : E) → E₂) x : E₂) ((e : (a : E) → E₂) y : E₂)

Tactic:
e.1.map_sub x y

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.toLinearMap, LinearMap.map_sub
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
c : R
x : E
⊢ (e : (a : E) → E₂) (c • x) =
    HSMul.hSMul.{u_2, u_6, u_6} (α := R₂) (β := E₂) ((σ₁₂ : (a : R) → R₂) c : R₂) ((e : (a : E) → E₂) x : E₂)

Tactic:
e.1.map_smulₛₗ c x

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.map_smulₛₗ
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup E₂
inst_3 : Module R E
inst_4 : Module R E₂
e : E ≃ₗᵢ[R] E₂
c : R
x : E
⊢ (e : (a : E) → E₂) (c • x) = HSMul.hSMul (β := E₂) c ((e : (a : E) → E₂) x : E₂)

Tactic:
e.1.map_smul c x

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.map_smul
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ dist.{u_6} (α := E₂) ((e : (a : E) → E₂) x : E₂) ((e : (a : E) → E₂) y : E₂) = dist x y

Tactic:
e.toLinearIsometry.dist_map x y

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.dist_map
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ edist.{u_6} (α := E₂) ((e : (a : E) → E₂) x : E₂) ((e : (a : E) → E₂) y : E₂) = edist x y

Tactic:
e.toLinearIsometry.edist_map x y

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.edist_map
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Bijective.{u_5 + 1, u_6 + 1} (α := E) (β := E₂) (⇑e : (a : E) → E₂)

Tactic:
e.1.bijective

Premises used: LinearEquiv.bijective, LinearIsometryEquiv.toLinearEquiv
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Injective.{u_5 + 1, u_6 + 1} (α := E) (β := E₂) (⇑e : (a : E) → E₂)

Tactic:
e.1.injective

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.injective
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := E₂) (⇑e : (a : E) → E₂)

Tactic:
e.1.surjective

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.surjective
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x y : E
⊢ Eq.{u_6 + 1} (α := E₂) ((e : (a : E) → E₂) x : E₂) ((e : (a : E) → E₂) y : E₂) ↔ x = y

Tactic:
e.injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometryEquiv.injective
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x y : E
h : x ≠ y
⊢ Ne.{u_6 + 1} (α := E₂) ((e : (a : E) → E₂) x : E₂) ((e : (a : E) → E₂) y : E₂)

Tactic:
e.injective.ne h

Premises used: Function.Injective.ne, LinearIsometryEquiv.injective
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ LipschitzWith.{u_5, u_6} (α := E) (β := E₂) 1 (⇑e : (a : E) → E₂)

Tactic:
e.isometry.lipschitz

Premises used: LinearIsometryEquiv.isometry, Isometry.lipschitz
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ AntilipschitzWith.{u_5, u_6} (α := E) (β := E₂) 1 (⇑e : (a : E) → E₂)

Tactic:
e.isometry.antilipschitz

Premises used: LinearIsometryEquiv.isometry, Isometry.antilipschitz
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
s : Set E
⊢ Eq.{u_6 + 1} (α := Set E₂) ((⇑e : (a : E) → E₂) '' s) ((⇑e.symm : (a : E₂) → E) ⁻¹' s)

Tactic:
e.toLinearEquiv.image_eq_preimage_symm s

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.image_eq_preimage_symm
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
s : Set E
⊢ Metric.ediam.{u_6} (X := E₂) ((⇑e : (a : E) → E₂) '' s) = Metric.ediam s

Tactic:
e.isometry.ediam_image s

Premises used: Isometry.ediam_image, LinearIsometryEquiv.isometry
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
s : Set E
⊢ Metric.diam.{u_6} (α := E₂) ((⇑e : (a : E) → E₂) '' s) = Metric.diam s

Tactic:
e.isometry.diam_image s

Premises used: LinearIsometryEquiv.isometry, Isometry.diam_image
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E₂
r : ℝ
⊢ Eq.{u_5 + 1} (α := Set E) ((⇑e : (a : E) → E₂) ⁻¹' Metric.ball x r : Set E)
    (Metric.ball ((e.symm : (a : E₂) → E) x) r : Set E)

Tactic:
e.toIsometryEquiv.preimage_ball x r

Premises used: LinearIsometryEquiv.toIsometryEquiv, IsometryEquiv.preimage_ball
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E₂
r : ℝ
⊢ Eq.{u_5 + 1} (α := Set E) ((⇑e : (a : E) → E₂) ⁻¹' Metric.sphere x r : Set E)
    (Metric.sphere ((e.symm : (a : E₂) → E) x) r : Set E)

Tactic:
e.toIsometryEquiv.preimage_sphere x r

Premises used: IsometryEquiv.preimage_sphere, LinearIsometryEquiv.toIsometryEquiv
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E₂
r : ℝ
⊢ Eq.{u_5 + 1} (α := Set E) ((⇑e : (a : E) → E₂) ⁻¹' Metric.closedBall x r : Set E)
    (Metric.closedBall ((e.symm : (a : E₂) → E) x) r : Set E)

Tactic:
e.toIsometryEquiv.preimage_closedBall x r

Premises used: LinearIsometryEquiv.toIsometryEquiv, IsometryEquiv.preimage_closedBall
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
r : ℝ
⊢ Eq.{u_6 + 1} (α := Set E₂) ((⇑e : (a : E) → E₂) '' Metric.ball x r : Set E₂)
    (Metric.ball ((e : (a : E) → E₂) x) r : Set E₂)

Tactic:
e.toIsometryEquiv.image_ball x r

Premises used: LinearIsometryEquiv.toIsometryEquiv, IsometryEquiv.image_ball
-- Module: Mathlib.Analysis.Normed.Operator.LinearIsometry
Goal:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
inst_4 : SeminormedAddCommGroup E
inst_5 : SeminormedAddCommGroup E₂
inst_6 : Module R E
inst_7 : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
r : ℝ
⊢ Eq.{u_6 + 1} (α := Set E₂) ((⇑e : (a : E) → E₂) '' Metric.sphere x r : Set E₂)
    (Metric.sphere ((e : (a : E) → E₂) x) r : Set E₂)

Tactic:
e.toIsometryEquiv.image_sphere x r

Premises used: IsometryEquiv.image_sphere, LinearIsometryEquiv.toIsometryEquiv