-- Mathlib/Topology/Algebra/Module/ModuleTopology.lean
theorem iso (e : A ≃L[R] B) : IsModuleTopology R B where
  eq_moduleTopology'

Proof state:
case h.h.mpr.intro
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
h1 : ContinuousSMul R B
h2 : ContinuousAdd B
⊢ ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
use τ.induced e

Result:
case h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
h1 : ContinuousSMul R B
h2 : ContinuousAdd B
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e.toHomeomorph.symm) (TopologicalSpace.induced (⇑e) τ) = τ

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
⊢ τB = moduleTopology R B

Tactic:
let g' : B →ₗ[R] A := e.symm

Result:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
⊢ τB = moduleTopology R B

Proof state:
case h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
h1 : ContinuousSMul R B
h2 : ContinuousAdd B
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e.toHomeomorph.symm) (TopologicalSpace.induced (⇑e) τ) = τ

Tactic:
rw [induced_compose]

Result:
case h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
h1 : ContinuousSMul R B
h2 : ContinuousAdd B
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ

Proof state:
case h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
h1 : ContinuousSMul R B
h2 : ContinuousAdd B
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ

Tactic:
refine ⟨⟨continuousSMul_induced g.toMulActionHom, continuousAdd_induced h⟩, ?_⟩

Result:
case h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
h1 : ContinuousSMul R B
h2 : ContinuousAdd B
⊢ TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
⊢ τB = moduleTopology R B

Tactic:
let h' : B →+ A := e.symm

Result:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
⊢ τB = moduleTopology R B

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
⊢ τB = moduleTopology R B

Tactic:
simp_rw [e.toHomeomorph.symm.isInducing.1, eq_moduleTopology R A, moduleTopology, induced_sInf]

Result:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
⊢ sInf (TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A}) =
    sInf {t | ContinuousSMul R B ∧ ContinuousAdd B}

Proof state:
case h.h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
⊢ τ ∈ TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A} ↔
    τ ∈ {t | ContinuousSMul R B ∧ ContinuousAdd B}

Tactic:
rw [Set.mem_image]

Result:
case h.h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
⊢ (∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ) ↔
    τ ∈ {t | ContinuousSMul R B ∧ ContinuousAdd B}