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₂
⊢ Eq (α := (a : E) → E₂) (⇑e.toLinearIsometry : (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₂
⊢ Isometry.{u_5, u_6} (α := E) (β := E₂) (⇑e : (a : E) → E₂)

Tactic:
e.toLinearIsometry.isometry

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.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₂
⊢ Injective (α := E ≃ₛₗᵢ[σ₁₂] E₂) toIsometryEquiv

Tactic:
fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toIsometryEquiv = _)

Premises used: LinearIsometryEquiv.coe_injective, congr_arg, Function.Injective, DFunLike.coe
-- 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₂
f g : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ f.toIsometryEquiv = g.toIsometryEquiv ↔ f = g

Tactic:
toIsometryEquiv_injective.eq_iff

Premises used: LinearIsometryEquiv.toIsometryEquiv_injective, Function.Injective.eq_iff
-- 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.toIsometryEquiv : (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₂
rw : Eq.{u_6 + 1} (α := Set E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑e.toIsometryEquiv : (a : E) → E₂)) univ
⊢ Eq.{u_6 + 1} (α := Set E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑e : (a : E) → E₂)) univ

Tactic:
rw [← coe_toIsometryEquiv]

Premises used: LinearIsometryEquiv.coe_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₂
⊢ Eq.{u_6 + 1} (α := Set E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑e.toIsometryEquiv : (a : E) → E₂)) univ

Tactic:
IsometryEquiv.range_eq_univ _

Premises used: IsometryEquiv.range_eq_univ
-- 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} (α := Set E₂) (range.{u_6, u_5 + 1} (ι := E) (⇑e.toIsometryEquiv : (a : E) → E₂)) univ

Tactic:
exact IsometryEquiv.range_eq_univ _

Premises used: IsometryEquiv.range_eq_univ
-- 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₂
⊢ Injective (α := E ≃ₛₗᵢ[σ₁₂] E₂) toHomeomorph

Tactic:
fun x _ h => coe_injective (congr_arg _ h : ⇑x.toHomeomorph = _)

Premises used: LinearIsometryEquiv.coe_injective, congr_arg, Function.Injective, DFunLike.coe
-- 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₂
f g : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ f.toHomeomorph = g.toHomeomorph ↔ f = g

Tactic:
toHomeomorph_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometryEquiv.toHomeomorph_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₂
⊢ Eq (α := (a : E) → E₂) (⇑e.toHomeomorph : (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₂
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑e : (a : E) → E₂)

Tactic:
e.isometry.continuous

Premises used: Isometry.continuous, 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₂
x : E
⊢ ContinuousAt.{u_5, u_6} (Y := E₂) (⇑e : (a : E) → E₂) x

Tactic:
e.continuous.continuousAt

Premises used: Continuous.continuousAt, LinearIsometryEquiv.continuous
-- 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
⊢ ContinuousOn.{u_5, u_6} (Y := E₂) (⇑e : (a : E) → E₂) s

Tactic:
e.continuous.continuousOn

Premises used: Continuous.continuousOn, LinearIsometryEquiv.continuous
-- 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
x : E
⊢ ContinuousWithinAt.{u_5, u_6} (Y := E₂) (⇑e : (a : E) → E₂) s x

Tactic:
e.continuous.continuousWithinAt

Premises used: Continuous.continuousWithinAt, LinearIsometryEquiv.continuous
-- 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₂
⊢ Injective (α := E ≃ₛₗᵢ[σ₁₂] E₂) toContinuousLinearEquiv

Tactic:
fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toContinuousLinearEquiv = _)

Premises used: LinearIsometryEquiv.coe_injective, congr_arg, Function.Injective, DFunLike.coe
-- 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₂
f g : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ (↑f : E ≃SL[σ₁₂] E₂) = (↑g : E ≃SL[σ₁₂] E₂) ↔ f = g

Tactic:
toContinuousLinearEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometryEquiv.toContinuousLinearEquiv_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₂
⊢ Eq (α := (a : E) → E₂) (⇑(↑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
E : Type u_5
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
⊢ Eq (α := (a : E) → E) (⇑(refl R E) : (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
⊢ Eq (α := E ≃L[R] E) (↑(refl R E) : E ≃L[R] E) (ContinuousLinearEquiv.refl R E)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.refl, LinearEquiv.refl, 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₂
x : E₂
⊢ (e : (a : E) → E₂) ((e.symm : (a : E₂) → E) x : E) = x

Tactic:
e.toLinearEquiv.apply_symm_apply x

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.apply_symm_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₂
x : E
⊢ (e.symm : (a : E₂) → E) ((e : (a : E) → E₂) x : E₂) = x

Tactic:
e.toLinearEquiv.symm_apply_apply x

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.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₂
x : E
⊢ Eq.{u_6 + 1} (α := E₂) ((e : (a : E) → E₂) x : E₂) (0 : E₂) ↔ x = 0

Tactic:
e.toLinearEquiv.map_eq_zero_iff

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.map_eq_zero_iff
-- 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.symm = e

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, 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₂
⊢ Bijective (α := E₂ ≃ₛₗᵢ[σ₂₁] E) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, LinearIsometryEquiv.symm_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₂
⊢ e.symm.toLinearEquiv = e.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, 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 (α := (a : E₂) → 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
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 : E₂ ≃SL[σ₂₁] E) = (↑e : E ≃SL[σ₁₂] E₂).symm

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₂
⊢ Eq (α := (a : E₂) → E) (⇑(↑e : E ≃SL[σ₁₂] 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
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.toIsometryEquiv = e.toIsometryEquiv.symm

Tactic:
rfl

Premises used: IsometryEquiv.symm, Equiv.symm, 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 (α := (a : E₂) → E) (⇑e.toIsometryEquiv.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
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.toHomeomorph = e.toHomeomorph.symm

Tactic:
rfl

Premises used: LinearIsometryEquiv.toHomeomorph, Homeomorph.symm, LinearEquiv.toEquiv, Equiv.symm, IsometryEquiv.toHomeomorph, 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 (α := (a : E₂) → E) (⇑e.toHomeomorph.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
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₃) (⇑(e₁.trans e₂) : (a : E) → E₃)
    (comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := 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
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₃
c : E
⊢ Eq.{u_7 + 1} (α := E₃) ((e₁.trans e₂ : (a : E) → E₃) c : E₃) ((e₂ : (a : E₂) → E₃) ((e₁ : (a : E) → E₂) c : 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
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₃) (toLinearEquiv (e.trans e')) (e.trans e'.toLinearEquiv)

Tactic:
rfl

Premises used: 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 (α := E ≃SL[σ₁₃] E₃) (↑(e.trans e') : E ≃SL[σ₁₃] E₃) ((↑e : E ≃SL[σ₁₂] E₂).trans (↑e' : E₂ ≃SL[σ₂₃] E₃))

Tactic:
rfl

Premises used: ContinuousLinearEquiv.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₃
⊢ toIsometryEquiv (e.trans e') = e.toIsometryEquiv.trans e'.toIsometryEquiv

Tactic:
rfl

Premises used: Equiv.trans, LinearIsometryEquiv.toIsometryEquiv, LinearEquiv.toEquiv, IsometryEquiv.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₃
⊢ toHomeomorph (e.trans e') = e.toHomeomorph.trans e'.toHomeomorph

Tactic:
rfl

Premises used: Equiv.trans, LinearEquiv.toEquiv, Homeomorph.trans, IsometryEquiv.toHomeomorph, 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 (refl R₂ E₂) = e

Tactic:
ext fun _ => rfl

Premises used: LinearIsometryEquiv.ext, 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₂
⊢ trans (refl R E) e = e

Tactic:
ext fun _ => rfl

Premises used: LinearIsometryEquiv.ext, rfl