-- 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
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
⊢ τ ∈ {t | ContinuousSMul R B ∧ ContinuousAdd B} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
rintro ⟨h1, h2⟩

Result:
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 = τ

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
⊢ sInf (TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A}) =
    sInf {t | ContinuousSMul R B ∧ ContinuousAdd B}

Tactic:
apply congr_arg

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.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A} =
    {t | ContinuousSMul R B ∧ ContinuousAdd 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 ∘ ⇑e.toHomeomorph.symm) τ = TopologicalSpace.induced id τ

Tactic:
simp

Result:
no goals

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 ∘ ⇑e.toHomeomorph.symm) τ = τ

Tactic:
nth_rw 2 [← induced_id (t := τ)]

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) τ = TopologicalSpace.induced id τ

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
⊢ τB = moduleTopology R B

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

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
⊢ τB = moduleTopology R B

Proof state:
case h.h.mp
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}

Tactic:
rintro ⟨σ, ⟨hσ1, hσ2⟩, rfl⟩

Result:
case h.h.mp.intro.intro.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 A
hσ1 : ContinuousSMul R A
hσ2 : ContinuousAdd A
⊢ TopologicalSpace.induced (⇑e.toHomeomorph.symm) σ ∈ {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
⊢ (∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ) ↔
    τ ∈ {t | ContinuousSMul R B ∧ ContinuousAdd B}

Tactic:
constructor

Result:
case h.h.mp
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}

case h.h.mpr
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
⊢ τ ∈ {t | ContinuousSMul R B ∧ ContinuousAdd B} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ