awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
hL : L.filter ≤ atTop
⊢ ∅ ∉ L.filter

Tactic:
have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL : { filter := F : SummationFilter β }.filter ≤ atTop
hL' : ∅ ∉ { filter := F : SummationFilter β }.filter
mk : ∀ (hAtTop : True) (hL : F ≤ pure Finset.univ), { filter := F : SummationFilter β } = { filter := pure Finset.univ }
⊢ { filter := F : SummationFilter β } = unconditional β

Tactic:
simp only [unconditional, hAtTop] at *

Premises used: SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
mk : F = pure Finset.univ
⊢ { filter := F : SummationFilter β } = { filter := pure Finset.univ }

Tactic:
congr 1
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
⊢ F = pure Finset.univ

Tactic:
eq_of_le_of_ge hL (pure_le_iff.mpr ?_)

Premises used: Iff.mpr, eq_of_le_of_ge, Filter.pure_le_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
mk : ∀ s ∈ F, Finset.univ ∈ s
⊢ F = pure Finset.univ

Tactic:
refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)

Premises used: Iff.mpr, eq_of_le_of_ge, Filter.pure_le_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
mk : ∀ (hL' : ∃ s ∈ F, Finset.univ ∉ s), ∅ ∈ F
⊢ ∀ s ∈ F, Finset.univ ∈ s

Tactic:
contrapose! hL'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hAtTop : True
hL : F ≤ pure Finset.univ
hL' : ∃ s ∈ F, Finset.univ ∉ s
mk : ∀ (s : Set (Finset β)) (hs : s ∈ F) (hs' : Finset.univ ∉ s), ∅ ∈ F
⊢ ∅ ∈ F

Tactic:
obtain ⟨s, hs, hs'⟩ := hL'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hAtTop : True
hL : F ≤ pure Finset.univ
s : Set (Finset β)
hs : s ∈ F
hs' : Finset.univ ∉ s
⊢ ∅ ∈ F

Tactic:
simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

Premises used: Iff.mpr, Filter.le_pure_iff, Filter.inter_mem, Set.inter_singleton_eq_empty, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
hL : L.filter ≤ atTop
hL' : ∅ ∉ L.filter
mk :
  ∀ (F : Filter (Finset β)) [{ filter := F : SummationFilter β }.LeAtTop] [{ filter := F : SummationFilter β }.NeBot]
    (hL : { filter := F : SummationFilter β }.filter ≤ atTop) (hL' : ∅ ∉ { filter := F : SummationFilter β }.filter),
    { filter := F : SummationFilter β } = unconditional β
⊢ L = unconditional β

Tactic:
cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

Premises used: SummationFilter.mk, eq_of_le_of_ge, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
haveI haveI₁ haveI₂ : ∀ (this : Fintype β), L = unconditional β
haveI₃ :
  ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)), L = unconditional β
haveI₄ :
  ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ))
    (hL : L.filter ≤ atTop), L = unconditional β
haveI₅ :
  ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)) (hL : L.filter ≤ atTop)
    (hL' : ∅ ∉ L.filter), L = unconditional β
⊢ L = unconditional β

Tactic:
classical
  haveI := Fintype.ofFinite β
  have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
  have hL := L.le_atTop
  have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
  cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

Premises used: SummationFilter.mk, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder β
inst_1 : LocallyFiniteOrder β
⊢ (conditional β).support = univ

Tactic:
simpa [eq_univ_iff_forall, support, -eventually_and]
    using fun x ↦ prod_mem_prod (eventually_le_atBot x) (eventually_ge_atTop x)

Premises used: Filter.eventually_and, Set.eq_univ_iff_forall, Filter.prod_mem_prod, Filter.eventually_ge_atTop, Filter.eventually_le_atBot, SummationFilter.support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder β
inst_1 : LocallyFiniteOrder β
inst_2 : Nonempty β
inst_3 : IsDirectedOrder β
inst_4 : IsCodirectedOrder β
⊢ Filter.NeBot (α := Finset β)
    (Filter.map (fun (p : β × β) ↦ Finset.Icc p.1 p.2) (SProd.sprod (α := Filter β) (β := Filter β) atBot atTop))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder β
inst_1 : LocallyFiniteOrder β
inst_2 : IsCountablyGenerated.{u_2} (α := β) atTop
inst_3 : IsCountablyGenerated.{u_2} (α := β) atBot
⊢ (conditional β).filter.IsCountablyGenerated

Tactic:
map.isCountablyGenerated ..

Premises used: Filter.map, Filter.map.isCountablyGenerated
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_4
inst : PartialOrder γ
inst_1 : LocallyFiniteOrder γ
inst_2 : OrderBot γ
⊢ (conditional γ).filter = Filter.map Finset.Iic atTop

Tactic:
simp [isBot_bot.atBot_eq, comp_def, Finset.Icc_bot]

Premises used: Function.comp_def, IsBot.atBot_eq, Finset.Icc_bot, isBot_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
γ : Type u_4
inst : PartialOrder γ
inst_1 : LocallyFiniteOrder γ
inst_2 : OrderTop γ
⊢ (conditional γ).filter = Filter.map Finset.Ici atBot

Tactic:
simp [isTop_top.atTop_eq, comp_def, Finset.Icc_top]

Premises used: Finset.Icc_top, IsTop.atTop_eq, Function.comp_def, isTop_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
n : ℕ
h : ∀ (x : ℕ), x ∈ Finset.Iic n ↔ x ∈ Finset.range (n + 1)
⊢ Finset.Iic n = Finset.range (n + 1)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
n x : ℕ
⊢ x ∈ Finset.Iic n ↔ x ∈ Finset.range (n + 1)

Tactic:
simp [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
⊢ ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)

Tactic:
have (n : ℕ) : Finset.Iic n = Finset.range (n + 1) := by ext x; simp [Nat.lt_succ_iff]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
simp : Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop
⊢ (conditional ℕ).filter = Filter.map Finset.range atTop

Tactic:
simp only [conditional_filter_eq_map_Iic, funext this]

Premises used: funext, SummationFilter.conditional_filter_eq_map_Iic
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
a : Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop ≤ Filter.map Finset.range atTop
a₁ : Filter.map Finset.range atTop ≤ Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop
⊢ Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
a : ∀ (s : Set (Finset ℕ)), (∃ (a : ℕ), ∀ b ≥ a, Finset.range b ∈ s) → ∃ (a : ℕ), ∀ b ≥ a, Finset.range (b + 1) ∈ s
⊢ Tendsto (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop (Filter.map Finset.range atTop)

Tactic:
simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage]

Premises used: Filter.mem_atTop_sets, Filter.tendsto_atTop', Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
a : ∀ (s : Set (Finset ℕ)), (∃ (a : ℕ), ∀ b ≥ a, Finset.range (b + 1) ∈ s) → ∃ (a : ℕ), ∀ b ≥ a, Finset.range b ∈ s
⊢ Tendsto Finset.range atTop (Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop)

Tactic:
simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage]

Premises used: Filter.mem_atTop_sets, Filter.tendsto_atTop', Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ b ≥ a, Finset.range b ∈ s
b : ℕ
hb : b ≥ a + 1
⊢ b + 1 ≥ a

Tactic:
lia
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ b ≥ a, Finset.range b ∈ s
⊢ ∃ (a : ℕ), ∀ b ≥ a, Finset.range (b + 1) ∈ s

Tactic:
exact ⟨a + 1, fun b hb ↦ ha (b + 1) (by lia)⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ b ≥ a, Finset.range (b + 1) ∈ s
b : ℕ
hb : b ≥ a + 1
⊢ b - 1 ≥ a

Tactic:
lia
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ b ≥ a, Finset.range (b + 1) ∈ s
b : ℕ
hb : b ≥ a + 1
h : b = b - 1 + 1
⊢ Finset.range b ∈ s

Tactic:
convert! ha (b - 1) (by lia)

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ b ≥ a, Finset.range (b + 1) ∈ s
b : ℕ
hb : b ≥ a + 1
⊢ b = b - 1 + 1

Tactic:
lia
-- Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ b ≥ a, Finset.range (b + 1) ∈ s
⊢ ∃ (a : ℕ), ∀ b ≥ a, Finset.range b ∈ s

Tactic:
exact ⟨a + 1, fun b hb ↦ by convert! ha (b - 1) (by lia); lia⟩
-- Module: Mathlib.Topology.Algebra.Module.Determinant
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : Module R M
inst_5 : Module.Free R M
inst_6 : Module.Finite R M
f : ι → M →L[R] M
⊢ Eq.{u_2 + 1} (α := R)
    (det (M := (i : ι) → M) (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘SL proj (φ := fun (i : ι) ↦ M) i))
    (∏ i : ι, (f i).det)

Tactic:
LinearMap.det_pi _

Premises used: LinearMap.det_pi, LinearMap.pi
-- Module: Mathlib.Topology.Algebra.Module.Determinant
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousMul 𝕜
f : 𝕜 →L[𝕜] 𝕜
v : 𝕜
⊢ det (M := 𝕜) (f.smulRight v) = HMul.hMul (α := 𝕜) ((f : (a : 𝕜) → 𝕜) 1 : 𝕜) v

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Determinant
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousMul 𝕜
v : 𝕜
rw : HMul.hMul (α := 𝕜) ((ContinuousLinearMap.id 𝕜 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜) v = v
⊢ det (M := 𝕜) (toSpanSingleton 𝕜 v) = v

Tactic:
rw [← smulRight_id, det_smulRight]

Premises used: ContinuousLinearMap.det_smulRight, ContinuousLinearMap.smulRight_id
-- Module: Mathlib.Topology.Algebra.Module.Determinant
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousMul 𝕜
v : 𝕜
⊢ HMul.hMul (α := 𝕜) ((ContinuousLinearMap.id 𝕜 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜) v = v

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Determinant
Goal:
R : Type u_1
inst : Field R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
A : M ≃L[R] M
⊢ (↑A.symm : M →L[R] M).det = (↑A : M →L[R] M).det⁻¹

Tactic:
LinearEquiv.det_coe_symm A.toLinearEquiv

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.det_coe_symm
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
⊢ IsModuleTopology 𝕜 E

Tactic:
haveI : IsModuleTopology 𝕜 E := isModuleTopologyOfFiniteDimensional
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
this : IsModuleTopology 𝕜 E
⊢ IsModuleTopology 𝕜 (E →L[𝕜] 𝕜)

Tactic:
haveI : IsModuleTopology 𝕜 (E →L[𝕜] 𝕜) := isModuleTopologyOfFiniteDimensional
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
this_1 : IsModuleTopology 𝕜 E
this : IsModuleTopology 𝕜 (E →L[𝕜] 𝕜)
⊢ Continuous (Y := 𝕜) fun (x : (E →L[𝕜] 𝕜) × E) ↦
    match (motive := (E →L[𝕜] 𝕜) × E → 𝕜) x with
    | (x, y) => (((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) x : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) y

Tactic:
IsModuleTopology.continuous_bilinear_of_finite_left (topDualPairing 𝕜 E)

Premises used: IsModuleTopology.continuous_bilinear_of_finite_left, topDualPairing
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
this_1 : IsModuleTopology 𝕜 E
this : IsModuleTopology 𝕜 (E →L[𝕜] 𝕜)
⊢ Continuous (Y := 𝕜) fun (x : (E →L[𝕜] 𝕜) × E) ↦
    match (motive := (E →L[𝕜] 𝕜) × E → 𝕜) x with
    | (x, y) => (((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) x : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) y

Tactic:
exact IsModuleTopology.continuous_bilinear_of_finite_left (topDualPairing 𝕜 E)

Premises used: IsModuleTopology.continuous_bilinear_of_finite_left, topDualPairing
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
⊢ Function.Bijective (β := (E →L[𝕜] 𝕜) →L[𝕜] 𝕜) fun (y : E) ↦
    { toLinearMap := (LinearMap.flip (topDualPairing 𝕜 E) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜) y, cont := ⋯ }

Tactic:
LinearMap.toContinuousLinearMap.bijective.comp ?_

Premises used: LinearEquiv.bijective, Function.Bijective.comp, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
refine :
  Function.Bijective (α := E) (β := (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
    (⇑(LinearMap.flip (topDualPairing 𝕜 E)) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
⊢ Function.Bijective (β := (E →L[𝕜] 𝕜) →L[𝕜] 𝕜) fun (y : E) ↦
    { toLinearMap := (LinearMap.flip (topDualPairing 𝕜 E) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜) y, cont := ⋯ }

Tactic:
refine LinearMap.toContinuousLinearMap.bijective.comp ?_

Premises used: LinearEquiv.bijective, Function.Bijective.comp, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
rw : Function.Bijective (α := E →L[𝕜] 𝕜) (β := E →ₗ[𝕜] 𝕜) (⇑(topDualPairing 𝕜 E) : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜)
⊢ Function.Bijective (α := E) (β := (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
    (⇑(LinearMap.flip (topDualPairing 𝕜 E)) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)

Tactic:
rw [LinearMap.flip_bijective_iff₁]

Premises used: LinearMap.flip_bijective_iff₁
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
⊢ Function.Bijective (α := E →L[𝕜] 𝕜) (β := E →ₗ[𝕜] 𝕜) (⇑(topDualPairing 𝕜 E) : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜)

Tactic:
LinearMap.toContinuousLinearMap.symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.Module.TopDualPairing
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
⊢ Function.Bijective (α := E →L[𝕜] 𝕜) (β := E →ₗ[𝕜] 𝕜) (⇑(topDualPairing 𝕜 E) : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜)

Tactic:
exact LinearMap.toContinuousLinearMap.symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsTopologicalSemiring A
s : NonUnitalSubalgebra R A
⊢ IsTopologicalSemiring.{u_2} ↥s

Tactic:
s.toNonUnitalSubsemiring.instIsTopologicalSemiring

Premises used: Set.Mem, NonUnitalSubalgebra.toNonUnitalSubsemiring, NonUnitalSubsemiring.instIsTopologicalSemiring
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
s : NonUnitalSubalgebra R A
⊢ IsSemitopologicalSemiring.{u_2} ↥s

Tactic:
s.toNonUnitalSubsemiring.instIsSemitopologicalSemiring

Premises used: Set.Mem, NonUnitalSubsemiring.instIsSemitopologicalSemiring, NonUnitalSubalgebra.toNonUnitalSubsemiring
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
s : NonUnitalSubalgebra R A
⊢ s ≤ s.topologicalClosure

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
s : NonUnitalSubalgebra R A
⊢ IsClosed (↑s.topologicalClosure : Set A)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
s t : NonUnitalSubalgebra R A
h : s ≤ t
ht : IsClosed (↑t : Set A)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
s t : NonUnitalSubalgebra R A
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
inst_6 : TopologicalSpace B
inst_7 : NonUnitalSemiring B
inst_8 : Module R B
inst_9 : IsTopologicalSemiring B
inst_10 : ContinuousConstSMul R B
s : NonUnitalSubalgebra R A
φ : A →ₙₐ[R] B
hφ : Continuous.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
⊢ LE.le.{u_3} (α := NonUnitalSubalgebra R B) (map φ s.topologicalClosure) (topologicalClosure (map φ s))

Tactic:
image_closure_subset_closure_image hφ

Premises used: Set.Mem, setOf, Set.Subset, closure, image_closure_subset_closure_image, Set.image, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : ContinuousConstSMul R A
inst_5 : IsSemitopologicalSemiring A
inst_6 : TopologicalSpace B
inst_7 : NonUnitalSemiring B
inst_8 : Module R B
inst_9 : IsTopologicalSemiring B
inst_10 : ContinuousConstSMul R B
s : NonUnitalSubalgebra R A
φ : A →ₙₐ[R] B
hφ : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
⊢ LE.le.{u_3} (α := NonUnitalSubalgebra R B) (topologicalClosure (map φ s)) (map φ s.topologicalClosure)

Tactic:
hφ.closure_image_subset _

Premises used: IsClosedMap.closure_image_subset, Set.Mem, setOf, Set.Subset, closure, Set.image, Set.sInter