awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
j : ι_1
⊢ (x + Pi.single (M := E) i (d n)) j ∈ closure[inst_3 j] (s j)
have hds₁ : ∀ (hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)) ⦃y : E j⦄ (hy : y ∈ tangentConeAt 𝕜 (s j) (x j))
  (d : ι → E j) (hd₀ : Tendsto d l (𝓝 0)) (hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j)
  (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)) (hn : x j + d n ∈ s j),
  (x + Pi.single (M := E) j (d n)) j ∈ closure[inst_3 j] (s j)
Tactic: rcases eq_or_ne j i with rfl | hj
Cleared hypotheses: i, hi, y, hy, d, hd₀, hds, hcd, hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
j : ι_1
hds₁ :
  ∀ (hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)) ⦃y : E j⦄ (hy : y ∈ tangentConeAt 𝕜 (s j) (x j))
    (d : ι → E j) (hd₀ : Tendsto d l (𝓝 0)) (hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j)
    (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)) (hn : x j + d n ∈ s j),
    (x + Pi.single (M := E) j (d n)) j ∈ closure[inst_3 j] (s j)
⊢ (x + Pi.single (M := E) i (d n)) j ∈ closure[inst_3 j] (s j)
have hds₂ : ∀ (hj : j ≠ i), (x + Pi.single (M := E) i (d n)) j ∈ closure[inst_3 j] (s j)
Tactic: rcases eq_or_ne j i with rfl | hj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun (n : ι) ↦ c n • Pi.single (M := E) i (d n)) l (𝓝 (Pi.single (M := E) i y))
have hcd₁ : ∀ (x : ι_1), Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) x) l (𝓝 (Pi.single (M := E) i y x))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
j : ι_1
⊢ Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) j) l (𝓝 (Pi.single (M := E) i y j))
have hcd₁ : ∀ (hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)) ⦃y : E j⦄ (hy : y ∈ tangentConeAt 𝕜 (s j) (x j))
  (d : ι → E j) (hd₀ : Tendsto d l (𝓝 0)) (hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j)
  (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
  Tendsto (fun (i : ι) ↦ (c i • Pi.single (M := E) j (d i)) j) l (𝓝 (Pi.single (M := E) j y j))
Tactic: rcases eq_or_ne j i with rfl | hj
Cleared hypotheses: i, hi, y, hy, d, hd₀, hds, hcd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι_1 : Type u_2
E : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommGroup (E i)
inst_2 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι_1) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι_1), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι_1), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι_1) → Set (E i)
x : (i : ι_1) → E i
inst_6 : DecidableEq ι_1
i : ι_1
hi : ∀ (j : ι_1), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
j : ι_1
hcd₁ :
  ∀ (hi : ∀ (j_1 : ι_1), j_1 ≠ j → x j_1 ∈ closure[inst_3 j_1] (s j_1)) ⦃y : E j⦄ (hy : y ∈ tangentConeAt 𝕜 (s j) (x j))
    (d : ι → E j) (hd₀ : Tendsto d l (𝓝 0)) (hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j)
    (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
    Tendsto (fun (i : ι) ↦ (c i • Pi.single (M := E) j (d i)) j) l (𝓝 (Pi.single (M := E) j y j))
⊢ Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) j) l (𝓝 (Pi.single (M := E) i y j))
have hcd₂ : ∀ (hj : j ≠ i), Tendsto (fun (i_1 : ι) ↦ (c i_1 • Pi.single (M := E) i (d i_1)) j) l (𝓝 (Pi.single (M := E) i y j))
Tactic: rcases eq_or_ne j i with rfl | hj
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x
have simp : ∀
  (h :
    ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
  Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
    Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
Tactic: simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
    Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
have refine : closure[Pi.topologicalSpace]
    (Set.pi (α := E) univ fun (i : ι) ↦ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i))) ⊆
  closure[Pi.topologicalSpace] (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
Tactic: refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
⊢ closure[Pi.topologicalSpace]
      (Set.pi (α := E) univ fun (i : ι) ↦ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i))) ⊆
    closure[Pi.topologicalSpace]
      (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
have simp : closure[Pi.topologicalSpace]
    (↑(⨆ (i : ι),
          Submodule.span 𝕜
            ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
              tangentConeAt 𝕜 (s i) (x i))) :
      Set ((i : ι) → E i)) ⊆
  closure[Pi.topologicalSpace] (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
Tactic: simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
⊢ closure[Pi.topologicalSpace]
      (↑(⨆ (i : ι),
            Submodule.span 𝕜
              ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
                tangentConeAt 𝕜 (s i) (x i))) :
        Set ((i : ι) → E i)) ⊆
    closure[Pi.topologicalSpace]
      (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
have h₁ : LE.le (α := Submodule 𝕜 ((i : ι) → E i))
  (⨆ (i : ι),
    Submodule.span 𝕜
      ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
        tangentConeAt 𝕜 (s i) (x i)))
  (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
⊢ LE.le (α := Submodule 𝕜 ((i : ι) → E i))
    (⨆ (i : ι),
      Submodule.span 𝕜
        ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
          tangentConeAt 𝕜 (s i) (x i)))
    (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
have h₁ : ∀ (i : ι),
  LE.le (α := Submodule 𝕜 ((i : ι) → E i))
    (Submodule.span 𝕜
      ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
        tangentConeAt 𝕜 (s i) (x i)))
    (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
Tactic: refine iSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)
i : ι
⊢ LE.le (α := Submodule 𝕜 ((i : ι) → E i))
    (Submodule.span 𝕜
      ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
        tangentConeAt 𝕜 (s i) (x i)))
    (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
have h₁ : (⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) '' tangentConeAt 𝕜 (s i) (x i) ⊆
  tangentConeAt 𝕜 (Set.pi (α := E) univ s) x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x
have simp : ∀
  (h :
    ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
  Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
    Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
Tactic: classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
  simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]
  gcongr
  refine iSup_le fun i ↦ ?_
  gcongr
  exact mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
simp :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
      Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x
have simp₁ : ∀
  (h :
    ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
  closure[Pi.topologicalSpace]
      (Set.pi (α := E) univ fun (i : ι) ↦ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i))) ⊆
    closure[Pi.topologicalSpace]
      (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
Tactic: classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
  simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]
  gcongr
  refine iSup_le fun i ↦ ?_
  gcongr
  exact mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
simp :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
      Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
simp₁ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    closure[Pi.topologicalSpace]
        (Set.pi (α := E) univ fun (i : ι) ↦ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i))) ⊆
      closure[Pi.topologicalSpace]
        (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x
have simp₂ : ∀
  (h :
    ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
  closure[Pi.topologicalSpace]
      (↑(⨆ (i : ι),
            Submodule.span 𝕜
              ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
                tangentConeAt 𝕜 (s i) (x i))) :
        Set ((i : ι) → E i)) ⊆
    closure[Pi.topologicalSpace]
      (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
Tactic: classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
  simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]
  gcongr
  refine iSup_le fun i ↦ ?_
  gcongr
  exact mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
simp :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
      Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
simp₁ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    closure[Pi.topologicalSpace]
        (Set.pi (α := E) univ fun (i : ι) ↦ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i))) ⊆
      closure[Pi.topologicalSpace]
        (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
simp₂ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    closure[Pi.topologicalSpace]
        (↑(⨆ (i : ι),
              Submodule.span 𝕜
                ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
                  tangentConeAt 𝕜 (s i) (x i))) :
          Set ((i : ι) → E i)) ⊆
      closure[Pi.topologicalSpace]
        (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x
have h₁ : ∀
  (h :
    ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
  LE.le (α := Submodule 𝕜 ((i : ι) → E i))
    (⨆ (i : ι),
      Submodule.span 𝕜
        ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
          tangentConeAt 𝕜 (s i) (x i)))
    (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
Tactic: classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
  simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]
  gcongr
  refine iSup_le fun i ↦ ?_
  gcongr
  exact mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Pi (goal)
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
simp :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i)) ∧
      Membership.mem (γ := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ closure[inst_3 i] (s i)) x
simp₁ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    closure[Pi.topologicalSpace]
        (Set.pi (α := E) univ fun (i : ι) ↦ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i))) ⊆
      closure[Pi.topologicalSpace]
        (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
simp₂ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    closure[Pi.topologicalSpace]
        (↑(⨆ (i : ι),
              Submodule.span 𝕜
                ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
                  tangentConeAt 𝕜 (s i) (x i))) :
          Set ((i : ι) → E i)) ⊆
      closure[Pi.topologicalSpace]
        (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)) : Set ((i : ι) → E i))
h₁ :
  ∀
    (h :
      ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i)),
    LE.le (α := Submodule 𝕜 ((i : ι) → E i))
      (⨆ (i : ι),
        Submodule.span 𝕜
          ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
            tangentConeAt 𝕜 (s i) (x i)))
      (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
⊢ UniqueDiffWithinAt 𝕜 (Set.pi (α := E) univ s) x
have h₂ : ∀ (h : ∀ (i : ι), Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) : Set (E i)) ∧ x i ∈ closure[inst_3 i] (s i))
  (i : ι),
  LE.le (α := Submodule 𝕜 ((i : ι) → E i))
    (Submodule.span 𝕜
      ((⇑(LinearMap.single 𝕜 E i : E i →ₗ[𝕜] (i : ι) → E i) : (a : E i) → (i : ι) → E i) ''
        tangentConeAt 𝕜 (s i) (x i)))
    (Submodule.span 𝕜 (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x))
Tactic: classical
  simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢
  refine ⟨.of_closure <| (dense_pi univ fun i _ ↦ (h i).1).closure.mono ?_, fun i _ => (h i).2⟩
  simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]
  gcongr
  refine iSup_le fun i ↦ ?_
  gcongr
  exact mapsTo_tangentConeAt_pi (fun j _ ↦ (h j).2) |>.image_subset
Cleared hypotheses: h