awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Semigroup
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 = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)

Tactic:
exact Set.sInter_eq_iInter

Premises used: Set.sInter_eq_iInter
-- Module: Mathlib.Topology.Algebra.Semigroup
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
⊢ Directed (ι := (↑c : Type u_1)) (fun (x1 x2 : Set M) ↦ x1 ⊇ x2) (Subtype.val (p := fun (x : Set M) ↦ x ∈ c))

Tactic:
DirectedOn.directed_val (IsChain.directedOn hc.symm)

Premises used: IsChain.symm, IsChain.directedOn, DirectedOn.directed_val
-- Module: Mathlib.Topology.Algebra.Semigroup
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
⊢ Directed (ι := (↑c : Type u_1)) (fun (x1 x2 : Set M) ↦ x1 ⊇ x2) (Subtype.val (p := fun (x : Set M) ↦ x ∈ c))

Tactic:
refine DirectedOn.directed_val (IsChain.directedOn hc.symm)
-- Module: Mathlib.Topology.Algebra.Semigroup
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
⊢ ∀ (i : (↑c : Type u_1)), (↑i : Set M).Nonempty

Tactic:
fun i => (hcs i.prop).2.1

Premises used: And.right, And.left, Subtype.prop
-- Module: Mathlib.Topology.Algebra.Semigroup
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
⊢ ∀ (i : (↑c : Type u_1)), IsCompact (↑i : Set M)

Tactic:
fun i => (hcs i.prop).1.isCompact

Premises used: And.left, Subtype.prop, IsClosed.isCompact
-- Module: Mathlib.Topology.Algebra.Semigroup
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
⊢ ∀ (i : (↑c : Type u_1)), IsClosed (↑i : Set M)

Tactic:
fun i => (hcs i.prop).1

Premises used: And.left, Subtype.prop
-- Module: Mathlib.Topology.Algebra.Semigroup
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
⊢ ∀ (i : (↑c : Type u_1)), (↑i : Set M).Nonempty

Tactic:
exacts [fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1]

Premises used: And.right, And.left, IsClosed.isCompact
-- Module: Mathlib.Topology.Algebra.Semigroup
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
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ ∀ t ∈ c, m * m' ∈ t

Tactic:
fun t ht => (hcs ht).2.2 m (Set.mem_sInter.mp hm t ht) m' (Set.mem_sInter.mp hm' t ht)

Premises used: And.right, Set.mem_sInter, Iff.mp
-- Module: Mathlib.Topology.Algebra.Semigroup
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
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ ∀ t ∈ c, m * m' ∈ t

Tactic:
exact fun t ht => (hcs ht).2.2 m (Set.mem_sInter.mp hm t ht) m' (Set.mem_sInter.mp hm' t ht)

Premises used: And.right, Set.mem_sInter, Iff.mp
-- Module: Mathlib.Topology.Algebra.Semigroup
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 := ⋯ }
⊢ CompactSpace M'

Tactic:
haveI : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact
-- Module: Mathlib.Topology.Algebra.Semigroup
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'
⊢ Nonempty M'

Tactic:
haveI : Nonempty M' := nonempty_subtype.mpr snemp
-- Module: Mathlib.Topology.Algebra.Semigroup
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'
⊢ ∀ (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 _
-- Module: Mathlib.Topology.Algebra.Semigroup
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
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
⊢ ∃ m ∈ s, m * m = m

Tactic:
obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this

Premises used: exists_idempotent_of_compact_t2_of_continuous_mul_left
-- Module: Mathlib.Topology.Algebra.Semigroup
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 : 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:
⟨m, hm, Subtype.ext_iff.mp idem⟩

Premises used: Subtype.ext_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Algebra.Semigroup
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 : 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:
exact ⟨m, hm, Subtype.ext_iff.mp idem⟩
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : SMul M X
inst_2 : ContinuousConstSMul M X
c : M
x : X
⊢ mk (c • x) = HSMul.hSMul (β := SeparationQuotient X) c (mk x)

Tactic:
rfl

Premises used: SeparationQuotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : SMul M X
inst_2 : ContinuousConstSMul M X
N : Type u_3
inst_3 : SMul N X
inst_4 : ContinuousConstSMul N X
inst_5 : SMulCommClass M N X
⊢ SMulCommClass.{u_1, u_3, u_2} M N (SeparationQuotient X)

Tactic:
surjective_mk.smulCommClass mk_smul mk_smul

Premises used: SeparationQuotient.mk_smul, SeparationQuotient.surjective_mk, Function.Surjective.smulCommClass
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
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
rw :
  Continuous[instTopologicalSpaceProd, _]
    ((fun (p : Prod.{u_1, u_2} M (SeparationQuotient X)) ↦ p.1 • p.2) ∘ Prod.map id mk)
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : Prod.{u_1, u_2} M (SeparationQuotient X)) ↦ p.1 • p.2

Tactic:
rw [(IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).isQuotientMap.continuous_iff]

Premises used: IsOpenQuotientMap.prodMap, IsOpenQuotientMap.id, SeparationQuotient.isOpenQuotientMap_mk, Topology.IsQuotientMap.continuous_iff, IsOpenQuotientMap.isQuotientMap
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
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) ∘ Prod.map id mk)

Tactic:
continuous_mk.comp continuous_smul

Premises used: SeparationQuotient.continuous_mk, Continuous.comp, SeparationQuotient.mk, Quot.map, Quotient.map', ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
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) ∘ Prod.map id mk)

Tactic:
exact continuous_mk.comp continuous_smul

Premises used: SeparationQuotient.continuous_mk, Continuous.comp, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b : M
⊢ mk (a * b) = HMul.hMul (α := SeparationQuotient M) (mk a) (mk b)

Tactic:
rfl

Premises used: Quotient.map₂, SeparationQuotient.mk, rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
x : M
n : ℕ
⊢ mk (x ^ n) = HPow.hPow (α := SeparationQuotient M) (mk x) n

Tactic:
rfl

Premises used: SeparationQuotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
x : G
⊢ Eq (α := SeparationQuotient G) (mk x⁻¹) (mk x)⁻¹

Tactic:
rfl

Premises used: SeparationQuotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Div G
inst_2 : ContinuousDiv G
x y : G
⊢ mk (x / y) = HDiv.hDiv (α := SeparationQuotient G) (mk x) (mk y)

Tactic:
rfl

Premises used: Quotient.map₂, SeparationQuotient.mk, rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x : G
n : ℤ
⊢ mk (x ^ n) = HPow.hPow (α := SeparationQuotient G) (mk x) n

Tactic:
rfl

Premises used: SeparationQuotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
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
⊢ UniformContinuous (β := SeparationQuotient G) fun (p : SeparationQuotient G × SeparationQuotient G) ↦ p.1 / p.2

Tactic:
rw [uniformContinuous_dom₂]

Premises used: SeparationQuotient.uniformContinuous_dom₂
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
⊢ 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:
uniformContinuous_mk.comp uniformContinuous_div

Premises used: SeparationQuotient.uniformContinuous_mk, Quotient.map₂, UniformContinuous.comp, uniformContinuous_div, SeparationQuotient.mk
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
⊢ 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:
exact uniformContinuous_mk.comp uniformContinuous_div

Premises used: SeparationQuotient.uniformContinuous_mk, UniformContinuous.comp, uniformContinuous_div
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Mul R
inst_2 : Add R
inst_3 : LeftDistribClass R
inst_4 : ContinuousMul R
inst_5 : ContinuousAdd R
⊢ LeftDistribClass.{u_1} (SeparationQuotient R)

Tactic:
surjective_mk.leftDistribClass mk mk_add mk_mul

Premises used: Function.Surjective.leftDistribClass, SeparationQuotient.mk_mul, SeparationQuotient.mk_add, SeparationQuotient.surjective_mk, SeparationQuotient.mk
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Mul R
inst_2 : Add R
inst_3 : RightDistribClass R
inst_4 : ContinuousMul R
inst_5 : ContinuousAdd R
⊢ RightDistribClass.{u_1} (SeparationQuotient R)

Tactic:
surjective_mk.rightDistribClass mk mk_add mk_mul

Premises used: Function.Surjective.rightDistribClass, SeparationQuotient.mk_mul, SeparationQuotient.mk_add, SeparationQuotient.surjective_mk, SeparationQuotient.mk
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NatCast R
n : ℕ
⊢ Eq.{u_1 + 1} (α := SeparationQuotient R) (mk (↑n : R)) (↑n : SeparationQuotient R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NatCast R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := SeparationQuotient R) (mk (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: SeparationQuotient.mk, rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : IntCast R
n : ℤ
⊢ Eq.{u_1 + 1} (α := SeparationQuotient R) (mk (↑n : R)) (↑n : SeparationQuotient R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
inst_6 : Semiring S
inst_7 : AddCommMonoid N
inst_8 : Module S N
inst_9 : TopologicalSpace N
σ : R →+* S
f : M →SL[σ] N
hf : ∀ (x y : M), Inseparable x y → Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Continuous[_, inst_9] (lift (⇑f : (a : M) → N) hf)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
inst_5 : ContinuousConstSMul R M
inst_6 : Semiring S
inst_7 : AddCommMonoid N
inst_8 : Module S N
inst_9 : TopologicalSpace N
σ : R →+* S
f : M →SL[σ] N
hf : ∀ (x y : M), Inseparable x y → Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
x : M
⊢ Eq.{u_4 + 1} (α := N) ((liftCLM f hf : (a : SeparationQuotient M) → N) (mk x) : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: Quotient.liftOn', SeparationQuotient.lift, rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalSemiring A
inst_5 : ContinuousConstSMul R A
r : R
⊢ Eq.{u_2 + 1} (α := SeparationQuotient A) (mk ((algebraMap R A : (a : R) → A) r) : SeparationQuotient A)
    ((algebraMap R (SeparationQuotient A) : (a : R) → SeparationQuotient A) r : SeparationQuotient A)

Tactic:
rfl

Premises used: SeparationQuotient.mk, rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousConstSMul R M
⊢ Module.Finite.{u_1, u_2} R (SeparationQuotient M)

Tactic:
Module.Finite.of_surjective (mkCLM R M).toLinearMap Quotient.mk_surjective

Premises used: Module.Finite.of_surjective, SeparationQuotient.mkCLM, ContinuousLinearMap.toLinearMap, Quotient.mk_surjective
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Hom
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : CommMonoid M
inst_3 : ContinuousMul M
inst_4 : CommMonoid N
f : M →ₜ* N
hf : ∀ (x y : M), Inseparable x y → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
x : M
⊢ Eq.{u_2 + 1} (α := N) ((liftContinuousMonoidHom f hf : (a : SeparationQuotient M) → N) (mk x) : N)
    ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: Quotient.liftOn', SeparationQuotient.lift, rfl
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
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
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)
⊢ ∃ (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⟩

Premises used: Iff.mpr, SeparationQuotient.mkCLM, LinearMap.exists_rightInverse_of_surjective, ContinuousLinearMap.toLinearMap, LinearMap.range_eq_top, SeparationQuotient.surjective_mk
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
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
⊢ Eq (α := SeparationQuotient E → SeparationQuotient E) (mk ∘ (⇑f : (a : SeparationQuotient E) → E)) id

Tactic:
replace hf : mk ∘ f = id := congr_arg DFunLike.coe hf
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
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 : Eq (α := SeparationQuotient E → SeparationQuotient E) (mk ∘ (⇑f : (a : SeparationQuotient E) → E)) id
⊢ Continuous (Y := SeparationQuotient E) (mk ∘ f.toFun)

Tactic:
continuity
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
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 : Eq (α := SeparationQuotient E → SeparationQuotient E) (mk ∘ (⇑f : (a : SeparationQuotient E) → E)) id
⊢ ∃ (f : SeparationQuotient E →L[K] E), mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)

Tactic:
exact ⟨⟨f, isInducing_mk.continuous_iff.2 (by continuity)⟩, DFunLike.ext' hf⟩
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
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
⊢ Eq (α := SeparationQuotient E →L[K] SeparationQuotient E)
    (mkCLM K E ∘SL outCLM K E : SeparationQuotient E →L[K] SeparationQuotient E)
    (ContinuousLinearMap.id K (SeparationQuotient E) : SeparationQuotient E →L[K] SeparationQuotient E)

Tactic:
(exists_out_continuousLinearMap K E).choose_spec

Premises used: Exists.choose_spec, SeparationQuotient.exists_out_continuousLinearMap, SeparationQuotient.outCLM
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
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
x : SeparationQuotient E
⊢ mk (((outCLM K E : SeparationQuotient E →L[K] E) : (a : SeparationQuotient E) → E) x) = x

Tactic:
DFunLike.congr_fun (mkCLM_comp_outCLM K E) x

Premises used: SeparationQuotient.mkCLM_comp_outCLM, DFunLike.congr_fun, SeparationQuotient.mk
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
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
⊢ Eq (α := SeparationQuotient E → SeparationQuotient E)
    (mk ∘ (⇑(outCLM K E : SeparationQuotient E →L[K] E) : (a : SeparationQuotient E) → E)) id

Tactic:
funext (mk_outCLM K)

Premises used: SeparationQuotient.mk_outCLM, funext