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₂
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₁
⊢ 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₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
⊢ Eq (α := M₂ ≃SL[σ₂₁] M₁) (ContinuousLinearEquiv.symm (equivOfInverse' f₁ f₂ h₁ h₂)) (equivOfInverse' f₂ f₁ h₂ h₁)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.equivOfInverse', 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 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
M₁ : Type u_4
inst_6 : TopologicalSpace M₁
inst_7 : AddCommMonoid M₁
M₂ : Type u_5
inst_8 : TopologicalSpace M₂
inst_9 : AddCommMonoid M₂
M₃ : Type u_6
inst_10 : TopologicalSpace M₃
inst_11 : AddCommMonoid M₃
inst_12 : Module R₁ M₁
inst_13 : Module R₂ M₂
inst_14 : Module R₃ M₃
e₁₂ : M₁ ≃SL[σ₁₂] M₂
inst_15 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →SL[σ₂₃] M₃
g : M₁ →SL[σ₁₃] M₃
⊢ f = g ∘SL (↑e₁₂.symm : M₂ →SL[σ₂₁] M₁) ↔ f ∘SL (↑e₁₂ : M₁ →SL[σ₁₂] M₂) = g

Tactic:
aesop
-- 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 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst_6 : TopologicalSpace M₁
inst_7 : AddCommMonoid M₁
M₂ : Type u_5
inst_8 : TopologicalSpace M₂
inst_9 : AddCommMonoid M₂
M₃ : Type u_6
inst_10 : TopologicalSpace M₃
inst_11 : AddCommMonoid M₃
inst_12 : Module R₁ M₁
inst_13 : Module R₂ M₂
inst_14 : Module R₃ M₃
e₁₂ : M₁ ≃SL[σ₁₂] M₂
inst_15 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →SL[σ₃₁] M₁
g : M₃ →SL[σ₃₂] M₂
⊢ f = (↑e₁₂.symm : M₂ →SL[σ₂₁] M₁) ∘SL g ↔ (↑e₁₂ : M₁ →SL[σ₁₂] M₂) ∘SL f = g

Tactic:
aesop
-- 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.{u_4 + 1} (α := M₁ →L[R₁] M₁) (↑1 : M₁ →L[R₁] M₁) 1

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₁
e e' : M₁ ≃L[R₁] M₁
⊢ (↑(e * e') : M₁ →L[R₁] M₁) = (↑e : M₁ →L[R₁] M₁) * (↑e' : M₁ →L[R₁] 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
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₃
R₄ : Type u_8
inst_22 : Semiring R₄
inst_23 : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_24 : RingHomInvPair σ₃₄ σ₄₃
inst_25 : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst_26 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_27 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_28 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
f : M₁ →SL[σ₁₄] M₄
x : M₁
⊢ Eq.{u_7 + 1} (α := M₄)
    (((fun (f : M₂ →SL[σ₂₃] M₃) ↦ (↑e₄₃.symm : M₃ →SL[σ₃₄] M₄) ∘SL f ∘SL (↑e₁₂ : M₁ →SL[σ₁₂] M₂))
            ((fun (f : M₁ →SL[σ₁₄] M₄) ↦ (↑e₄₃ : M₄ →SL[σ₄₃] M₃) ∘SL f ∘SL (↑e₁₂.symm : M₂ →SL[σ₂₁] M₁)) f) :
          (a : M₁) → M₄)
        x :
      M₄)
    ((f : (a : M₁) → M₄) x : M₄)

Tactic:
simp only [ContinuousLinearMap.comp_apply, symm_apply_apply, coe_coe]

Premises used: ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearEquiv.coe_coe, ContinuousLinearMap.comp_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₃
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₃
R₄ : Type u_8
inst_22 : Semiring R₄
inst_23 : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_24 : RingHomInvPair σ₃₄ σ₄₃
inst_25 : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst_26 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_27 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_28 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
f : M₂ →SL[σ₂₃] M₃
x : M₂
⊢ Eq.{u_6 + 1} (α := M₃)
    (((fun (f : M₁ →SL[σ₁₄] M₄) ↦ (↑e₄₃ : M₄ →SL[σ₄₃] M₃) ∘SL f ∘SL (↑e₁₂.symm : M₂ →SL[σ₂₁] M₁))
            ((fun (f : M₂ →SL[σ₂₃] M₃) ↦ (↑e₄₃.symm : M₃ →SL[σ₃₄] M₄) ∘SL f ∘SL (↑e₁₂ : M₁ →SL[σ₁₂] M₂)) f) :
          (a : M₂) → M₃)
        x :
      M₃)
    ((f : (a : M₂) → M₃) x : M₃)

Tactic:
simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]

Premises used: ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.coe_coe, ContinuousLinearMap.comp_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₃
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₃
R₄ : Type u_8
inst_22 : Semiring R₄
inst_23 : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_24 : RingHomInvPair σ₃₄ σ₄₃
inst_25 : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst_26 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_27 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_28 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_29 : SMulCommClass R₃ R₃ M₃
inst_30 : SMulCommClass R₄ R₄ M₄
inst_31 : ContinuousAdd M₃
inst_32 : ContinuousConstSMul R₃ M₃
inst_33 : ContinuousAdd M₄
inst_34 : ContinuousConstSMul R₄ M₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
⊢ ∀ (x y : M₁ →SL[σ₁₄] M₄),
    (e₁₂.arrowCongrEquiv e₄₃).toFun (x + y) = (e₁₂.arrowCongrEquiv e₄₃).toFun x + (e₁₂.arrowCongrEquiv e₄₃).toFun y

Tactic:
simp
-- 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₃
R₄ : Type u_8
inst_22 : Semiring R₄
inst_23 : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst_24 : RingHomInvPair σ₃₄ σ₄₃
inst_25 : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst_26 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst_27 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst_28 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_29 : SMulCommClass R₃ R₃ M₃
inst_30 : SMulCommClass R₄ R₄ M₄
inst_31 : ContinuousAdd M₃
inst_32 : ContinuousConstSMul R₃ M₃
inst_33 : ContinuousAdd M₄
inst_34 : ContinuousConstSMul R₄ M₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
⊢ ∀ (m : R₄) (x : M₁ →SL[σ₁₄] M₄),
    (e₁₂.arrowCongrEquiv e₄₃).toFun (m • x) =
      HSMul.hSMul (α := R₃) ((σ₄₃ : (a : R₄) → R₃) m : R₃) ((e₁₂.arrowCongrEquiv e₄₃).toFun x)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
inst : Semiring R₁
ι : Type u_9
M : ι → Type u_10
inst_1 : (i : ι) → TopologicalSpace (M i)
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_10} R₁ (M i)
N : ι → Type u_11
inst_4 : (i : ι) → TopologicalSpace (N i)
inst_5 : (i : ι) → AddCommMonoid (N i)
inst_6 : (i : ι) → Module.{u_1, u_11} R₁ (N i)
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_10, u_11} (RingHom.id R₁) (M i) (N i)
m : (i : ι) → M i
i : ι
⊢ Eq.{u_11 + 1} (α := N i) ((piCongrRight (M := M) (N := N) f : (a : (i : ι) → M i) → (i : ι) → N i) m i : N i)
    ((f i : (a : M i) → N i) (m i) : N i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R₁ : Type u_1
inst : Semiring R₁
ι : Type u_9
M : ι → Type u_10
inst_1 : (i : ι) → TopologicalSpace (M i)
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_10} R₁ (M i)
N : ι → Type u_11
inst_4 : (i : ι) → TopologicalSpace (N i)
inst_5 : (i : ι) → AddCommMonoid (N i)
inst_6 : (i : ι) → Module.{u_1, u_11} R₁ (N i)
f : (i : ι) → ContinuousLinearEquiv.{u_1, u_1, u_10, u_11} (RingHom.id R₁) (M i) (N i)
n : (i : ι) → N i
i : ι
⊢ Eq.{u_10 + 1} (α := M i) (((piCongrRight (M := M) (N := N) f).symm : (a : (i : ι) → N i) → (i : ι) → M i) n i : M i)
    (((f i).symm : (a : N i) → M i) (n i) : M i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
⊢ ∀ (x y : M),
    ((↑f : M →L[R] M) : (a : M) → M) (x + y) =
      HAdd.hAdd (α := M) (β := M) (((↑f : M →L[R] M) : (a : M) → M) x : M) (((↑f : M →L[R] M) : (a : M) → M) y : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
⊢ ∀ (m : R) (x : M),
    ((↑f : M →L[R] M) : (a : M) → M) (m • x) =
      HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) m : R) (((↑f : M →L[R] M) : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
rw : (1 : (a : M) → M) x = x
⊢ (f.inv * (↑f : M →L[R] M) : (a : M) → M) x = x

Tactic:
rw [f.inv_val]

Premises used: Units.inv_val
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ (1 : (a : M) → M) x = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
rw : (1 : (a : M) → M) x = x
⊢ ((↑f : M →L[R] M) * f.inv : (a : M) → M) x = x

Tactic:
rw [f.val_inv]

Premises used: Units.val_inv
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : M ≃L[R] M
h : ∀ (x : M), Eq (α := M) (((↑f : M →L[R] M) * (↑f.symm : M →L[R] M) : (a : M) → M) x : M) ((1 : (a : M) → M) x : M)
⊢ (↑f : M →L[R] M) * (↑f.symm : M →L[R] M) = 1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : M ≃L[R] M
x : M
⊢ Eq (α := M) (((↑f : M →L[R] M) * (↑f.symm : M →L[R] M) : (a : M) → M) x : M) ((1 : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : M ≃L[R] M
h : ∀ (x : M), Eq (α := M) (((↑f.symm : M →L[R] M) * (↑f : M →L[R] M) : (a : M) → M) x : M) ((1 : (a : M) → M) x : M)
⊢ (↑f.symm : M →L[R] M) * (↑f : M →L[R] M) = 1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : M ≃L[R] M
x : M
⊢ Eq (α := M) (((↑f.symm : M →L[R] M) * (↑f : M →L[R] M) : (a : M) → M) x : M) ((1 : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
x y : (M →L[R] M)ˣ
h : ∀ (x_1 : M), Eq (α := M) ((ofUnit (x * y) : (a : M) → M) x_1 : M) ((ofUnit x * ofUnit y : (a : M) → M) x_1 : M)
⊢ ofUnit (x * y) = ofUnit x * ofUnit y

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
x y : (M →L[R] M)ˣ
x_1 : M
⊢ Eq (α := M) ((ofUnit (x * y) : (a : M) → M) x_1 : M) ((ofUnit x * ofUnit y : (a : M) → M) x_1 : M)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ Eq (α := M) ((((unitsEquiv R M : (a : (M →L[R] M)ˣ) → M ≃L[R] M) f : M ≃L[R] M) : (a : M) → M) x : M)
    (((↑f : M →L[R] M) : (a : M) → M) x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
u : Rˣ
x : R
⊢ (ContinuousLinearMap.smulRight (S := R) 1 (↑u⁻¹ : R) : (a : R) → R)
      ((ContinuousLinearMap.smulRight (S := R) 1 (↑u : R) : (a : R) → R) x : R) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
u : Rˣ
x : R
⊢ (ContinuousLinearMap.smulRight (S := R) 1 (↑u : R) : (a : R) → R)
      ((ContinuousLinearMap.smulRight (S := R) 1 (↑u⁻¹ : R) : (a : R) → R) x : R) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e.symm : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) 1) : R) (1 : R)
rw₂ : Eq (α := R) ((e.symm : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
rw₃ : Eq (α := R) ((e.symm : (a : R) → R) ((e : (a : R) → R) 1 : R) : R) (1 : R)
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) (β := R) ((e : (a : R) → R) 1 : R) ((e.symm : (a : R) → R) 1 : R) = 1

Tactic:
rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply]

Premises used: ContinuousLinearEquiv.map_smul, smul_eq_mul, ContinuousLinearEquiv.symm_apply_apply, mul_one
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
rw : HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1
rw₁ : Eq (α := R) ((e : (a : R) → R) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) 1) : R) (1 : R)
rw₂ : Eq (α := R) ((e : (a : R) → R) (HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) (1 : R)) : R) (1 : R)
rw₃ : Eq (α := R) ((e : (a : R) → R) ((e.symm : (a : R) → R) 1 : R) : R) (1 : R)
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) (β := R) ((e.symm : (a : R) → R) 1 : R) ((e : (a : R) → R) 1 : R) = 1

Tactic:
rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]

Premises used: ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.map_smul, smul_eq_mul, mul_one
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
u : Rˣ
⊢ (↑((fun (e : R ≃L[R] R) ↦
            ({ val := (e : (a : R) → R) 1, inv := (e.symm : (a : R) → R) 1, val_inv := ⋯, inv_val := ⋯ } : Rˣ))
          ((fun (u : Rˣ) ↦
              (equivOfInverse (ContinuousLinearMap.smulRight (S := R) 1 (↑u : R))
                  (ContinuousLinearMap.smulRight (S := R) 1 (↑u⁻¹ : R)) ⋯ ⋯ :
                R ≃L[R] R))
            u)) :
      R) =
    (↑u : R)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
⊢ Eq (α := R)
    (((fun (u : Rˣ) ↦
              (equivOfInverse (ContinuousLinearMap.smulRight (S := R) 1 (↑u : R))
                  (ContinuousLinearMap.smulRight (S := R) 1 (↑u⁻¹ : R)) ⋯ ⋯ :
                R ≃L[R] R))
            ((fun (e : R ≃L[R] R) ↦
                ({ val := (e : (a : R) → R) 1, inv := (e.symm : (a : R) → R) 1, val_inv := ⋯, inv_val := ⋯ } : Rˣ))
              e) :
          (a : R) → R)
        1 :
      R)
    ((e : (a : R) → R) 1 : R)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
u : Rˣ
x : R
⊢ (((unitsEquivAut R : (a : Rˣ) → R ≃L[R] R) u : R ≃L[R] R) : (a : R) → R) x = x * (↑u : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
u : Rˣ
x : R
⊢ (ContinuousLinearEquiv.symm ((unitsEquivAut R : (a : Rˣ) → R ≃L[R] R) u) : (a : R) → R) x = x * (↑u⁻¹ : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
e : R ≃L[R] R
⊢ Eq (α := R) ((↑((Equiv.symm (unitsEquivAut R) : (a : R ≃L[R] R) → Rˣ) e) : R) : R) ((e : (a : R) → R) 1 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Unique ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
⊢ Eq (α := (a : ι → M) → M) (⇑(funUnique ι R M) : (a : ι → M) → M) (Function.eval (β := fun (x : ι) ↦ M) default)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Unique ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
⊢ Eq (α := (a : M) → ι → M) (⇑(ContinuousLinearEquiv.symm (funUnique ι R M)) : (a : M) → ι → M) (Function.const ι)

Tactic:
rfl

Premises used: Eq.mpr, uniqueElim, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
M₂ : Type u_3
inst_3 : TopologicalSpace M₂
inst_4 : AddCommGroup M₂
M₃ : Type u_4
inst_5 : TopologicalSpace M₃
inst_6 : AddCommGroup M₃
M₄ : Type u_5
inst_7 : TopologicalSpace M₄
inst_8 : AddCommGroup M₄
inst_9 : Module R M
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R M₄
inst_13 : IsTopologicalAddGroup M₄
e : M ≃L[R] M₂
e' : M₃ ≃L[R] M₄
f : M →L[R] M₄
x : M × M₃
⊢ Eq (α := M₂ × M₄) ((e.skewProd e' f : (a : M × M₃) → M₂ × M₄) x : M₂ × M₄)
    (((e : (a : M) → M₂) x.1,
        HAdd.hAdd (α := M₄) (β := M₄) ((e' : (a : M₃) → M₄) x.2 : M₄) ((f : (a : M) → M₄) x.1 : M₄)) :
      M₂ × M₄)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
M₂ : Type u_3
inst_3 : TopologicalSpace M₂
inst_4 : AddCommGroup M₂
M₃ : Type u_4
inst_5 : TopologicalSpace M₃
inst_6 : AddCommGroup M₃
M₄ : Type u_5
inst_7 : TopologicalSpace M₄
inst_8 : AddCommGroup M₄
inst_9 : Module R M
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R M₄
inst_13 : IsTopologicalAddGroup M₄
e : M ≃L[R] M₂
e' : M₃ ≃L[R] M₄
f : M →L[R] M₄
x : M₂ × M₄
⊢ Eq (α := M × M₃) (((e.skewProd e' f).symm : (a : M₂ × M₄) → M × M₃) x : M × M₃)
    (((e.symm : (a : M₂) → M) x.1,
        (e'.symm : (a : M₄) → M₃)
          (HSub.hSub (β := M₄) x.2 ((f : (a : M) → M₄) ((e.symm : (a : M₂) → M) x.1 : M) : M₄))) :
      M × M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : ContinuousNeg M
⊢ Eq.{u_2 + 1} (α := (a : M) → M) (⇑(neg R) : (a : M) → M) (-id)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : ContinuousNeg M
x : M
⊢ (neg R : (a : M) → M) x = -x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : ContinuousNeg M
⊢ Eq.{u_2 + 1} (α := M ≃L[R] M) (ContinuousLinearEquiv.symm (neg R)) (neg R)

Tactic:
rfl

Premises used: ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.neg, LinearEquiv.neg, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
R : Type u_1
inst : Ring R
R₂ : Type u_2
inst_1 : Ring R₂
M : Type u_3
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
M₂ : Type u_4
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_8 : RingHomInvPair σ₁₂ σ₂₁
inst_9 : RingHomInvPair σ₂₁ σ₁₂
e : M ≃SL[σ₁₂] M₂
x y : M
⊢ (e : (a : M) → M₂) (x - y) = HSub.hSub (α := M₂) (β := M₂) ((e : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) y : M₂)

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

Premises used: ContinuousLinearMap.map_sub, ContinuousLinearEquiv.toContinuousLinearMap