-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicClosure_idem (s : Set P) :
    intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
t : AffineSubspace 𝕜 P := affineSpan 𝕜 (intrinsicClosure 𝕜 s)
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Tactic:
clear_value t

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
t : AffineSubspace 𝕜 P
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
t : AffineSubspace 𝕜 P
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Tactic:
obtain rfl := ht.trans (affineSpan_intrinsicClosure _)

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 (intrinsicClosure 𝕜 s) = intrinsicClosure 𝕜 s

Tactic:
refine IsClosed.intrinsicClosure ?_

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (closure (Subtype.val ⁻¹' s))

Tactic:
exact isClosed_closure

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Tactic:
rw [intrinsicClosure, preimage_image_eq _ Subtype.coe_injective]

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (closure (Subtype.val ⁻¹' s))

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Tactic:
set t := affineSpan 𝕜 (intrinsicClosure 𝕜 s) with ht

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
t : AffineSubspace 𝕜 P := affineSpan 𝕜 (intrinsicClosure 𝕜 s)
ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)