awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ (F := E) ∞ (fun (x : ℝ × E) ↦ x.1⁻¹ • x.2) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
ContDiffOn.smul (contDiffOn_fst.inv fun x hx => ne_of_gt hx.1.1) contDiffOn_snd

Premises used: contDiffOn_fst, ne_of_gt, And.left, ContDiffOn.smul, contDiffOn_snd, ContDiffOn.inv
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ (F := E) ∞ (fun (x : ℝ × E) ↦ x.1⁻¹ • x.2) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
exact ContDiffOn.smul (contDiffOn_fst.inv fun x hx => ne_of_gt hx.1.1) contDiffOn_snd

Premises used: contDiffOn_fst, ne_of_gt, ContDiffOn.smul, contDiffOn_snd, ContDiffOn.inv
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
D_lt_one : D < 1
⊢ Eq.{u_1 + 1} (α := Set E) (support (y D)) (ball 0 (1 + D))

Tactic:
support_eq_iff.2
    ⟨fun _ hx => (y_pos_of_mem_ball Dpos D_lt_one hx).ne', fun _ hx =>
      y_eq_zero_of_notMem_ball Dpos hx⟩

Premises used: Iff.mpr, ExistsContDiffBumpBase.y_eq_zero_of_notMem_ball, Function.support_eq_iff, ExistsContDiffBumpBase.y_pos_of_mem_ball, LT.lt.ne', And.intro
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
⊢ HasContDiffBump E

Tactic:
⟨⟨?_⟩⟩

Premises used: HasContDiffBump.mk, Nonempty.intro
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
refine : ContDiffBumpBase E
⊢ HasContDiffBump E

Tactic:
refine ⟨⟨?_⟩⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
R : ℝ
hR : 1 < R
ha : 0 < R - 1
hb : 0 < R + 1
⊢ 0 < (R - 1) / (R + 1)

Tactic:
apply div_pos

Premises used: div_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
R : ℝ
hR : 1 < R
linarith : R - 1 ≤ 0 → 1 - R + (R - 1 - 0) = 0
⊢ 0 < R - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
R : ℝ
hR : 1 < R
linarith : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (R + 1 - 0) = 0
linarith₁ : R + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < R + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)

Tactic:
have IR : ∀ R : ℝ, 1 < R → 0 < (R - 1) / (R + 1) := by intro R hR; apply div_pos <;> linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
pos : ∀ (h : 1 < R), 0 ≤ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ∧ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ≤ 1
neg : ∀ (h : ¬1 < R), LE.le (α := ℝ) 0 0 ∧ LE.le (α := ℝ) 0 1
⊢ (0 ≤ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) ∧
    (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) ≤ 1

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : 1 < R
⊢ 0 ≤ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ∧ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ≤ 1

Tactic:
⟨y_nonneg _ _, y_le_one _ (IR R h)⟩

Premises used: ExistsContDiffBumpBase.y_nonneg, And.intro, ExistsContDiffBumpBase.y_le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : 1 < R
⊢ 0 ≤ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ∧ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ≤ 1

Tactic:
refine ⟨y_nonneg _ _, y_le_one _ (IR R h)⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : ¬1 < R
⊢ LE.le (α := ℝ) 0 0 ∧ LE.le (α := ℝ) 0 1

Tactic:
simp only [le_refl, zero_le_one, and_self]

Premises used: le_refl, and_self, zero_le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
pos : 1 < R → y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) = y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x)
neg : ¬1 < R → Eq (α := ℝ) 0 0
⊢ (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) else 0) =
    if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : 1 < R
⊢ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) = y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x)

Tactic:
simp only [y_neg, smul_neg]

Premises used: smul_neg, ExistsContDiffBumpBase.y_neg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : ¬1 < R
⊢ Eq (α := ℝ) 0 0

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
this :
  ContDiffOn ℝ ∞
    (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
apply :
  ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ,
    uncurry (fun (R : ℝ) (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) x =
      Function.comp (β := ℝ × E) (uncurry y) (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2)) x
⊢ ContDiffOn ℝ (F := ℝ) ∞
    (uncurry fun (R : ℝ) (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
apply this.congr

Premises used: ContDiffOn.congr
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
this :
  ContDiffOn ℝ ∞
    (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
⊢ uncurry (fun (R : ℝ) (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) (R, x) =
    Function.comp (β := ℝ × E) (uncurry y) (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2)) (R, x)

Tactic:
simp only [hR, uncurry_apply_pair, if_true, Function.comp_apply]

Premises used: if_true, Function.comp_apply, Function.uncurry_apply_pair
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
ContDiffOn :
  _root_.ContDiffOn ℝ ∞
    (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
⊢ _root_.ContDiffOn ℝ (F := ℝ) ∞
    (uncurry fun (R : ℝ) (x : E) ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
suffices
          ContDiffOn ℝ ∞
            (uncurry y ∘ fun p : ℝ × E => ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
            (Ioi 1 ×ˢ univ) by
          apply this.congr
          rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
          simp only [hR, uncurry_apply_pair, if_true, Function.comp_apply]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
hf :
  ContDiffOn ℝ (F := ℝ × E) ∞ (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
st :
  MapsTo (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ ∞
    (Function.comp (β := ℝ × E) (uncurry y) fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
apply (y_smooth E).comp

Premises used: ContDiffOn.comp, ExistsContDiffBumpBase.y_smooth
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
hf :
  ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ (x.1 - 1) / (x.1 + 1)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
hf₁ :
  ContDiffOn ℝ (F := E) ∞ (fun (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹ • x.2)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
⊢ ContDiffOn ℝ (F := ℝ × E) ∞ (fun (p : ℝ × E) ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2))
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
apply ContDiffOn.prodMk

Premises used: ContDiffOn.prodMk
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ (x.1 - 1) / (x.1 + 1)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
(contDiffOn_fst.sub contDiffOn_const).div (contDiffOn_fst.add contDiffOn_const) ?_

Premises used: ContDiffOn.add, contDiffOn_fst, ContDiffOn.div, ContDiffOn.sub, contDiffOn_const
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
hf : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ, x.1 + 1 ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ (x.1 - 1) / (x.1 + 1)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
refine
              (contDiffOn_fst.sub contDiffOn_const).div (contDiffOn_fst.add contDiffOn_const) ?_

Premises used: ContDiffOn.add, contDiffOn_fst, ContDiffOn.div, ContDiffOn.sub, contDiffOn_const
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
hf : 0 < (R, x).1 + 1
⊢ (R, x).1 + 1 ≠ 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
hf : 0 < R + 1
⊢ 0 < (R, x).1 + 1

Tactic:
dsimp only
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
linarith : R + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (R + 1 - 0) = 0
linarith₁ : R + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < R + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
apply :
  ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)
⊢ ContDiffOn ℝ (F := E) ∞ (fun (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹ • x.2)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
apply ContDiffOn.smul _ contDiffOn_snd

Premises used: ContDiffOn.smul, contDiffOn_snd
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
((contDiffOn_fst.add contDiffOn_const).div_const _).inv ?_

Premises used: ContDiffOn.add, contDiffOn_fst, ContDiffOn.div_const, ContDiffOn.inv, contDiffOn_const
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
refine : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ, (x.1 + 1) / 2 ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((x.1 + 1) / 2)⁻¹) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioi 1) univ)

Tactic:
refine ((contDiffOn_fst.add contDiffOn_const).div_const _).inv ?_

Premises used: ContDiffOn.add, contDiffOn_fst, ContDiffOn.div_const, ContDiffOn.inv, contDiffOn_const
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
h : 0 < ((R, x).1 + 1) / 2
⊢ ((R, x).1 + 1) / 2 ≠ 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
h : 0 < (R + 1) / 2
⊢ 0 < ((R, x).1 + 1) / 2

Tactic:
dsimp only
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
linarith : (R + 1) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (R + 1) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ :
  (R + 1) / 2 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - R) + (1 * R + HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 2 0) = 0
linarith₄ : (R + 1) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < (R + 1) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
ha : 0 < R - 1
hb : 0 < R + 1
⊢ 0 < (R - 1) / (R + 1)

Tactic:
apply div_pos

Premises used: div_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
linarith : R - 1 ≤ 0 → 1 - R + (R - 1 - 0) = 0
⊢ 0 < R - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
⊢ 0 < (R - 1) / (R + 1)

Tactic:
have A : 0 < (R - 1) / (R + 1) := by apply div_pos <;> linarith
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
A : 0 < (R - 1) / (R + 1)
apply : R - 1 < R + 1
apply₁ : 0 < R + 1
⊢ (R - 1) / (R + 1) < 1

Tactic:
apply (div_lt_one _).2

Premises used: Iff.mpr, div_lt_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
inst_2 : FiniteDimensional ℝ E_1
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right : Membership.mem (γ := Set E) univ (R, x).2
A : 0 < (R - 1) / (R + 1)
linarith : R + 1 ≤ R - 1 → HMul.hMul (α := ℝ) 2 (-1) + (R + 1 - (R - 1)) = 0
linarith₁ : R + 1 ≤ R - 1 → GT.gt (α := ℝ) 2 0
⊢ R - 1 < R + 1

Tactic:
linarith