awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
dsimp :
  Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (if h : i ∈ I then
          LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
        else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (LinearMap.pi (φ := φ) fun (i : ι) ↦
          if h : i ∈ I then
            LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
          else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → (i : ι) → φ i)
      a i

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
pos :
  ∀ (h : i ∈ I),
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
          (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
        a
neg :
  i ∉ I →
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (0 : (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i) a
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (if h : i ∈ I then
          LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
        else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a

Tactic:
split_ifs
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
h : i ∈ I
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a

Tactic:
apply continuous_apply

Premises used: continuous_apply
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
h : i ∉ I
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (0 : (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i) a

Tactic:
continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
h : i ∉ I
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (0 : (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i) a

Tactic:
exact continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
pos :
  ∀ (h : i ∈ I),
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
          (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
        a
neg :
  i ∉ I →
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (0 : (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i) a
pos₁ :
  ∀ (h : i ∈ I),
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
          (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
        a
neg₁ :
  i ∉ I →
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (0 : (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i) a
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (if h : i ∈ I then
          LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
        else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a

Tactic:
split_ifs <;> [apply continuous_apply; exact continuous_zero]

Premises used: continuous_zero, continuous_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 : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂) = (↑(↑e : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂)

Tactic:
rfl

Premises used: 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 g : M₁ ≃SL[σ₁₂] M₂
h₁ : (↑(↑f : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun = (↑(↑g : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun
h₂ : (↑f : M₁ ≃ₛₗ[σ₁₂] M₂).invFun = (↑g : M₁ ≃ₛₗ[σ₁₂] M₂).invFun
obtain :
  ∀ (f' : M₁ ≃ₛₗ[σ₁₂] M₂) (continuous_toFun : Continuous[inst_11, inst_13] (↑f' : M₁ →ₛₗ[σ₁₂] M₂).toFun)
    (continuous_invFun : Continuous[inst_13, inst_11] f'.invFun)
    (h₁ :
      (↑(↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                    M₁ ≃SL[σ₁₂] M₂ } :
                M₁ ≃ₛₗ[σ₁₂] M₂) :
            M₁ →ₛₗ[σ₁₂] M₂).toFun =
        (↑(↑g : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun)
    (h₂ :
      (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
        (↑g : M₁ ≃ₛₗ[σ₁₂] M₂).invFun),
    { toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M₁ ≃SL[σ₁₂] M₂ } =
      g
⊢ f = g

Tactic:
obtain ⟨f', _⟩ := f
-- 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₃
g : M₁ ≃SL[σ₁₂] M₂
f' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun : Continuous[inst_11, inst_13] (↑f' : M₁ →ₛₗ[σ₁₂] M₂).toFun
continuous_invFun : Continuous[inst_13, inst_11] f'.invFun
h₁ :
  (↑(↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂) :
        M₁ →ₛₗ[σ₁₂] M₂).toFun =
    (↑(↑g : M₁ ≃ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂).toFun
h₂ :
  (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            M₁ ≃SL[σ₁₂] M₂ } :
        M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
    (↑g : M₁ ≃ₛₗ[σ₁₂] M₂).invFun
obtain :
  ∀ (g' : M₁ ≃ₛₗ[σ₁₂] M₂) (continuous_toFun_1 : Continuous[inst_11, inst_13] (↑g' : M₁ →ₛₗ[σ₁₂] M₂).toFun)
    (continuous_invFun_1 : Continuous[inst_13, inst_11] g'.invFun)
    (h₁ :
      (↑(↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                    M₁ ≃SL[σ₁₂] M₂ } :
                M₁ ≃ₛₗ[σ₁₂] M₂) :
            M₁ →ₛₗ[σ₁₂] M₂).toFun =
        (↑(↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
                    M₁ ≃SL[σ₁₂] M₂ } :
                M₁ ≃ₛₗ[σ₁₂] M₂) :
            M₁ →ₛₗ[σ₁₂] M₂).toFun)
    (h₂ :
      (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂).invFun =
        (↑{ toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂).invFun),
    { toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M₁ ≃SL[σ₁₂] M₂ } =
      { toLinearEquiv := g', continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
⊢ { toLinearEquiv := f', continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
      M₁ ≃SL[σ₁₂] M₂ } =
    g

Tactic:
obtain ⟨g', _⟩ := g
-- 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₁ ≃ₛₗ[σ₁₂] M₂
a : Continuous[inst_4, inst_6] (↑e : M₁ →ₛₗ[σ₁₂] M₂).toFun
b : Continuous[inst_6, inst_4] e.invFun
⊢ Eq (α := (a : M₁) → M₂)
    (⇑{ toLinearEquiv := e, continuous_toFun := a, continuous_invFun := b : M₁ ≃SL[σ₁₂] M₂ } : (a : M₁) → M₂)
    (⇑e : (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₂
b : M₁
⊢ Eq.{u_5 + 1} (α := M₂) (((↑e : M₁ →SL[σ₁₂] M₂) : (a : M₁) → M₂) b : M₂) ((e : (a : M₁) → M₂) b : 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₂
⊢ Eq (α := (a : M₁) → M₂) (⇑(↑f : M₁ ≃ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (⇑f : (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₂
⊢ Eq (α := (a : M₁) → M₂) (⇑(↑e : M₁ →SL[σ₁₂] M₂) : (a : M₁) → M₂) (⇑e : (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₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun : Continuous[inst_4, inst_6] (↑e : M₁ →ₛₗ[σ₁₂] M₂).toFun
continuous_invFun : Continuous[inst_6, inst_4] e.invFun
continuous_toFun_1 :
  Continuous[inst_4, inst_6]
    (↑(↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
                M₁ ≃SL[σ₁₂] M₂ } :
            M₁ ≃ₛₗ[σ₁₂] M₂) :
        M₁ →ₛₗ[σ₁₂] M₂).toFun
continuous_invFun_1 :
  Continuous[inst_6, inst_4]
    (↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
            M₁ ≃SL[σ₁₂] M₂ } :
        M₁ ≃ₛₗ[σ₁₂] M₂).invFun
⊢ { toLinearEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
      M₁ ≃SL[σ₁₂] M₂ } =
    {
      toLinearEquiv :=
        (↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
              M₁ ≃SL[σ₁₂] M₂ } :
          M₁ ≃ₛₗ[σ₁₂] M₂),
      continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }

Tactic:
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 g : M₁ ≃SL[σ₁₂] M₂
h : Eq (α := (a : M₁) → M₂) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₁) → M₂)
⊢ f = g

Tactic:
toLinearEquiv_injective <| LinearEquiv.ext <| congr_fun h

Premises used: LinearEquiv.ext, ContinuousLinearEquiv.toLinearEquiv_injective, congr_fun
-- 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.Injective (α := M₁ ≃SL[σ₁₂] M₂) toContinuousLinearMap

Tactic:
fun _e _e' h => ext <| funext <| ContinuousLinearMap.ext_iff.1 h

Premises used: ContinuousLinearEquiv.ext, funext, ContinuousLinearMap.ext_iff, Iff.mp, Function.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 e' : M₁ ≃SL[σ₁₂] M₂
⊢ (↑e : M₁ →SL[σ₁₂] M₂) = (↑e' : M₁ →SL[σ₁₂] M₂) ↔ e = e'

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, ContinuousLinearEquiv.coe_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₂
⊢ Eq (α := (a : M₁) → M₂) (⇑e.toHomeomorph : (a : M₁) → M₂) (⇑e : (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₂
⊢ IsOpenMap.{u_4, u_5} (X := M₁) (Y := M₂) (⇑e : (a : M₁) → M₂)

Tactic:
(ContinuousLinearEquiv.toHomeomorph e).isOpenMap

Premises used: ContinuousLinearEquiv.toHomeomorph, Homeomorph.isOpenMap
-- 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₂) '' closure[inst_4] s) (closure[inst_6] ((⇑e : (a : M₁) → M₂) '' s))

Tactic:
e.toHomeomorph.image_closure s

Premises used: Homeomorph.image_closure, 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₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ Eq.{u_4 + 1} (α := Set M₁) ((⇑e : (a : M₁) → M₂) ⁻¹' closure[inst_6] s) (closure[inst_4] ((⇑e : (a : M₁) → M₂) ⁻¹' s))

Tactic:
e.toHomeomorph.preimage_closure s

Premises used: Homeomorph.preimage_closure, 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₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₁
⊢ IsClosed[inst_6] ((⇑e : (a : M₁) → M₂) '' s) ↔ IsClosed[inst_4] s

Tactic:
e.toHomeomorph.isClosed_image

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

Tactic:
e.toHomeomorph.map_nhds_eq x

Premises used: Homeomorph.map_nhds_eq, 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₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ Eq.{u_5 + 1} (α := M₂) ((e : (a : M₁) → M₂) 0 : M₂) (0 : M₂)

Tactic:
(e : M₁ →SL[σ₁₂] M₂).map_zero

Premises used: ContinuousLinearMap.map_zero, 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₂
x y : M₁
⊢ (e : (a : M₁) → M₂) (x + y) = HAdd.hAdd (α := M₂) (β := M₂) ((e : (a : M₁) → M₂) x : M₂) ((e : (a : M₁) → M₂) y : M₂)

Tactic:
(e : M₁ →SL[σ₁₂] M₂).map_add x y

Premises used: ContinuousLinearMap.map_add, 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₂
c : R₁
x : M₁
⊢ (e : (a : M₁) → M₂) (c • x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R₂) (β := M₂) ((σ₁₂ : (a : R₁) → R₂) c : R₂) ((e : (a : M₁) → M₂) x : M₂)

Tactic:
(e : M₁ →SL[σ₁₂] M₂).map_smulₛₗ c x

Premises used: ContinuousLinearMap.map_smulₛₗ, 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₂
inst_5 : Module R₁ M₁
inst_6 : Module R₁ M₂
e : M₁ ≃L[R₁] M₂
c : R₁
x : M₁
⊢ (e : (a : M₁) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((e : (a : M₁) → M₂) x : M₂)

Tactic:
(e : M₁ →L[R₁] M₂).map_smul c x

Premises used: ContinuousLinearEquiv.toContinuousLinearMap, ContinuousLinearMap.map_smul