awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
⊢ ∃ (N' : Set M), Minimal (fun (x : Set M) ↦ x ∈ S) N'
have refine : ∀ (c : Set (Set M)) (hcs : c ⊆ S) (hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c), ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s
Tactic: refine zorn_superset _ fun c hcs hc => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
⊢ ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s
have refine_1 : (⋂₀ c).Nonempty
Tactic: refine
    ⟨⋂₀ c, ⟨isClosed_sInter fun t ht => (hcs ht).1, ?_, fun m hm m' hm' => ?_⟩, fun s hs =>
      Set.sInter_subset_of_mem hs⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
refine_1 : (⋂₀ c).Nonempty
⊢ ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s
have refine_2 : ∀ (m : M) (hm : m ∈ ⋂₀ c) (m' : M) (hm' : m' ∈ ⋂₀ c), m * m' ∈ ⋂₀ c
Tactic: refine
    ⟨⋂₀ c, ⟨isClosed_sInter fun t ht => (hcs ht).1, ?_, fun m hm m' hm' => ?_⟩, fun s hs =>
      Set.sInter_subset_of_mem hs⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
⊢ (⋂₀ c).Nonempty
have refine_1 : ∀ (hcs : ∅ ⊆ S) (hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) ∅), Set.Nonempty.{u_1} (α := M) (⋂₀ ∅)
Tactic: obtain rfl | hcnemp := c.eq_empty_or_nonempty
Cleared hypotheses: c, hcs, hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
refine_1 : ∀ (hcs : ∅ ⊆ S) (hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) ∅), Set.Nonempty.{u_1} (α := M) (⋂₀ ∅)
⊢ (⋂₀ c).Nonempty
have refine_1₁ : ∀ (hcnemp : c.Nonempty), (⋂₀ c).Nonempty
Tactic: obtain rfl | hcnemp := c.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) ∅
⊢ Set.Nonempty.{u_1} (α := M) (⋂₀ ∅)
have refine_1 : Set.Nonempty.{u_1} (α := M) Set.univ
Tactic: rw [Set.sInter_empty]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ (⋂₀ c).Nonempty
have h : ⋂₀ c = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)
Tactic: convert!
      @IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
h : ⋂₀ c = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)
⊢ (⋂₀ c).Nonempty
have refine_1 : Directed (ι := (↑c : Type u_1)) (fun (x1 x2 : Set M) ↦ x1 ⊇ x2) (Subtype.val (p := fun (x : Set M) ↦ x ∈ c))
Tactic: convert!
      @IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
h : ⋂₀ c = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)
refine_1 : Directed (ι := (↑c : Type u_1)) (fun (x1 x2 : Set M) ↦ x1 ⊇ x2) (Subtype.val (p := fun (x : Set M) ↦ x ∈ c))
⊢ (⋂₀ c).Nonempty
have refine_1₁ : ∀ (i : (↑c : Type u_1)), (↑i : Set M).Nonempty
Tactic: convert!
      @IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
h : ⋂₀ c = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)
refine_1 : Directed (ι := (↑c : Type u_1)) (fun (x1 x2 : Set M) ↦ x1 ⊇ x2) (Subtype.val (p := fun (x : Set M) ↦ x ∈ c))
refine_1₁ : ∀ (i : (↑c : Type u_1)), (↑i : Set M).Nonempty
⊢ (⋂₀ c).Nonempty
have refine_1₂ : ∀ (i : (↑c : Type u_1)), IsCompact (↑i : Set M)
Tactic: convert!
      @IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
h : ⋂₀ c = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)
refine_1 : Directed (ι := (↑c : Type u_1)) (fun (x1 x2 : Set M) ↦ x1 ⊇ x2) (Subtype.val (p := fun (x : Set M) ↦ x ∈ c))
refine_1₁ : ∀ (i : (↑c : Type u_1)), (↑i : Set M).Nonempty
refine_1₂ : ∀ (i : (↑c : Type u_1)), IsCompact (↑i : Set M)
⊢ (⋂₀ c).Nonempty
have refine_1₃ : ∀ (i : (↑c : Type u_1)), IsClosed (↑i : Set M)
Tactic: convert!
      @IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (hypothesis)
Goal:
M : Type u_1
inst : Semigroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m : M // m ∈ s }
this : Semigroup M' := { mul := fun (p q : M') ↦ ⟨(↑p : M) * (↑q : M), ⋯⟩, mul_assoc := ⋯ }
⊢ ∃ m ∈ s, m * m = m
have this₁ : CompactSpace M'
Tactic: haveI : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (hypothesis)
Goal:
M : Type u_1
inst : Semigroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m : M // m ∈ s }
this_1 : Semigroup M' := { mul := fun (p q : M') ↦ ⟨(↑p : M) * (↑q : M), ⋯⟩, mul_assoc := ⋯ }
this : CompactSpace M'
⊢ ∃ m ∈ s, m * m = m
have this₁ : Nonempty M'
Tactic: haveI : Nonempty M' := nonempty_subtype.mpr snemp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (hypothesis)
Goal:
M : Type u_1
inst : Semigroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m : M // m ∈ s }
this_1 : Semigroup M' := { mul := fun (p q : M') ↦ ⟨(↑p : M) * (↑q : M), ⋯⟩, mul_assoc := ⋯ }
this_2 : CompactSpace M'
this : Nonempty M'
⊢ ∃ m ∈ s, m * m = m
have this₁ : ∀ (p : M'), Continuous (Y := M') fun (x : M') ↦ x * p
Tactic: have : ∀ p : M', Continuous (· * p) := fun p =>
    ((continuous_const_mul p.1).comp continuous_subtype_val).subtype_mk _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Semigroup (goal)
Goal:
M : Type u_1
inst : Semigroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m : M // m ∈ s }
this_1 : Semigroup M' := { mul := fun (p q : M') ↦ ⟨(↑p : M) * (↑q : M), ⋯⟩, mul_assoc := ⋯ }
this_2 : CompactSpace M'
this_3 : Nonempty M'
this : ∀ (p : M'), Continuous (Y := M') fun (x : M') ↦ x * p
⊢ ∃ m ∈ s, m * m = m
have obtain : ∀ (m : M) (hm : m ∈ s)
  (idem :
    Subtype.mk (p := fun (m : M) ↦ m ∈ s) m hm * Subtype.mk (p := fun (m : M) ↦ m ∈ s) m hm =
      Subtype.mk (p := fun (m : M) ↦ m ∈ s) m hm),
  ∃ m ∈ s, m * m = m
Tactic: obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Basic (goal)
Goal:
M : Type u_1
X : Type u_2
inst : SMul M X
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace X
inst_3 : ContinuousSMul M X
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : Prod.{u_1, u_2} M (SeparationQuotient X)) ↦ p.1 • p.2
have rw : Continuous[instTopologicalSpaceProd, _]
  ((fun (p : Prod.{u_1, u_2} M (SeparationQuotient X)) ↦ p.1 • p.2) ∘ Prod.map id mk)
Tactic: rw [(IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).isQuotientMap.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
⊢ UniformContinuous (β := SeparationQuotient G) fun (p : SeparationQuotient G × SeparationQuotient G) ↦ p.1 / p.2
have rw : UniformContinuous (β := SeparationQuotient G) fun (p : G × G) ↦
  HDiv.hDiv (α := SeparationQuotient G) (mk p.1, mk p.2).1 (mk p.1, mk p.2).2
Tactic: rw [uniformContinuous_dom₂]
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Section (goal)
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
⊢ ∃ (f : SeparationQuotient E →L[K] E), mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)
have rcases : ∀ (f : SeparationQuotient E →ₗ[K] E) (hf : (↑(mkCLM K E) : E →ₗ[K] SeparationQuotient E) ∘ₗ f = LinearMap.id),
  ∃ (f : SeparationQuotient E →L[K] E), mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)
Tactic: rcases (mkCLM K E).toLinearMap.exists_rightInverse_of_surjective
    (LinearMap.range_eq_top.mpr surjective_mk) with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Section (hypothesis)
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : (↑(mkCLM K E) : E →ₗ[K] SeparationQuotient E) ∘ₗ f = LinearMap.id
⊢ ∃ (f : SeparationQuotient E →L[K] E), mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)
have hf₁ : Eq (α := SeparationQuotient E → SeparationQuotient E) (mk ∘ (⇑f : (a : SeparationQuotient E) → E)) id
Tactic: replace hf : mk ∘ f = id := congr_arg DFunLike.coe hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Section (goal)
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
L : Type u_3
inst_6 : Semiring L
σ : L →+* K
F : Type u_4
inst_7 : AddCommMonoid F
inst_8 : Module L F
inst_9 : TopologicalSpace F
f : ContinuousLinearMap.{u_3, u_1, u_4, u_2} σ F (SeparationQuotient E)
⊢ ∃ (a : F →SL[σ] E), mkCLM K E ∘SL a = f
have h : mkCLM K E ∘SL outCLM K E ∘SL f = f
Tactic: use (outCLM K E).comp f
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Section (goal)
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
L : Type u_3
inst_6 : Semiring L
σ : L →+* K
F : Type u_4
inst_7 : AddCommMonoid F
inst_8 : Module L F
inst_9 : TopologicalSpace F
f : ContinuousLinearMap.{u_3, u_1, u_4, u_2} σ F (SeparationQuotient E)
⊢ mkCLM K E ∘SL outCLM K E ∘SL f = f
have h : (mkCLM K E ∘SL outCLM K E) ∘SL f = f
Tactic: rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Section (goal)
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
L : Type u_3
inst_6 : Semiring L
σ : L →+* K
F : Type u_4
inst_7 : AddCommMonoid F
inst_8 : Module L F
inst_9 : TopologicalSpace F
f : ContinuousLinearMap.{u_3, u_1, u_4, u_2} σ F (SeparationQuotient E)
h : (mkCLM K E ∘SL outCLM K E) ∘SL f = f
⊢ mkCLM K E ∘SL outCLM K E ∘SL f = f
have h₁ : ContinuousLinearMap.id K (SeparationQuotient E) ∘SL f = f
Tactic: rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Section (goal)
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
L : Type u_3
inst_6 : Semiring L
σ : L →+* K
F : Type u_4
inst_7 : AddCommMonoid F
inst_8 : Module L F
inst_9 : TopologicalSpace F
f : ContinuousLinearMap.{u_3, u_1, u_4, u_2} σ F (SeparationQuotient E)
h : (mkCLM K E ∘SL outCLM K E) ∘SL f = f
h₁ : ContinuousLinearMap.id K (SeparationQuotient E) ∘SL f = f
⊢ mkCLM K E ∘SL outCLM K E ∘SL f = f
have h₂ : f = f
Tactic: rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.SeparationQuotient.Section (goal)
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul K E
⊢ IsUniformInducing (α := SeparationQuotient E) (β := E)
    (⇑(outCLM K E : SeparationQuotient E →L[K] E) : (a : SeparationQuotient E) → E)
have rw : IsUniformInducing.{u_2, u_2} (α := SeparationQuotient E) id
Tactic: rw [← isUniformInducing_mk.of_comp_iff, mk_comp_outCLM]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
x : WithConv (E →L[R] F)
⊢ star (star x) = x
have h : ∀ (x_1 : E), Eq.{u_3 + 1} (α := F) (((star (star x)).ofConv : (a : E) → F) x_1 : F) ((x.ofConv : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
inst_14 : ContinuousAdd F
x y : WithConv (E →L[R] F)
⊢ star (x + y) = star x + star y
have h : ∀ (x_1 : E),
  Eq.{u_3 + 1} (α := F) (((star (x + y)).ofConv : (a : E) → F) x_1 : F)
    (((star x + star y).ofConv : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
G : Type u_4
inst_14 : AddCommMonoid G
inst_15 : Module R G
inst_16 : StarAddMonoid G
inst_17 : StarModule R G
inst_18 : TopologicalSpace G
inst_19 : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
⊢ star (toConv (f.ofConv ∘SL g.ofConv)) = toConv ((star f).ofConv ∘SL (star g).ofConv)
have h : ∀ (x : G),
  Eq.{u_3 + 1} (α := F) (((star (toConv (f.ofConv ∘SL g.ofConv))).ofConv : (a : G) → F) x : F)
    (((toConv ((star f).ofConv ∘SL (star g).ofConv)).ofConv : (a : G) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
G : Type u_4
inst_14 : AddCommMonoid G
inst_15 : Module R G
inst_16 : StarAddMonoid G
inst_17 : StarModule R G
inst_18 : TopologicalSpace G
inst_19 : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
⊢ star (toConv (f ∘SL g)) = toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)
have h : ∀ (x : G),
  Eq.{u_3 + 1} (α := F) (((star (toConv (f ∘SL g))).ofConv : (a : G) → F) x : F)
    (((toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)).ofConv : (a : G) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : TopologicalSpace E
inst_7 : ContinuousStar E
⊢ Eq (α := WithConv (E →L[R] E)) (star (toConv (ContinuousLinearMap.id R E))) (toConv (ContinuousLinearMap.id R E))
have h : ∀ (x : E),
  Eq (α := E) ((ofConv (star (toConv (ContinuousLinearMap.id R E))) : (a : E) → E) x : E)
    ((ofConv (toConv (ContinuousLinearMap.id R E)) : (a : E) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
⊢ Eq (α := WithConv (E →L[R] F)) (star (toConv 0)) (toConv 0)
have h : ∀ (x : E),
  Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv 0)) : (a : E) → F) x : F) ((ofConv (toConv 0) : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
E : Type u_2
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : TopologicalSpace E
inst_3 : ContinuousStar E
S : Type u_4
inst_4 : Semiring S
inst_5 : StarAddMonoid S
inst_6 : StarModule S S
inst_7 : Module S E
inst_8 : StarModule S E
inst_9 : TopologicalSpace S
inst_10 : ContinuousStar S
inst_11 : ContinuousSMul S E
a : E
⊢ Eq (α := WithConv (S →L[S] E)) (star (toConv (toSpanSingleton S a))) (toConv (toSpanSingleton S (star a)))
have h : Eq.{u_2 + 1} (α := E) ((ofConv (star (toConv (toSpanSingleton S a))) : (a : S) → E) 1 : E)
  ((ofConv (toConv (toSpanSingleton S (star a))) : (a : S) → E) 1 : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : AddCommMonoid F
inst_3 : StarAddMonoid F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
inst_6 : ContinuousStar E
inst_7 : ContinuousStar F
S : Type u_4
inst_8 : Semiring S
inst_9 : StarAddMonoid S
inst_10 : StarModule S S
inst_11 : Module S E
inst_12 : StarModule S E
inst_13 : TopologicalSpace S
inst_14 : ContinuousStar S
inst_15 : Module S F
inst_16 : StarModule S F
inst_17 : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
⊢ Eq (α := WithConv (E →L[S] F)) (star (toConv (f.ofConv.smulRight x))) (toConv ((star f).ofConv.smulRight (star x)))
have h : ∀ (x_1 : E),
  Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv (f.ofConv.smulRight x))) : (a : E) → F) x_1 : F)
    ((ofConv (toConv ((star f).ofConv.smulRight (star x))) : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
inst_14 : SMulCommClass R R F
inst_15 : ContinuousConstSMul R F
x : R
x_1 : WithConv (E →L[R] F)
⊢ star (x • x_1) = star x • star x_1
have h : ∀ (x_2 : E),
  Eq.{u_3 + 1} (α := F) (((star (x • x_1)).ofConv : (a : E) → F) x_2 : F)
    (((star x • star x_1).ofConv : (a : E) → F) x_2 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
⊢ f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)
have h : ∀ (u : R), u ∈ f ⁻¹' {(1, 1)} ↔ u ∈ (↑(unitary R) : Set R)
Tactic: ext u
-- Lean 4 proof step from Mathlib.Topology.Algebra.Star.Unitary (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
⊢ IsClosed (↑(unitary R) : Set R)
have hf : f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)
Tactic: have hf : f ⁻¹' {(1, 1)} = unitary R := by ext u; simp [f, Unitary.mem_iff]