awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
S : Set (Set α)
simp_rw : Eq.{u_3 + 1} (α := Set α) (closure[inst] (⋃ i ∈ S, i)) (⋃ s ∈ S, closure[inst] s)
⊢ closure[inst] (⋃₀ S) = ⋃ s ∈ S, closure[inst] s

Tactic:
simp_rw [sUnion_eq_biUnion, closure_iUnion]

Premises used: closure_iUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[inst_1] s
simp_rw : ∀ (hS : ∀ s ∈ S, ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = s), ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S
⊢ IsOpen[inst_1] (⋂₀ S)

Tactic:
simp_rw [h.isOpen_iff] at hS ⊢

Premises used: Topology.IsInducing.isOpen_iff
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
hS : ∀ s ∈ S, ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = s
choose :
  ∀ (U : (s : Set β) → s ∈ S → Set α) (hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a))
    (htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s), ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S
⊢ ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S

Tactic:
choose U hU htU using hS
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
⊢ ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S

Tactic:
⟨_, isOpen_iInter₂ hU, ?_⟩

Premises used: And.intro, Exists.intro, isOpen_iInter₂
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
refine : f ⁻¹' ⋂ (i : Set β), ⋂ (j : i ∈ S), U i j = ⋂₀ S
⊢ ∃ (t : Set α), IsOpen[inst] t ∧ f ⁻¹' t = ⋂₀ S

Tactic:
refine ⟨_, isOpen_iInter₂ hU, ?_⟩
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
f : β → α
h : IsInducing f
S : Set (Set β)
U : (s : Set β) → s ∈ S → Set α
hU : ∀ (s : Set β) (a : s ∈ S), IsOpen[inst] (U s a)
htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s
simp_rw : ⋂ (i : Set β), ⋂ (i_1 : i ∈ S), f ⁻¹' U i i_1 = ⋂₀ S
simp_rw₁ : ⋂ i ∈ S, i = ⋂₀ S
⊢ f ⁻¹' ⋂ (i : Set β), ⋂ (j : i ∈ S), U i j = ⋂₀ S

Tactic:
simp_rw [preimage_iInter, htU, sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter, Set.preimage_iInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
t₁ t₂ : TopologicalSpace α
h : AlexandrovDiscrete α
h_1 : AlexandrovDiscrete α
⊢ AlexandrovDiscrete α

Tactic:
@AlexandrovDiscrete.mk α (t₁ ⊔ t₂) fun _S hS ↦
    ⟨@isOpen_sInter _ t₁ _ _ fun _s hs ↦ (hS _ hs).1, isOpen_sInter fun _s hs ↦ (hS _ hs).2⟩

Premises used: isOpen_sInter, AlexandrovDiscrete.mk, And.right, And.left, And.intro
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
α : Type u_3
t : ι → TopologicalSpace α
h : ∀ (i : ι), AlexandrovDiscrete α
⊢ AlexandrovDiscrete α

Tactic:
@AlexandrovDiscrete.mk α (⨆ i, t i)
    fun _S hS ↦ isOpen_iSup_iff.2
      fun i ↦ @isOpen_sInter _ (t i) _ _
        fun _s hs ↦ isOpen_iSup_iff.1 (hS _ hs) _

Premises used: Iff.mpr, isOpen_sInter, AlexandrovDiscrete.mk, isOpen_iSup_iff, Iff.mp
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
rw : IsOpen[inst] (⋂₀ {t : Set α | IsOpen[inst] t ∧ s ⊆ t})
⊢ IsOpen[inst] (nhdsKer s)

Tactic:
rw [nhdsKer_def]

Premises used: nhdsKer_def
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst] (⋂₀ {t : Set α | IsOpen[inst] t ∧ s ⊆ t})

Tactic:
isOpen_sInter fun _ ↦ And.left

Premises used: isOpen_sInter, And.left
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst] (⋂₀ {t : Set α | IsOpen[inst] t ∧ s ⊆ t})

Tactic:
exact isOpen_sInter fun _ ↦ And.left

Premises used: isOpen_sInter, And.left
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ nhdsKer s ∈ 𝓝ˢ s

Tactic:
isOpen_nhdsKer.mem_nhdsSet.2 subset_nhdsKer

Premises used: Iff.mpr, subset_nhdsKer, isOpen_nhdsKer, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ nhdsKer s = s ↔ IsOpen[inst] s

Tactic:
⟨fun h ↦ h ▸ isOpen_nhdsKer, IsOpen.nhdsKer_eq⟩

Premises used: Eq.rec, IsOpen.nhdsKer_eq, Iff.intro, isOpen_nhdsKer
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ nhdsKer s ⊆ s ↔ IsOpen[inst] s

Tactic:
simp only [nhdsKer_eq_iff_isOpen.symm, Subset.antisymm_iff, subset_nhdsKer, and_true]

Premises used: and_true, subset_nhdsKer, Set.Subset.antisymm_iff, nhdsKer_eq_iff_isOpen, Iff.symm
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s t : Set α
⊢ nhdsKer s ⊆ t ↔ ∃ (U : Set α), IsOpen[inst] U ∧ s ⊆ U ∧ U ⊆ t

Tactic:
⟨fun h ↦ ⟨nhdsKer s, isOpen_nhdsKer, subset_nhdsKer, h⟩,
    fun ⟨_U, hU, hsU, hUt⟩ ↦ (nhdsKer_minimal hsU hU).trans hUt⟩

Premises used: _private.0.nhdsKer_subset_iff.match_1, subset_nhdsKer, HasSubset.Subset.trans, HasSubset.Subset, And.intro, Iff.intro, Exists.intro, isOpen_nhdsKer, nhdsKer, nhdsKer_minimal
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s t : Set α
⊢ nhdsKer s ⊆ t ↔ t ∈ 𝓝ˢ s

Tactic:
nhdsKer_subset_iff.trans mem_nhdsSet_iff_exists.symm

Premises used: mem_nhdsSet_iff_exists, nhdsKer_subset_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
t : Set α
a : α
⊢ nhdsKer {a} ⊆ t ↔ t ∈ 𝓝 a

Tactic:
simp [nhdsKer_subset_iff_mem_nhdsSet]

Premises used: nhdsKer_subset_iff_mem_nhdsSet
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s t : Set α
⊢ nhdsKer s ≤ t ↔ s ≤ interior t

Tactic:
simp [nhdsKer_subset_iff, subset_interior_iff]

Premises used: nhdsKer_subset_iff, subset_interior_iff
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
rw : 𝓟 (nhdsKer s) = 𝓝ˢ (nhdsKer s)
rw₁ rw₂ : 𝓟 (nhdsKer s) = 𝓟 (nhdsKer s)
⊢ 𝓟 (nhdsKer s) = 𝓝ˢ s

Tactic:
rw [← nhdsSet_nhdsKer, isOpen_nhdsKer.nhdsSet_eq]

Premises used: isOpen_nhdsKer, IsOpen.nhdsSet_eq, nhdsSet_nhdsKer
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
a : α
rw : 𝓝ˢ {a} = 𝓝 a
rw₁ rw₂ : 𝓝 a = 𝓝 a
⊢ 𝓟 (nhdsKer {a}) = 𝓝 a

Tactic:
rw [principal_nhdsKer, nhdsSet_singleton]

Premises used: principal_nhdsKer, nhdsSet_singleton
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ (𝓝ˢ s).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ nhdsKer s

Tactic:
principal_nhdsKer s ▸ hasBasis_principal (nhdsKer s)

Premises used: Eq.rec, nhdsKer, Filter.hasBasis_principal, principal_nhdsKer
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
a : α
⊢ (𝓝 a).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ nhdsKer {a}

Tactic:
principal_nhdsKer_singleton a ▸ hasBasis_principal (nhdsKer {a})

Premises used: principal_nhdsKer_singleton, Eq.rec, nhdsKer, Filter.hasBasis_principal, Singleton.singleton
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ IsOpen[inst] s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s

Tactic:
simp only [← nhdsKer_subset_iff_isOpen, Set.subset_def, mem_nhdsKer_iff_specializes, exists_imp,
    and_imp, @forall_comm (_ ⤳ _)]

Premises used: Set.subset_def, and_imp, mem_nhdsKer_iff_specializes, forall_comm, nhdsKer_subset_iff_isOpen, exists_imp
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
simp :
  ∀ (S : Set (Set α)),
    (∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s) → ∀ (a : α), (nhdsKer {a} ∩ ⋃₀ S).Nonempty → a ∈ ⋃₀ S
⊢ AlexandrovDiscrete α

Tactic:
simp only [alexandrovDiscrete_iff_isClosed, isClosed_iff_clusterPt, ClusterPt, funext hα,
      inf_principal, principal_neBot_iff]

Premises used: Filter.principal_neBot_iff, Filter.inf_principal, alexandrovDiscrete_iff_isClosed, funext, ClusterPt, isClosed_iff_clusterPt
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : (nhdsKer {a} ∩ ⋃₀ S).Nonempty
⊢ ∃ i ∈ S, (nhdsKer {a} ∩ i).Nonempty

Tactic:
rw [sUnion_eq_biUnion, inter_iUnion₂, nonempty_biUnion] at ha

Premises used: Set.nonempty_biUnion, Set.sUnion_eq_biUnion, Set.inter_iUnion₂
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : ∃ i ∈ S, (nhdsKer {a} ∩ i).Nonempty
obtain : ∀ (s : Set α) (hs : s ∈ S) (has : (nhdsKer {a} ∩ s).Nonempty), a ∈ ⋃₀ S
⊢ a ∈ ⋃₀ S

Tactic:
obtain ⟨s, hs, has⟩ := ha
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
s : Set α
hs : s ∈ S
has : (nhdsKer {a} ∩ s).Nonempty
⊢ a ∈ s

Tactic:
specialize hS s hs a has
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
a : α
s : Set α
hs : s ∈ S
has : (nhdsKer {a} ∩ s).Nonempty
hS : a ∈ s
⊢ a ∈ ⋃₀ S

Tactic:
mem_sUnion_of_mem hS hs

Premises used: Set.mem_sUnion_of_mem
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
a : α
s : Set α
hs : s ∈ S
has : (nhdsKer {a} ∩ s).Nonempty
hS : a ∈ s
⊢ a ∈ ⋃₀ S

Tactic:
exact mem_sUnion_of_mem hS hs

Premises used: Set.mem_sUnion_of_mem
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst] s
rw : IsOpen[inst] (⋂ t ∈ S, f ⁻¹' t)
⊢ IsOpen[coinduced f inst] (⋂₀ S)

Tactic:
rw [isOpen_coinduced, preimage_sInter]

Premises used: isOpen_coinduced, Set.preimage_sInter
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst] s
⊢ IsOpen[inst] (⋂ t ∈ S, f ⁻¹' t)

Tactic:
isOpen_iInter₂ hS

Premises used: isOpen_iInter₂
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst] s
⊢ IsOpen[inst] (⋂ t ∈ S, f ⁻¹' t)

Tactic:
exact isOpen_iInter₂ hS
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a_1 a : α
⊢ 𝓝 a = generate {nhdsKer {a}}

Tactic:
simp
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
p : α → Prop
⊢ AlexandrovDiscrete.{u_3} { a : α // p a }

Tactic:
IsInducing.subtypeVal.alexandrovDiscrete

Premises used: Set.Mem, Topology.IsInducing.alexandrovDiscrete, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s_1 t : Set α
a : α
s : Setoid α
⊢ AlexandrovDiscrete.{u_3} (Quotient s)

Tactic:
alexandrovDiscrete_coinduced

Premises used: alexandrovDiscrete_coinduced
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
⊢ AlexandrovDiscrete (α ⊕ β)

Tactic:
alexandrovDiscrete_coinduced.sup alexandrovDiscrete_coinduced

Premises used: alexandrovDiscrete_coinduced, AlexandrovDiscrete.sup
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι_1 : Sort u_1
κ : ι_1 → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
X : ι → Type u_6
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), AlexandrovDiscrete.{u_6} (X i)
⊢ AlexandrovDiscrete ((i : ι) × X i)

Tactic:
alexandrovDiscrete_iSup fun _ ↦ alexandrovDiscrete_coinduced

Premises used: alexandrovDiscrete_coinduced, alexandrovDiscrete_iSup
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
simp_rw : ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ : ∀ (a : α) (b : β), 𝓝 (a, b) = 𝓟 (nhdsKer {(a, b)})
simp_rw₂ : ∀ (a : α) (b : β), 𝓝 a ×ˢ 𝓝 b = 𝓟 (nhdsKer {(a, b)})
simp_rw₃ :
  ∀ (a : α) (b : β),
    SProd.sprod (α := Filter α) (β := Filter β) (𝓟 (nhdsKer {a})) (𝓟 (nhdsKer {b})) = 𝓟 (nhdsKer {(a, b)})
simp_rw₄ :
  ∀ (a : α) (b : β), 𝓟 (SProd.sprod (α := Set α) (β := Set β) (nhdsKer {a}) (nhdsKer {b})) = 𝓟 (nhdsKer {(a, b)})
simp_rw₅ : ∀ (a : α) (b : β), True
⊢ AlexandrovDiscrete (α × β)

Tactic:
simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]

Premises used: principal_nhdsKer_singleton, Filter.prod_principal_principal, nhdsKer_pair, Prod.forall, nhds_prod_eq, forall_true_iff, alexandrovDiscrete_iff_nhds
-- Module: Mathlib.Topology.AlexandrovDiscrete
Goal:
ι_1 : Sort u_1
κ : ι_1 → Sort u_2
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AlexandrovDiscrete α
inst_3 : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst_4 : Finite ι
X : ι → Type u_6
inst_5 : (i : ι) → TopologicalSpace (X i)
inst_6 : ∀ (i : ι), AlexandrovDiscrete.{u_6} (X i)
simp_rw : ∀ (a : (i : ι) → X i), 𝓝 a = 𝓟 (nhdsKer {a})
simp_rw₁ :
  ∀ (a : (i : ι) → X i), Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (a i)) (𝓟 (nhdsKer {a}))
simp_rw₂ :
  ∀ (a : (i : ι) → X i),
    Eq (α := Filter ((i : ι) → X i)) (Filter.pi (α := X) fun (i : ι) ↦ 𝓟 (nhdsKer {a i})) (𝓟 (nhdsKer {a}))
simp_rw₃ :
  ∀ (a : (i : ι) → X i),
    Eq (α := Filter ((i : ι) → X i)) (𝓟 (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {a i})) (𝓟 (nhdsKer {a}))
simp_rw₄ : ∀ (a : (i : ι) → X i), True
⊢ AlexandrovDiscrete ((i : ι) → X i)

Tactic:
simp_rw [alexandrovDiscrete_iff_nhds, nhds_pi, ← principal_nhdsKer_singleton,
    pi_principal, nhdsKer_singleton_pi, forall_true_iff]

Premises used: nhdsKer_singleton_pi, principal_nhdsKer_singleton, nhds_pi, forall_true_iff, alexandrovDiscrete_iff_nhds, Filter.pi_principal
-- Module: Mathlib.Topology.Algebra.Affine
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabit :
  ∀ (inhabited_h : Inhabited P),
    Continuous.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
      Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
⊢ Continuous.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)

Tactic:
inhabit P
-- Module: Mathlib.Topology.Algebra.Affine
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
h :
  ∀ (v : V),
    Eq.{u_4 + 1} (α := W) ((f.linear : (a : V) → W) v : W)
      (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
          (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
          (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
            (⇑(Homeomorph.vaddConst default) : (a : V) → P))
          v :
        W)
⊢ Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P)))

Tactic:
ext v
-- Module: Mathlib.Topology.Algebra.Affine
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
v : V
⊢ Eq.{u_4 + 1} (α := W) ((f.linear : (a : V) → W) v : W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
        (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
          (⇑(Homeomorph.vaddConst default) : (a : V) → P))
        v :
      W)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Affine
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
⊢ Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P)))

Tactic:
have :
    (f.linear : V → W) =
      (Homeomorph.vaddConst <| f default).symm ∘ f ∘ (Homeomorph.vaddConst default) := by
    ext v
    simp
-- Module: Mathlib.Topology.Algebra.Affine
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this :
  Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P)))
rw :
  Continuous.{u_2, u_4} (X := V) (Y := W)
      (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
        (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
          (⇑(Homeomorph.vaddConst default) : (a : V) → P))) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
⊢ Continuous.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.Affine
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this :
  Eq (α := (a : V) → W) (⇑f.linear : (a : V) → W)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
      (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
        (⇑(Homeomorph.vaddConst default) : (a : V) → P)))
⊢ Continuous.{u_2, u_4} (X := V) (Y := W)
      (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := Q)
        (⇑(Homeomorph.symm (Homeomorph.vaddConst ((f : (a : P) → Q) default)) : Q ≃ₜ W) : (a : Q) → W)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P) (⇑f : (a : P) → Q)
          (⇑(Homeomorph.vaddConst default) : (a : V) → P))) ↔
    Continuous.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)

Tactic:
simp only [Homeomorph.comp_continuous_iff, Homeomorph.comp_continuous_iff']

Premises used: Homeomorph.comp_continuous_iff', Homeomorph.comp_continuous_iff
-- Module: Mathlib.Topology.Algebra.Affine
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
inst_10 : Ring R
inst_11 : Module R V
inst_12 : Module R W
f : P →ᵃ[R] Q
inhabit :
  ∀ (inhabited_h : Inhabited P),
    IsOpenMap.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
      IsOpenMap.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)
⊢ IsOpenMap.{u_2, u_4} (X := V) (Y := W) (⇑f.linear : (a : V) → W) ↔
    IsOpenMap.{u_3, u_5} (X := P) (Y := Q) (⇑f : (a : P) → Q)

Tactic:
inhabit P