-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem congr {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'}
    [t : TopologicalSpace E] (hp : WithSeminorms p) (hpq : Seminorm.IsBounded p q LinearMap.id)
    (hqp : Seminorm.IsBounded q p LinearMap.id) : WithSeminorms q

Proof state:
case topology_eq_withSeminorms
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology

Tactic:
refine le_antisymm ?_ ?_ <;>
rw [← continuous_id_iff_le] <;>
refine continuous_from_bounded (.mk (topology := _) rfl) (.mk (topology := _) rfl)
  LinearMap.id (by assumption)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Seminorm.IsBounded q p LinearMap.id

Tactic:
assumption

Result:
no goals

Proof state:
case topology_eq_withSeminorms
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ t = q.moduleFilterBasis.topology

Tactic:
rw [hp.topology_eq_withSeminorms]

Result:
case topology_eq_withSeminorms
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ WithSeminorms q

Tactic:
constructor

Result:
case topology_eq_withSeminorms
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ t = q.moduleFilterBasis.topology

Proof state:
case topology_eq_withSeminorms
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
t : TopologicalSpace E
hp : WithSeminorms p
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology

Tactic:
clear hp t

Result:
case topology_eq_withSeminorms
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology = q.moduleFilterBasis.topology