awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨆ (x : ℕ), f (x + k)))

Tactic:
exact tendsto_atTop_ciSup h_mon h_bdd

Premises used: tendsto_atTop_ciSup
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))

Tactic:
rw [← range_add_eq_image_Ici] at h_bdd

Premises used: Set.range_add_eq_image_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Antitone (β := ℝ) fun (n : ℕ) ↦ f (n + k)

Tactic:
rw [Ici, ← antitone_add_nat_iff_antitoneOn_nat_Ici] at h_ant

Premises used: Set.Ici, antitone_add_nat_iff_antitoneOn_nat_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
h_ant₁ : Antitone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
⊢ BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))

Tactic:
rw [Ici, ← antitone_add_nat_iff_antitoneOn_nat_Ici] at h_ant

Premises used: Set.Ici, antitone_add_nat_iff_antitoneOn_nat_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨅ (x : ℕ), f (x + k)))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))

Tactic:
rw [← tendsto_add_atTop_iff_nat k, ← range_add_eq_image_Ici, sInf_range]

Premises used: Set.range_add_eq_image_Ici, Filter.tendsto_add_atTop_iff_nat, sInf_range
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨅ (x : ℕ), f (x + k)))

Tactic:
tendsto_atTop_ciInf h_ant h_bdd

Premises used: tendsto_atTop_ciInf
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨅ (x : ℕ), f (x + k)))

Tactic:
exact tendsto_atTop_ciInf h_ant h_bdd

Premises used: tendsto_atTop_ciInf
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
rw : IsLUB (range f) (⨆ (i : ι), f i)
⊢ IsLUB (range f) x

Tactic:
rw [tendsto_nhds_unique h_tto (tendsto_atTop_ciSup h_mon h_bdd)]

Premises used: tendsto_atTop_ciSup, tendsto_nhds_unique
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) (⨆ (i : ι), f i)

Tactic:
isLUB_ciSup h_bdd

Premises used: isLUB_ciSup
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) (⨆ (i : ι), f i)

Tactic:
exact isLUB_ciSup h_bdd

Premises used: isLUB_ciSup
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
rw : IsGLB (range f) (⨅ (i : ι), f i)
⊢ IsGLB (range f) x

Tactic:
rw [tendsto_nhds_unique h_tto (tendsto_atTop_ciInf h_ant h_bdd)]

Premises used: tendsto_atTop_ciInf, tendsto_nhds_unique
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) (⨅ (i : ι), f i)

Tactic:
isGLB_ciInf h_bdd

Premises used: isGLB_ciInf
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) (⨅ (i : ι), f i)

Tactic:
exact isGLB_ciInf h_bdd

Premises used: isGLB_ciInf
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
rw : IsLUB (f '' Ici k) (sSup (f '' Ici k))
⊢ IsLUB (f '' Ici k) x

Tactic:
rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici h_mon h_bdd)]

Premises used: Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici, tendsto_nhds_unique
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) (sSup (f '' Ici k))

Tactic:
isLUB_csSup (image_nonempty.mpr nonempty_Ici) h_bdd

Premises used: Iff.mpr, Set.image_nonempty, isLUB_csSup, Set.nonempty_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) (sSup (f '' Ici k))

Tactic:
exact isLUB_csSup (image_nonempty.mpr nonempty_Ici) h_bdd

Premises used: Iff.mpr, Set.image_nonempty, isLUB_csSup, Set.nonempty_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
rw : IsGLB (f '' Ici k) (sInf (f '' Ici k))
⊢ IsGLB (f '' Ici k) x

Tactic:
rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici h_ant h_bdd)]

Premises used: tendsto_nhds_unique, Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) (sInf (f '' Ici k))

Tactic:
isGLB_csInf (image_nonempty.mpr nonempty_Ici) h_bdd

Premises used: Iff.mpr, Set.image_nonempty, isGLB_csInf, Set.nonempty_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) (sInf (f '' Ici k))

Tactic:
exact isGLB_csInf (image_nonempty.mpr nonempty_Ici) h_bdd

Premises used: Iff.mpr, Set.image_nonempty, isGLB_csInf, Set.nonempty_Ici
-- Module: Mathlib.Topology.Instances.RealVectorSpace
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
F : Type u_2
inst_4 : AddCommGroup F
inst_5 : Module ℝ F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul ℝ F
inst_8 : T2Space F
G : Type u_3
inst_9 : FunLike G E F
inst_10 : AddMonoidHomClass G E F
f : G
hf : Continuous.{u_1, u_2} (X := E) (Y := F) (⇑f : (a : E) → F)
c : ℝ
x : E
⊢ Continuous.{0, u_2} (Y := F) fun (c : ℝ) ↦ (f : (a : E) → F) (c • x)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.RealVectorSpace
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
F : Type u_2
inst_4 : AddCommGroup F
inst_5 : Module ℝ F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul ℝ F
inst_8 : T2Space F
f : E →+ F
hf : Continuous.{u_1, u_2} (X := E) (Y := F) (⇑f : (a : E) → F)
⊢ Eq (α := (a : E) → F) (⇑(f.toRealLinearMap hf) : (a : E) → F) (⇑f : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Instances.RealVectorSpace
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
F : Type u_2
inst_4 : AddCommGroup F
inst_5 : Module ℝ F
inst_6 : TopologicalSpace F
inst_7 : ContinuousSMul ℝ F
inst_8 : T2Space F
inst_9 : T2Space E
A : Type u_3
inst_10 : TopologicalSpace A
inst_11 : Ring A
inst_12 : Algebra ℝ A
inst_13 : Module A E
inst_14 : ContinuousSMul ℝ A
inst_15 : ContinuousSMul A E
⊢ IsScalarTower ℝ A E

Tactic:
⟨fun r x y => map_real_smul ((smulAddHom A E).flip y) (continuous_id.smul continuous_const) r x⟩

Premises used: continuous_const, map_real_smul, Continuous.smul, AddMonoidHom.flip, continuous_id, smulAddHom, IsScalarTower.mk, DFunLike.coe
-- Module: Mathlib.Topology.Instances.Sign
Goal:
⊢ DiscreteTopology SignType

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : 0 < a
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
(continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr ?_

Premises used: ContinuousAt.congr, continuousAt_const
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : 0 < a
refine : (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ 1) (⇑SignType.sign : (a : α) → SignType)
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
refine (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr ?_

Premises used: ContinuousAt.congr, continuousAt_const
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : 0 < a
rw :
  ∃ (t : Set α),
    (∀ y ∈ t, Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t
⊢ (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ 1) (⇑SignType.sign : (a : α) → SignType)

Tactic:
rw [Filter.EventuallyEq, eventually_nhds_iff]

Premises used: Filter.EventuallyEq, eventually_nhds_iff
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : 0 < a
⊢ ∃ (t : Set α),
    (∀ y ∈ t, Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t

Tactic:
⟨{ x | 0 < x }, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩

Premises used: setOf, sign_pos, And.intro, LT.lt, Exists.intro, isOpen_lt', OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : 0 < a
⊢ ∃ (t : Set α),
    (∀ y ∈ t, Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t

Tactic:
exact ⟨{ x | 0 < x }, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : a < 0
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
(continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr ?_

Premises used: ContinuousAt.congr, continuousAt_const
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : a < 0
refine : (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ -1) (⇑SignType.sign : (a : α) → SignType)
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
refine (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr ?_

Premises used: ContinuousAt.congr, continuousAt_const
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : a < 0
rw :
  ∃ (t : Set α),
    (∀ y ∈ t, Eq (α := SignType) (-1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t
⊢ (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ -1) (⇑SignType.sign : (a : α) → SignType)

Tactic:
rw [Filter.EventuallyEq, eventually_nhds_iff]

Premises used: Filter.EventuallyEq, eventually_nhds_iff
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : a < 0
⊢ ∃ (t : Set α),
    (∀ y ∈ t, Eq (α := SignType) (-1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t

Tactic:
⟨{ x | x < 0 }, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩

Premises used: setOf, isOpen_gt', sign_neg, And.intro, LT.lt, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : a < 0
⊢ ∃ (t : Set α),
    (∀ y ∈ t, Eq (α := SignType) (-1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t

Tactic:
exact ⟨{ x | x < 0 }, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
h : a ≠ 0
inl : ∀ (h_neg : a < 0), ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
inr : ∀ (h_pos : 0 < a), ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
rcases h.lt_or_gt with (h_neg | h_pos)

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
continuousAt_sign_of_neg h_neg

Premises used: continuousAt_sign_of_neg
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
exact continuousAt_sign_of_neg h_neg

Premises used: continuousAt_sign_of_neg
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
continuousAt_sign_of_pos h_pos

Premises used: continuousAt_sign_of_pos
-- Module: Mathlib.Topology.Instances.Sign
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a

Tactic:
exact continuousAt_sign_of_pos h_pos

Premises used: continuousAt_sign_of_pos
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : T2Space R
inst_3 : T2Space M
⊢ T2Space (tsze R M)

Tactic:
Prod.t2Space

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, TrivSqZeroExt.fst, Prod.t2Space
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
x : tsze R M
⊢ 𝓝 x = 𝓝 x.fst ×ˢ 𝓝 x.snd

Tactic:
nhds_prod_eq

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, Set.Mem, setOf, TrivSqZeroExt.fst, nhds_prod_eq
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Zero M
x : R
⊢ 𝓝 (inl x) = SProd.sprod (β := Filter M) (𝓝 x) (𝓝 0)

Tactic:
nhds_def _

Premises used: TrivSqZeroExt.nhds_def, TrivSqZeroExt.snd, Set.Mem, setOf, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Zero R
m : M
⊢ 𝓝 (inr m) = SProd.sprod (α := Filter R) (𝓝 0) (𝓝 m)

Tactic:
nhds_def _

Premises used: TrivSqZeroExt.nhds_def, TrivSqZeroExt.snd, Set.Mem, setOf, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
⊢ Continuous[instTopologicalSpace, inst] fst

Tactic:
continuous_fst

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, continuous_fst, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
⊢ Continuous[instTopologicalSpace, inst_1] snd

Tactic:
continuous_snd

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, continuous_snd, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Zero M
⊢ Continuous[inst, instTopologicalSpace] inl

Tactic:
continuous_id.prodMk continuous_const

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, continuous_const, setOf, TrivSqZeroExt.inl, TrivSqZeroExt.fst, continuous_id, Continuous.prodMk
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Zero R
⊢ Continuous[inst_1, instTopologicalSpace] inr

Tactic:
continuous_const.prodMk continuous_id

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt.inr, TrivSqZeroExt, continuous_const, setOf, TrivSqZeroExt.fst, continuous_id, Continuous.prodMk
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Zero M
⊢ IsEmbedding (X := R) (Y := tsze R M) TrivSqZeroExt.inl

Tactic:
.of_comp continuous_inl continuous_fst .id

Premises used: Topology.IsEmbedding.id, TrivSqZeroExt.continuous_inl, Topology.IsEmbedding.of_comp, TrivSqZeroExt.continuous_fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Zero R
⊢ IsEmbedding (X := M) (Y := tsze R M) TrivSqZeroExt.inr

Tactic:
.of_comp continuous_inr continuous_snd .id

Premises used: TrivSqZeroExt.continuous_snd, Topology.IsEmbedding.id, TrivSqZeroExt.continuous_inr, Topology.IsEmbedding.of_comp
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Add R
inst_3 : Add M
inst_4 : ContinuousAdd R
inst_5 : ContinuousAdd M
⊢ ContinuousAdd (tsze R M)

Tactic:
Prod.continuousAdd

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, TrivSqZeroExt.fst, Prod.continuousAdd
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Mul R
inst_3 : Add M
inst_4 : SMul R M
inst_5 : SMul.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
inst_8 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
inst_9 : ContinuousAdd M
⊢ ContinuousMul (tsze R M)

Tactic:
⟨((continuous_fst.comp continuous_fst).mul (continuous_fst.comp continuous_snd)).prodMk <|
      ((continuous_fst.comp continuous_fst).smul (continuous_snd.comp continuous_snd)).add
        ((MulOpposite.continuous_op.comp <| continuous_fst.comp <| continuous_snd).smul
          (continuous_snd.comp continuous_fst))⟩

Premises used: TrivSqZeroExt.continuous_snd, Continuous.comp, ContinuousMul.mk, Continuous.mul, Continuous.smul, TrivSqZeroExt.continuous_fst, Continuous.add, MulOpposite.continuous_op, Continuous.prodMk
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Neg R
inst_3 : Neg M
inst_4 : ContinuousNeg R
inst_5 : ContinuousNeg M
⊢ ContinuousNeg (tsze R M)

Tactic:
Prod.continuousNeg

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, TrivSqZeroExt.fst, Prod.continuousNeg
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_6 : IsTopologicalSemiring R
inst_7 : ContinuousAdd M
inst_8 : ContinuousSMul R M
inst_9 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
⊢ IsTopologicalSemiring (tsze R M)

Tactic:

Premises used: IsTopologicalSemiring.mk
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : ContinuousConstSMul S R
inst_5 : ContinuousConstSMul S M
⊢ ContinuousConstSMul S (tsze R M)

Tactic:
Prod.continuousConstSMul

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, Prod.continuousConstSMul, TrivSqZeroExt.fst
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace S
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : ContinuousSMul S R
inst_6 : ContinuousSMul S M
⊢ ContinuousSMul S (tsze R M)

Tactic:
Prod.continuousSMul

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt, setOf, TrivSqZeroExt.fst, Prod.continuousSMul
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid R
inst_3 : AddCommMonoid M
f : α → R
a : R
h : HasSum f a
⊢ HasSum (α := tsze R M) (fun (x : α) ↦ inl (f x)) (inl a)

Tactic:
h.map (⟨⟨inl, inl_zero _⟩, inl_add _⟩ : R →+ tsze R M) continuous_inl

Premises used: HasSum.map, TrivSqZeroExt.inl_add, AddMonoidHom.mk, TrivSqZeroExt.inl, ZeroHom.mk, TrivSqZeroExt.continuous_inl, TrivSqZeroExt.inl_zero
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid R
inst_3 : AddCommMonoid M
f : α → M
a : M
h : HasSum f a
⊢ HasSum (α := tsze R M) (fun (x : α) ↦ inr (f x)) (inr a)

Tactic:
h.map (⟨⟨inr, inr_zero _⟩, inr_add _⟩ : M →+ tsze R M) continuous_inr

Premises used: HasSum.map, TrivSqZeroExt.inr, AddMonoidHom.mk, ZeroHom.mk, TrivSqZeroExt.continuous_inr, TrivSqZeroExt.inr_add, TrivSqZeroExt.inr_zero
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid R
inst_3 : AddCommMonoid M
f : α → tsze R M
a : tsze R M
h : HasSum f a
⊢ HasSum (fun (x : α) ↦ (f x).fst) a.fst

Tactic:
h.map (⟨⟨fst, fst_zero⟩, fst_add⟩ : tsze R M →+ R) continuous_fst

Premises used: HasSum.map, TrivSqZeroExt.fst_add, AddMonoidHom.mk, ZeroHom.mk, TrivSqZeroExt.fst, TrivSqZeroExt.continuous_fst, TrivSqZeroExt.fst_zero
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
R : Type u_3
M : Type u_4
inst : TopologicalSpace R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid R
inst_3 : AddCommMonoid M
f : α → tsze R M
a : tsze R M
h : HasSum f a
⊢ HasSum (fun (x : α) ↦ (f x).snd) a.snd

Tactic:
h.map (⟨⟨snd, snd_zero⟩, snd_add⟩ : tsze R M →+ M) continuous_snd

Premises used: HasSum.map, TrivSqZeroExt.snd, TrivSqZeroExt.continuous_snd, TrivSqZeroExt.snd_add, AddMonoidHom.mk, ZeroHom.mk, TrivSqZeroExt.snd_zero
-- Module: Mathlib.Topology.Instances.TrivSqZeroExt
Goal:
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst : UniformSpace R
inst_1 : UniformSpace M
inst_2 : CompleteSpace R
inst_3 : CompleteSpace M
⊢ CompleteSpace (tsze R M)

Tactic:
inferInstanceAs <| CompleteSpace (R × M)

Premises used: _private.0.TrivSqZeroExt.instCompleteSpace._proof_1