awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (a : M₁) → M₂) x : M₂) (0 : M₂) ↔ x = 0

Tactic:
e.toLinearEquiv.map_eq_zero_iff

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.map_eq_zero_iff
-- 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₂
⊢ Continuous[inst_4, inst_6] (⇑e : (a : M₁) → M₂)

Tactic:
e.continuous_toFun

Premises used: ContinuousLinearEquiv.continuous_toFun
-- 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₁
⊢ ContinuousOn.{u_4, u_5} (Y := M₂) (⇑e : (a : M₁) → M₂) s

Tactic:
e.continuous.continuousOn

Premises used: Continuous.continuousOn, ContinuousLinearEquiv.continuous
-- 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₁
⊢ ContinuousAt.{u_4, u_5} (Y := M₂) (⇑e : (a : M₁) → M₂) x

Tactic:
e.continuous.continuousAt

Premises used: Continuous.continuousAt, ContinuousLinearEquiv.continuous
-- 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₁
x : M₁
⊢ ContinuousWithinAt.{u_4, u_5} (Y := M₂) (⇑e : (a : M₁) → M₂) s x

Tactic:
e.continuous.continuousWithinAt

Premises used: ContinuousLinearEquiv.continuous, Continuous.continuousWithinAt
-- 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₂
α : Type u_8
inst_10 : TopologicalSpace α
e : M₁ ≃SL[σ₁₂] M₂
f : α → M₁
s : Set α
⊢ ContinuousOn.{u_8, u_5} (Y := M₂) ((⇑e : (a : M₁) → M₂) ∘ f) s ↔ ContinuousOn f s

Tactic:
e.toHomeomorph.comp_continuousOn_iff _ _

Premises used: Homeomorph.comp_continuousOn_iff, ContinuousLinearEquiv.toHomeomorph
-- 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₂
α : Type u_8
inst_10 : TopologicalSpace α
e : M₁ ≃SL[σ₁₂] M₂
f : α → M₁
⊢ Continuous[inst_10, inst_6] ((⇑e : (a : M₁) → M₂) ∘ f) ↔ Continuous[inst_10, inst_4] f

Tactic:
e.toHomeomorph.comp_continuous_iff

Premises used: Homeomorph.comp_continuous_iff, ContinuousLinearEquiv.toHomeomorph
-- 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₁
inst_4 : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) 1 : M₁) ((g : (a : R₁) → M₁) 1 : M₁)
x : R₁
rw :
  Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
    ((g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1) : M₁)
rw₁ : HSMul.hSMul (β := M₁) x ((f : (a : R₁) → M₁) 1 : M₁) = (g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1)
rw₂ : HSMul.hSMul (β := M₁) x ((g : (a : R₁) → M₁) 1 : M₁) = (g : (a : R₁) → M₁) (HSMul.hSMul (β := R₁) x 1)
rw₃ rw₄ : HSMul.hSMul (β := M₁) x ((g : (a : R₁) → M₁) 1 : M₁) = HSMul.hSMul (β := M₁) x ((g : (a : R₁) → M₁) 1 : M₁)
⊢ Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) (x * 1) : M₁) ((g : (a : R₁) → M₁) (x * 1) : M₁)

Tactic:
rw [← smul_eq_mul, map_smul, h, map_smul]

Premises used: ContinuousLinearEquiv.map_smul, smul_eq_mul
-- 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₁
M : Type u_8
inst_4 : TopologicalSpace M
inst_5 : AddCommMonoid M
inst_6 : Module R₁ M
e : M₁ ≃L[R₁] M
⊢ Eq (α := (a : M₁) → M) (⇑e.toContinuousAddEquiv : (a : M₁) → M) (⇑e : (a : M₁) → M)

Tactic:
rfl

Premises used: rfl
-- 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₁
x : M₁
⊢ (ContinuousLinearEquiv.refl R₁ M₁ : (a : M₁) → M₁) x = x

Tactic:
rfl

Premises used: rfl
-- 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.refl R₁ M₁) : M₁ →L[R₁] M₁) (ContinuousLinearMap.id R₁ M₁)

Tactic:
rfl

Premises used: ContinuousLinearMap.id, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- 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 (α := (a : M₁) → M₁) (⇑(ContinuousLinearEquiv.refl R₁ M₁) : (a : M₁) → M₁) id

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₂
⊢ (↑e.symm : M₂ ≃ₛₗ[σ₂₁] M₁) = (↑e : M₁ ≃ₛₗ[σ₁₂] M₂).symm

Tactic:
rfl

Premises used: 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₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ Eq (α := (a : M₂) → M₁) (⇑(↑e : M₁ ≃ₛₗ[σ₁₂] M₂).symm : (a : M₂) → M₁) (⇑e.symm : (a : 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₂
⊢ e.symm.toHomeomorph = e.toHomeomorph.symm

Tactic:
rfl

Premises used: Homeomorph.symm, Equiv.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₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ Eq (α := (a : M₂) → M₁) (⇑e.toHomeomorph.symm : (a : M₂) → M₁) (⇑e.symm : (a : 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₂
x : M₁
⊢ map.{u_5, u_4} (α := M₂) ((⇑e.symm : (a : M₂) → M₁) : (a : M₂) → M₁) (𝓝 ((e : (a : M₁) → M₂) x) : Filter M₂) = 𝓝 x

Tactic:
e.toHomeomorph.symm_map_nhds_eq x

Premises used: ContinuousLinearEquiv.toHomeomorph, Homeomorph.symm_map_nhds_eq
-- 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₃
h :
  ∀ (x : M₁),
    Eq.{u_6 + 1} (α := M₃) (((↑(e₁.trans e₂) : M₁ ≃ₛₗ[σ₁₃] M₃) : (a : M₁) → M₃) x : M₃)
      (((↑e₁ : M₁ ≃ₛₗ[σ₁₂] M₂).trans (↑e₂ : M₂ ≃ₛₗ[σ₂₃] M₃) : (a : M₁) → M₃) x : M₃)
⊢ Eq (α := M₁ ≃ₛₗ[σ₁₃] M₃) (↑(e₁.trans e₂) : M₁ ≃ₛₗ[σ₁₃] M₃) ((↑e₁ : M₁ ≃ₛₗ[σ₁₂] M₂).trans (↑e₂ : M₂ ≃ₛₗ[σ₂₃] M₃))

Tactic:
ext
-- 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₃
x : M₁
⊢ Eq.{u_6 + 1} (α := M₃) (((↑(e₁.trans e₂) : M₁ ≃ₛₗ[σ₁₃] M₃) : (a : M₁) → M₃) x : M₃)
    (((↑e₁ : M₁ ≃ₛₗ[σ₁₂] M₂).trans (↑e₂ : M₂ ≃ₛₗ[σ₂₃] M₃) : (a : M₁) → M₃) x : M₃)

Tactic:
rfl
-- 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₁
M₂ : Type u_5
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
M₃ : Type u_6
inst_5 : TopologicalSpace M₃
inst_6 : AddCommMonoid M₃
M₄ : Type u_7
inst_7 : TopologicalSpace M₄
inst_8 : AddCommMonoid M₄
inst_9 : Module R₁ M₁
inst_10 : Module R₁ M₂
inst_11 : Module R₁ M₃
inst_12 : Module R₁ M₄
e : M₁ ≃L[R₁] M₂
e' : M₃ ≃L[R₁] M₄
x : M₁ × M₃
⊢ Eq (α := M₂ × M₄) ((e.prodCongr e' : (a : M₁ × M₃) → M₂ × M₄) x : M₂ × M₄)
    (((e : (a : M₁) → M₂) x.1, (e' : (a : M₃) → M₄) x.2) : M₂ × M₄)

Tactic:
rfl

Premises used: Prod.map, rfl
-- 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₁
M₂ : Type u_5
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
M₃ : Type u_6
inst_5 : TopologicalSpace M₃
inst_6 : AddCommMonoid M₃
M₄ : Type u_7
inst_7 : TopologicalSpace M₄
inst_8 : AddCommMonoid M₄
inst_9 : Module R₁ M₁
inst_10 : Module R₁ M₂
inst_11 : Module R₁ M₃
inst_12 : Module R₁ M₄
e : M₁ ≃L[R₁] M₂
e' : M₃ ≃L[R₁] M₄
⊢ (↑(e.prodCongr e') : M₁ × M₃ →L[R₁] M₂ × M₄) = (↑e : M₁ →L[R₁] M₂).prodMap (↑e' : M₃ →L[R₁] M₄)

Tactic:
rfl

Premises used: ContinuousLinearMap.prodMap, Prod.map, Function.prod, ContinuousLinearMap.prod, LinearMap.prod, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- 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₁
M₂ : Type u_5
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
M₃ : Type u_6
inst_5 : TopologicalSpace M₃
inst_6 : AddCommMonoid M₃
M₄ : Type u_7
inst_7 : TopologicalSpace M₄
inst_8 : AddCommMonoid M₄
inst_9 : Module R₁ M₁
inst_10 : Module R₁ M₂
inst_11 : Module R₁ M₃
inst_12 : Module R₁ M₄
e : M₁ ≃L[R₁] M₂
e' : M₃ ≃L[R₁] M₄
⊢ (e.prodCongr e').symm = e.symm.prodCongr e'.symm

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, LinearEquiv.prodCongr, Prod.map, ContinuousLinearEquiv.prodCongr, rfl
-- 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₁
M₂ : Type u_5
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₁ M₁
inst_6 : Module R₁ M₂
⊢ Eq (α := (M₂ × M₁) ≃L[R₁] M₁ × M₂) (ContinuousLinearEquiv.symm (prodComm R₁ M₁ M₂)) (prodComm R₁ M₂ M₁)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, LinearEquiv.prodComm, ContinuousLinearEquiv.prodComm, Prod.swap, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : TopologicalSpace M₁
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
⊢ Eq (α := ((M₁ × M₂) × M₃) ≃ₗ[R] M₁ × M₂ × M₃) (↑(prodAssoc R M₁ M₂ M₃) : ((M₁ × M₂) × M₃) ≃ₗ[R] M₁ × M₂ × M₃)
    (LinearEquiv.prodAssoc R M₁ M₂ M₃)

Tactic:
rfl

Premises used: LinearEquiv.prodAssoc, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : TopologicalSpace M₁
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
⊢ Eq (α := (a : (M₁ × M₂) × M₃) → M₁ × M₂ × M₃) (⇑(prodAssoc R M₁ M₂ M₃) : (a : (M₁ × M₂) × M₃) → M₁ × M₂ × M₃)
    (⇑(Equiv.prodAssoc M₁ M₂ M₃) : (a : (M₁ × M₂) × M₃) → M₁ × M₂ × M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : TopologicalSpace M₁
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
p₁ : M₁
p₂ : M₂
p₃ : M₃
⊢ (prodAssoc R M₁ M₂ M₃ : (a : (M₁ × M₂) × M₃) → M₁ × M₂ × M₃) ((p₁, p₂), p₃) = (p₁, p₂, p₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : TopologicalSpace M₁
inst_8 : TopologicalSpace M₂
inst_9 : TopologicalSpace M₃
p₁ : M₁
p₂ : M₂
p₃ : M₃
⊢ (ContinuousLinearEquiv.symm (prodAssoc R M₁ M₂ M₃) : (a : M₁ × M₂ × M₃) → (M₁ × M₂) × M₃) (p₁, p₂, p₃) =
    ((p₁, p₂), p₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
M₄ : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : TopologicalSpace M₁
inst_10 : TopologicalSpace M₂
inst_11 : TopologicalSpace M₃
inst_12 : TopologicalSpace M₄
⊢ Eq (α := ((M₁ × M₃) × M₂ × M₄) ≃L[R] (M₁ × M₂) × M₃ × M₄)
    (ContinuousLinearEquiv.symm (prodProdProdComm R M₁ M₂ M₃ M₄)) (prodProdProdComm R M₁ M₃ M₂ M₄)

Tactic:
rfl

Premises used: LinearEquiv.prodProdProdComm, ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.prodProdProdComm, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
M₄ : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : TopologicalSpace M₁
inst_10 : TopologicalSpace M₂
inst_11 : TopologicalSpace M₃
inst_12 : TopologicalSpace M₄
⊢ Eq (α := ((M₁ × M₂) × M₃ × M₄) ≃ₗ[R] (M₁ × M₃) × M₂ × M₄)
    (↑(prodProdProdComm R M₁ M₂ M₃ M₄) : ((M₁ × M₂) × M₃ × M₄) ≃ₗ[R] (M₁ × M₃) × M₂ × M₄)
    (LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄)

Tactic:
rfl

Premises used: LinearEquiv.prodProdProdComm, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
M₄ : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : TopologicalSpace M₁
inst_10 : TopologicalSpace M₂
inst_11 : TopologicalSpace M₃
inst_12 : TopologicalSpace M₄
⊢ Eq (α := (a : (M₁ × M₂) × M₃ × M₄) → (M₁ × M₃) × M₂ × M₄)
    (⇑(prodProdProdComm R M₁ M₂ M₃ M₄) : (a : (M₁ × M₂) × M₃ × M₄) → (M₁ × M₃) × M₂ × M₄)
    (⇑(Equiv.prodProdProdComm M₁ M₂ M₃ M₄) : (a : (M₁ × M₂) × M₃ × M₄) → (M₁ × M₃) × M₂ × M₄)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
M₄ : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
inst_9 : TopologicalSpace M₁
inst_10 : TopologicalSpace M₂
inst_11 : TopologicalSpace M₃
inst_12 : TopologicalSpace M₄
p₁ : M₁
p₂ : M₂
p₃ : M₃
p₄ : M₄
⊢ (prodProdProdComm R M₁ M₂ M₃ M₄ : (a : (M₁ × M₂) × M₃ × M₄) → (M₁ × M₃) × M₂ × M₄) ((p₁, p₂), p₃, p₄) =
    ((p₁, p₃), p₂, p₄)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace N
inst_4 : AddCommMonoid N
inst_5 : Unique N
inst_6 : Module R M
inst_7 : Module R N
⊢ LinearEquiv.toEquiv (modM := Prod.instModule) (↑(prodUnique R M N) : (M × N) ≃ₗ[R] M) = Equiv.prodUnique M N

Tactic:
rfl

Premises used: Equiv.trans, Equiv.prodUnique, LinearEquiv.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace N
inst_4 : AddCommMonoid N
inst_5 : Unique N
inst_6 : Module R M
inst_7 : Module R N
x : M × N
⊢ (prodUnique R M N : (a : M × N) → M) x = x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace N
inst_4 : AddCommMonoid N
inst_5 : Unique N
inst_6 : Module R M
inst_7 : Module R N
x : M
⊢ Eq (α := M × N) ((ContinuousLinearEquiv.symm (prodUnique R M N) : (a : M) → M × N) x : M × N) ((x, default) : M × N)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace N
inst_4 : AddCommMonoid N
inst_5 : Unique N
inst_6 : Module R M
inst_7 : Module R N
⊢ LinearEquiv.toEquiv (modM := Prod.instModule) (↑(uniqueProd R M N) : (N × M) ≃ₗ[R] M) = Equiv.uniqueProd M N

Tactic:
rfl

Premises used: Equiv.trans, Equiv.uniqueProd, LinearEquiv.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace N
inst_4 : AddCommMonoid N
inst_5 : Unique N
inst_6 : Module R M
inst_7 : Module R N
x : N × M
⊢ (uniqueProd R M N : (a : N × M) → M) x = x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace N
inst_4 : AddCommMonoid N
inst_5 : Unique N
inst_6 : Module R M
inst_7 : Module R N
x : M
⊢ Eq (α := N × M) ((ContinuousLinearEquiv.symm (uniqueProd R M N) : (a : M) → N × M) x : N × M) ((default, x) : N × M)

Tactic:
rfl

Premises used: Prod.map, 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₂
⊢ Function.Bijective.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑e : (a : M₁) → M₂)

Tactic:
e.toLinearEquiv.toEquiv.bijective

Premises used: Equiv.bijective, 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₂
⊢ Function.Injective.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑e : (a : M₁) → M₂)

Tactic:
e.toLinearEquiv.toEquiv.injective

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toEquiv, Equiv.injective
-- 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₂
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑e : (a : M₁) → M₂)

Tactic:
e.toLinearEquiv.toEquiv.surjective

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toEquiv, Equiv.surjective