mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f g : M₁ ≃SL[σ₁₂] M₂
h₁ : (↑↑f).toFun = (↑↑g).toFun
h₂ : (↑f).invFun = (↑g).invFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
⊢ Function.Injective toLinearEquiv

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
inst✝⁴ : Semiring R₁
M₁ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ f (x * 1) = g (x * 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁶ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁵ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹² : RingHomInvPair σ₁₃ σ₃₁
inst✝¹¹ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
⊢ ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e ∘ ⇑e.symm = id

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : 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₂ (f₁ x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : 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₁ (f₂ x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁵ : Semiring R₁
inst✝¹⁴ : Semiring R₂
inst✝¹³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹¹ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
e₁₂ : M₁ ≃SL[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →SL[σ₂₃] M₃
g : M₁ →SL[σ₁₃] M₃
⊢ f = g ∘SL ↑e₁₂.symm ↔ f ∘SL ↑e₁₂ = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁵ : Semiring R₁
inst✝¹⁴ : Semiring R₂
inst✝¹³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹¹ : RingHomInvPair σ₂₁ σ₁₂
σ₃₂ : R₃ →+* R₂
σ₃₁ : R₃ →+* R₁
inst✝¹⁰ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
e₁₂ : M₁ ≃SL[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →SL[σ₃₁] M₁
g : M₃ →SL[σ₃₂] M₂
⊢ f = ↑e₁₂.symm ∘SL g ↔ ↑e₁₂ ∘SL f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²⁸ : Semiring R₁
inst✝²⁷ : Semiring R₂
inst✝²⁶ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁴ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²³ : RingHomInvPair σ₂₃ σ₃₂
inst✝²² : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²¹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁰ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : AddCommMonoid M₁
M₂ : Type u_5
inst✝¹⁵ : TopologicalSpace M₂
inst✝¹⁴ : AddCommMonoid M₂
M₃ : Type u_6
inst✝¹³ : TopologicalSpace M₃
inst✝¹² : AddCommMonoid M₃
M₄ : Type u_7
inst✝¹¹ : TopologicalSpace M₄
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : Module R₁ M₁
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Module R₃ M₃
R₄ : Type u_8
inst✝⁶ : Semiring R₄
inst✝⁵ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝⁴ : RingHomInvPair σ₃₄ σ₄₃
inst✝³ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝² : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
f : M₁ →SL[σ₁₄] M₄
x : M₁
⊢ ((fun f ↦ ↑e₄₃.symm ∘SL f ∘SL ↑e₁₂) ((fun f ↦ ↑e₄₃ ∘SL f ∘SL ↑e₁₂.symm) f)) x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²⁸ : Semiring R₁
inst✝²⁷ : Semiring R₂
inst✝²⁶ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁴ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²³ : RingHomInvPair σ₂₃ σ₃₂
inst✝²² : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²¹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁰ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : AddCommMonoid M₁
M₂ : Type u_5
inst✝¹⁵ : TopologicalSpace M₂
inst✝¹⁴ : AddCommMonoid M₂
M₃ : Type u_6
inst✝¹³ : TopologicalSpace M₃
inst✝¹² : AddCommMonoid M₃
M₄ : Type u_7
inst✝¹¹ : TopologicalSpace M₄
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : Module R₁ M₁
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Module R₃ M₃
R₄ : Type u_8
inst✝⁶ : Semiring R₄
inst✝⁵ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝⁴ : RingHomInvPair σ₃₄ σ₄₃
inst✝³ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝² : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
f : M₂ →SL[σ₂₃] M₃
x : M₂
⊢ ((fun f ↦ ↑e₄₃ ∘SL f ∘SL ↑e₁₂.symm) ((fun f ↦ ↑e₄₃.symm ∘SL f ∘SL ↑e₁₂) f)) x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³⁴ : Semiring R₁
inst✝³³ : Semiring R₂
inst✝³² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²⁹ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁸ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝²³ : TopologicalSpace M₁
inst✝²² : AddCommMonoid M₁
M₂ : Type u_5
inst✝²¹ : TopologicalSpace M₂
inst✝²⁰ : AddCommMonoid M₂
M₃ : Type u_6
inst✝¹⁹ : TopologicalSpace M₃
inst✝¹⁸ : AddCommMonoid M₃
M₄ : Type u_7
inst✝¹⁷ : TopologicalSpace M₄
inst✝¹⁶ : AddCommMonoid M₄
inst✝¹⁵ : Module R₁ M₁
inst✝¹⁴ : Module R₂ M₂
inst✝¹³ : Module R₃ M₃
R₄ : Type u_8
inst✝¹² : Semiring R₄
inst✝¹¹ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝¹⁰ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁹ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝⁸ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁷ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝⁵ : SMulCommClass R₃ R₃ M₃
inst✝⁴ : SMulCommClass R₄ R₄ M₄
inst✝³ : ContinuousAdd M₃
inst✝² : ContinuousConstSMul R₃ M₃
inst✝¹ : ContinuousAdd M₄
inst✝ : 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:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝³⁴ : Semiring R₁
inst✝³³ : Semiring R₂
inst✝³² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²⁹ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁸ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝²³ : TopologicalSpace M₁
inst✝²² : AddCommMonoid M₁
M₂ : Type u_5
inst✝²¹ : TopologicalSpace M₂
inst✝²⁰ : AddCommMonoid M₂
M₃ : Type u_6
inst✝¹⁹ : TopologicalSpace M₃
inst✝¹⁸ : AddCommMonoid M₃
M₄ : Type u_7
inst✝¹⁷ : TopologicalSpace M₄
inst✝¹⁶ : AddCommMonoid M₄
inst✝¹⁵ : Module R₁ M₁
inst✝¹⁴ : Module R₂ M₂
inst✝¹³ : Module R₃ M₃
R₄ : Type u_8
inst✝¹² : Semiring R₄
inst✝¹¹ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝¹⁰ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁹ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝⁸ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁷ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝⁵ : SMulCommClass R₃ R₃ M₃
inst✝⁴ : SMulCommClass R₄ R₄ M₄
inst✝³ : ContinuousAdd M₃
inst✝² : ContinuousConstSMul R₃ M₃
inst✝¹ : ContinuousAdd M₄
inst✝ : ContinuousConstSMul R₄ M₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
⊢ ∀ (m : R₄) (x : M₁ →SL[σ₁₄] M₄), (e₁₂.arrowCongrEquiv e₄₃).toFun (m • x) = σ₄₃ m • (e₁₂.arrowCongrEquiv e₄₃).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
⊢ ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
⊢ ∀ (m : R) (x : M), ↑f (m • x) = (RingHom.id R) m • ↑f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : M ≃L[R] M
⊢ ↑f * ↑f.symm = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : M ≃L[R] M
⊢ ↑f.symm * ↑f = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
x y : (M →L[R] M)ˣ
⊢ ofUnit (x * y) = ofUnit x * ofUnit y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
u : Rˣ
x : R
⊢ (ContinuousLinearMap.smulRight 1 ↑u⁻¹) ((ContinuousLinearMap.smulRight 1 ↑u) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
u : Rˣ
x : R
⊢ (ContinuousLinearMap.smulRight 1 ↑u) ((ContinuousLinearMap.smulRight 1 ↑u⁻¹) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e 1 * e.symm 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e.symm 1 * e 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
u : Rˣ
⊢ ↑((fun e ↦ { val := e 1, inv := e.symm 1, val_inv := ⋯, inv_val := ⋯ })
        ((fun u ↦ equivOfInverse (ContinuousLinearMap.smulRight 1 ↑u) (ContinuousLinearMap.smulRight 1 ↑u⁻¹) ⋯ ⋯) u)) =
    ↑u

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ ((fun u ↦ equivOfInverse (ContinuousLinearMap.smulRight 1 ↑u) (ContinuousLinearMap.smulRight 1 ↑u⁻¹) ⋯ ⋯)
        ((fun e ↦ { val := e 1, inv := e.symm 1, val_inv := ⋯, inv_val := ⋯ }) e))
      1 =
    e 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : ContinuousNeg M
x : M
⊢ (neg R) x = -x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝¹¹ : Ring R
R₂ : Type u_2
inst✝¹⁰ : Ring R₂
M : Type u_3
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Module R M₂
inst✝ : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse ⇑f₂ ⇑f₁
x : M
⊢ (f₂.coprod (↑f₁).ker.subtypeL) ((f₁.prod (f₁.projKerOfRightInverse f₂ h)) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝¹¹ : Ring R
R₂ : Type u_2
inst✝¹⁰ : Ring R₂
M : Type u_3
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Module R M₂
inst✝ : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse ⇑f₂ ⇑f₁
x✝ : M₂ × ↥(↑f₁).ker
x : M₂
y : ↥(↑f₁).ker
⊢ (f₁.prod (f₁.projKerOfRightInverse f₂ h)) ((f₂.coprod (↑f₁).ker.subtypeL) (x, y)) = (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ (↑e).inverse = ↑e.symm

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ IsInvertible 0 ↔ Subsingleton M ∧ Subsingleton M₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ inverse 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
hf : f.IsInvertible
⊢ (g ∘SL f).IsInvertible

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
⊢ f.inverse = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
x : M
y : M₂
hf : f.IsInvertible
⊢ f.inverse y = x ↔ y = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : ↑A = ↑e ∘SL f
⊢ f = ↑e.symm ∘SL ↑e ∘SL f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ (↑e ∘SL f).IsInvertible ↔ f.IsInvertible

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : ↑A = f ∘SL ↑e
⊢ f = (f ∘SL ↑e) ∘SL ↑e.symm

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ Set.range ⇑(algebraMap R S)
⊢ (includeLeftSubRight R S) s = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Ring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
⊢ ↑(LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)) ∘ₗ
      LinearMap.lTensor T (includeLeftSubRight R S) =
    ↑R (includeLeftSubRight T (T ⊗[R] S))

Tactic:
by

Goal state after: