awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
inst_17 : Module R₁ M₁
inst_18 : Module R₂ M₂
inst_19 : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
c : M₁
⊢ Eq.{u_6 + 1} (α := M₃) ((e₁.trans e₂ : (a : M₁) → M₃) c : M₃)
    ((e₂ : (a : M₂) → M₃) ((e₁ : (a : M₁) → M₂) c : M₂) : M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
c : M₂
⊢ (e : (a : M₁) → M₂) ((e.symm : (a : M₂) → M₁) c : M₁) = c

Tactic:
e.1.right_inv c

Premises used: LinearEquiv.right_inv, ContinuousLinearEquiv.toLinearEquiv
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
b : M₁
⊢ (e.symm : (a : M₂) → M₁) ((e : (a : M₁) → M₂) b : M₂) = b

Tactic:
e.1.left_inv b

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.left_inv
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ e.symm.trans e = ContinuousLinearEquiv.refl R₂ M₂

Tactic:
ext <| funext fun _ ↦ apply_symm_apply _ _

Premises used: ContinuousLinearEquiv.ext, ContinuousLinearEquiv.apply_symm_apply, funext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ e.trans e.symm = ContinuousLinearEquiv.refl R₁ M₁

Tactic:
ext <| funext fun _ ↦ symm_apply_apply _ _

Premises used: ContinuousLinearEquiv.ext, funext, ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
inst_17 : Module R₁ M₁
inst_18 : Module R₂ M₂
inst_19 : Module R₃ M₃
e₁ : M₂ ≃SL[σ₂₁] M₁
e₂ : M₃ ≃SL[σ₃₂] M₂
c : M₁
⊢ Eq.{u_6 + 1} (α := M₃) ((ContinuousLinearEquiv.symm (e₂.trans e₁) : (a : M₁) → M₃) c : M₃)
    ((e₂.symm : (a : M₂) → M₃) ((e₁.symm : (a : M₁) → M₂) c : M₂) : M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₁
⊢ Set.image.{u_5, u_4} (α := M₂) (⇑e.symm : (a : M₂) → M₁) ((⇑e : (a : M₁) → M₂) '' s) = s

Tactic:
e.toLinearEquiv.toEquiv.symm_image_image s

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toEquiv, Equiv.symm_image_image
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ Set.image.{u_4, u_5} (α := M₁) (⇑e : (a : M₁) → M₂) ((⇑e.symm : (a : M₂) → M₁) '' s) = s

Tactic:
e.symm.symm_image_image s

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.symm_image_image
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
inst_17 : Module R₁ M₁
inst_18 : Module R₂ M₂
inst_19 : Module R₃ M₃
f : M₁ ≃SL[σ₁₂] M₂
f' : M₂ ≃SL[σ₂₃] M₃
⊢ (↑f' : M₂ →SL[σ₂₃] M₃) ∘SL (↑f : M₁ →SL[σ₁₂] M₂) = (↑(f.trans f') : M₁ →SL[σ₁₃] M₃)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ (↑e : M₁ →SL[σ₁₂] M₂) ∘SL (↑e.symm : M₂ →SL[σ₂₁] M₁) = ContinuousLinearMap.id R₂ M₂

Tactic:
ContinuousLinearMap.ext e.apply_symm_apply

Premises used: ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ (↑e.symm : M₂ →SL[σ₂₁] M₁) ∘SL (↑e : M₁ →SL[σ₁₂] M₂) = ContinuousLinearMap.id R₁ M₁

Tactic:
ContinuousLinearMap.ext e.symm_apply_apply

Premises used: ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
h :
  ∀ (x : M₁),
    Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := M₂) (⇑e.symm : (a : M₂) → M₁) (⇑e : (a : M₁) → M₂) x = id x
⊢ Eq.{u_4 + 1} (α := M₁ → M₁)
    (Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := M₂) (⇑e.symm : (a : M₂) → M₁) (⇑e : (a : M₁) → M₂)) id

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₁
⊢ Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := M₂) (⇑e.symm : (a : M₂) → M₁) (⇑e : (a : M₁) → M₂) x = id x

Tactic:
symm_apply_apply e x

Premises used: ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₁
⊢ Function.comp.{u_4 + 1, u_5 + 1, u_4 + 1} (β := M₂) (⇑e.symm : (a : M₂) → M₁) (⇑e : (a : M₁) → M₂) x = id x

Tactic:
exact symm_apply_apply e x

Premises used: ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
h :
  ∀ (x : M₂),
    Function.comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := M₁) (⇑e : (a : M₁) → M₂) (⇑e.symm : (a : M₂) → M₁) x = id x
⊢ Eq.{u_5 + 1} (α := M₂ → M₂)
    (Function.comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := M₁) (⇑e : (a : M₁) → M₂) (⇑e.symm : (a : M₂) → M₁)) id

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
⊢ Function.comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := M₁) (⇑e : (a : M₁) → M₂) (⇑e.symm : (a : M₂) → M₁) x = id x

Tactic:
apply_symm_apply e x

Premises used: ContinuousLinearEquiv.apply_symm_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
⊢ Function.comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := M₁) (⇑e : (a : M₁) → M₂) (⇑e.symm : (a : M₂) → M₁) x = id x

Tactic:
exact apply_symm_apply e x

Premises used: ContinuousLinearEquiv.apply_symm_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
⊢ Function.Bijective (α := M₁ ≃SL[σ₁₂] M₂) ContinuousLinearEquiv.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, ContinuousLinearEquiv.symm_symm
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq (α := M₁ ≃L[R₁] M₁) (ContinuousLinearEquiv.symm (ContinuousLinearEquiv.refl R₁ M₁))
    (ContinuousLinearEquiv.refl R₁ M₁)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.refl, LinearEquiv.refl, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_5 + 1} (α := M₂) ((e.symm.symm : (a : M₁) → M₂) x : M₂) ((e : (a : M₁) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
y : M₁
⊢ (e.symm : (a : M₂) → M₁) x = y ↔ x = (e : (a : M₁) → M₂) y

Tactic:
e.toLinearEquiv.symm_apply_eq

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.symm_apply_eq
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
y : M₁
⊢ y = (e.symm : (a : M₂) → M₁) x ↔ (e : (a : M₁) → M₂) y = x

Tactic:
e.toLinearEquiv.eq_symm_apply

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.eq_symm_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₁
⊢ Eq.{u_5 + 1} (α := Set M₂) ((⇑e : (a : M₁) → M₂) '' s) ((⇑e.symm : (a : M₂) → M₁) ⁻¹' s)

Tactic:
e.toLinearEquiv.toEquiv.image_eq_preimage_symm s

Premises used: ContinuousLinearEquiv.toLinearEquiv, Equiv.image_eq_preimage_symm, LinearEquiv.toEquiv
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
rw : Eq.{u_4 + 1} (α := Set M₁) ((⇑e.symm.symm : (a : M₁) → M₂) ⁻¹' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)
rw₁ rw₂ : Eq.{u_4 + 1} (α := Set M₁) ((⇑e : (a : M₁) → M₂) ⁻¹' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)
⊢ Eq.{u_4 + 1} (α := Set M₁) ((⇑e.symm : (a : M₂) → M₁) '' s) ((⇑e : (a : M₁) → M₂) ⁻¹' s)

Tactic:
rw [e.symm.image_eq_preimage_symm, e.symm_symm]

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.image_eq_preimage_symm, ContinuousLinearEquiv.symm_symm
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ Set.preimage.{u_5, u_4} (β := M₁) (⇑e.symm : (a : M₂) → M₁) ((⇑e : (a : M₁) → M₂) ⁻¹' s) = s

Tactic:
e.toLinearEquiv.toEquiv.symm_preimage_preimage s

Premises used: Equiv.symm_preimage_preimage, ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toEquiv
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₁
⊢ Set.preimage.{u_4, u_5} (β := M₂) (⇑e : (a : M₁) → M₂) ((⇑e.symm : (a : M₂) → M₁) ⁻¹' s) = s

Tactic:
e.symm.symm_preimage_preimage s

Premises used: ContinuousLinearEquiv.symm_preimage_preimage, ContinuousLinearEquiv.symm
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
E₁ : Type u_8
E₂ : Type u_9
inst_4 : UniformSpace E₁
inst_5 : UniformSpace E₂
inst_6 : AddCommGroup E₁
inst_7 : AddCommGroup E₂
inst_8 : Module R₁ E₁
inst_9 : Module R₂ E₂
inst_10 : IsUniformAddGroup E₁
inst_11 : IsUniformAddGroup E₂
e : E₁ ≃SL[σ₁₂] E₂
⊢ IsUniformEmbedding.{u_8, u_9} (α := E₁) (β := E₂) (⇑e : (a : E₁) → E₂)

Tactic:
e.toLinearEquiv.toEquiv.isUniformEmbedding e.toContinuousLinearMap.uniformContinuous
    e.symm.toContinuousLinearMap.uniformContinuous

Premises used: ContinuousLinearEquiv.symm, Equiv.isUniformEmbedding, ContinuousLinearEquiv.toLinearEquiv, ContinuousLinearMap.uniformContinuous, LinearEquiv.toEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
E₁ : Type u_8
E₂ : Type u_9
inst_4 : UniformSpace E₁
inst_5 : UniformSpace E₂
inst_6 : AddCommGroup E₁
inst_7 : AddCommGroup E₂
inst_8 : Module R₁ E₁
inst_9 : Module R₂ E₂
inst_10 : IsUniformAddGroup E₁
inst_11 : IsUniformAddGroup E₂
e : E₁ ≃ₛₗ[σ₁₂] E₂
h₁ : Continuous[inst_4.toTopologicalSpace, inst_5.toTopologicalSpace] (⇑e : (a : E₁) → E₂)
h₂ : Continuous[inst_5.toTopologicalSpace, inst_4.toTopologicalSpace] (⇑e.symm : (a : E₂) → E₁)
⊢ IsUniformEmbedding.{u_8, u_9} (α := E₁) (β := E₂) (⇑e : (a : E₁) → E₂)

Tactic:
ContinuousLinearEquiv.isUniformEmbedding
    ({ e with
        continuous_toFun := h₁
        continuous_invFun := h₂ } :
      E₁ ≃SL[σ₁₂] E₂)

Premises used: ContinuousLinearEquiv.mk, ContinuousLinearEquiv.isUniformEmbedding
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : Function.LeftInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f₂ : (a : M₂) → M₁) (⇑f₁ : (a : M₁) → M₂)
h₂ : Function.RightInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f₂ : (a : M₂) → M₁) (⇑f₁ : (a : M₁) → M₂)
x : M₁
⊢ Eq.{u_5 + 1} (α := M₂) ((equivOfInverse f₁ f₂ h₁ h₂ : (a : M₁) → M₂) x : M₂) ((f₁ : (a : M₁) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
inst_3 : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : Function.LeftInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f₂ : (a : M₂) → M₁) (⇑f₁ : (a : M₁) → M₂)
h₂ : Function.RightInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f₂ : (a : M₂) → M₁) (⇑f₁ : (a : M₁) → M₂)
⊢ Eq (α := M₂ ≃SL[σ₂₁] M₁) (ContinuousLinearEquiv.symm (equivOfInverse f₁ f₂ h₁ h₂)) (equivOfInverse f₂ f₁ h₂ h₁)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.equivOfInverse, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
M₄ : Type u_7
inst_17 : TopologicalSpace M₄
inst_18 : AddCommMonoid M₄
inst_19 : Module R₁ M₁
inst_20 : Module R₂ M₂
inst_21 : Module R₃ M₃
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
x : M₁
⊢ (f₂ : (a : M₂) → M₁) ((f₁ : (a : M₁) → M₂) x : M₂) = x

Tactic:
simpa using congr($(h₂) x)
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_3 : RingHomInvPair σ₁₂ σ₂₁
inst_4 : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst_5 : RingHomInvPair σ₂₃ σ₃₂
inst_6 : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_7 : RingHomInvPair σ₁₃ σ₃₁
inst_8 : RingHomInvPair σ₃₁ σ₁₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_11 : TopologicalSpace M₁
inst_12 : AddCommMonoid M₁
M₂ : Type u_5
inst_13 : TopologicalSpace M₂
inst_14 : AddCommMonoid M₂
M₃ : Type u_6
inst_15 : TopologicalSpace M₃
inst_16 : AddCommMonoid M₃
M₄ : Type u_7
inst_17 : TopologicalSpace M₄
inst_18 : AddCommMonoid M₄
inst_19 : Module R₁ M₁
inst_20 : Module R₂ M₂
inst_21 : Module R₃ M₃
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
x : M₂
⊢ (f₁ : (a : M₁) → M₂) ((f₂ : (a : M₂) → M₁) x : M₁) = x

Tactic:
simpa using congr($(h₁) x)