awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt ε : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ Metric.ball t₀ ε) ↔
    IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
isIntegralCurveOn_comp_add

Premises used: isIntegralCurveOn_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt ε : ℝ
h : Metric.ball (t₀ - dt) ε = -dt +ᵥ Metric.ball t₀ ε
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε) ↔
    IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
convert! isIntegralCurveOn_comp_add

Premises used: isIntegralCurveOn_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt ε : ℝ
⊢ Metric.ball (t₀ - dt) ε = -dt +ᵥ Metric.ball t₀ ε

Tactic:
simp [neg_add_eq_sub]

Premises used: neg_add_eq_sub
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
hγ : IsIntegralCurveAt γ v t₀
dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (t₀ - dt)

Tactic:
isIntegralCurveAt_comp_add.mpr hγ

Premises used: Iff.mpr, isIntegralCurveAt_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x - dt) (v ∘ fun (x : ℝ) ↦ x - dt) (t₀ + dt) ↔ IsIntegralCurveAt γ v t₀

Tactic:
simpa using isIntegralCurveAt_comp_add (dt := -dt)

Premises used: isIntegralCurveAt_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
hγ : IsIntegralCurveAt γ v t₀
dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x - dt) (v ∘ fun (x : ℝ) ↦ x - dt) (t₀ + dt)

Tactic:
isIntegralCurveAt_comp_sub.mpr hγ

Premises used: Iff.mpr, isIntegralCurveAt_comp_sub
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
dt : ℝ
rw :
  ∀ (hγ : IsIntegralCurveOn γ v univ) (dt : ℝ),
    IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) univ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt)

Tactic:
rw [← isIntegralCurveOn_univ] at *

Premises used: isIntegralCurveOn_univ
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurveOn γ v univ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) univ

Tactic:
simpa using hγ.comp_add dt

Premises used: IsIntegralCurveOn.comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
simp_rw : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) univ ↔ IsIntegralCurveOn γ v univ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) ↔ IsIntegralCurve γ v

Tactic:
simp_rw [← isIntegralCurveOn_univ]

Premises used: isIntegralCurveOn_univ
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (HVAdd.hVAdd (β := Set ℝ) (-dt) univ) ↔
    IsIntegralCurveOn γ v univ

Tactic:
isIntegralCurveOn_comp_add

Premises used: isIntegralCurveOn_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
h : univ = HVAdd.hVAdd (β := Set ℝ) (-dt) univ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) univ ↔ IsIntegralCurveOn γ v univ

Tactic:
convert! isIntegralCurveOn_comp_add

Premises used: isIntegralCurveOn_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ univ = HVAdd.hVAdd (β := Set ℝ) (-dt) univ

Tactic:
simp
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x - dt) (v ∘ fun (x : ℝ) ↦ x - dt) ↔ IsIntegralCurve γ v

Tactic:
simpa using isIntegralCurve_comp_add (dt := -dt)

Premises used: isIntegralCurve_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x - dt) (v ∘ fun (x : ℝ) ↦ x - dt)

Tactic:
isIntegralCurve_comp_sub.mpr hγ

Premises used: Iff.mpr, isIntegralCurve_comp_sub
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
simp : HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v (t * a) (γ (t * a))) {t : ℝ | t * a ∈ s} t
⊢ HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x * a)
    (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) t ((γ ∘ fun (x : ℝ) ↦ x * a) t)) {t : ℝ | t * a ∈ s} t

Tactic:
simp only [comp_apply, Pi.smul_apply]

Premises used: Function.comp_apply, Pi.smul_apply
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v (t * a) (γ (t * a))) {t : ℝ | t * a ∈ s} t

Tactic:
HasDerivWithinAt.scomp t (hγ (t * a) ht) (hasDerivAt_mul_const a).hasDerivWithinAt
    fun _ ht' ↦ ht'

Premises used: HasDerivAt.hasDerivWithinAt, HMul.hMul, HasDerivWithinAt.scomp, hasDerivAt_mul_const
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v (t * a) (γ (t * a))) {t : ℝ | t * a ∈ s} t

Tactic:
exact HasDerivWithinAt.scomp t (hγ (t * a) ht) (hasDerivAt_mul_const a).hasDerivWithinAt
    fun _ ht' ↦ ht'

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivWithinAt.scomp, hasDerivAt_mul_const
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
h : ∀ (t : ℝ), t ∈ a⁻¹ • s ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ a⁻¹ • s = {t : ℝ | t * a ∈ s}

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
t : ℝ
h : t * a ∈ s ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ t ∈ a⁻¹ • s ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t

Tactic:
rw [mem_inv_smul_set_iff₀ ha, smul_eq_mul, mul_comm]

Premises used: Set.mem_inv_smul_set_iff₀, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
t : ℝ
⊢ t * a ∈ s ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t

Tactic:
rfl
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ a⁻¹ • s = {t : ℝ | t * a ∈ s}

Tactic:
have heq : a⁻¹ • s = { t | t * a ∈ s } := by
    ext t
    rw [mem_inv_smul_set_iff₀ ha, smul_eq_mul, mul_comm]
    rfl
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s) ↔
    IsIntegralCurveOn γ v s

Tactic:
⟨fun hγ ↦ ?_, heq ▸ fun hγ ↦ hγ.comp_mul a⟩

Premises used: IsIntegralCurveOn.comp_mul, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
refine :
  ∀
    (hγ :
      IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)),
    IsIntegralCurveOn γ v s
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s) ↔
    IsIntegralCurveOn γ v s

Tactic:
refine ⟨fun hγ ↦ ?_, heq ▸ fun hγ ↦ hγ.comp_mul a⟩
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
⊢ IsIntegralCurveOn (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹)
    (HSMul.hSMul (β := ℝ → E → E) a⁻¹
      (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹))
    {t : ℝ | t * a⁻¹ ∈ a⁻¹ • s}

Tactic:
hγ.comp_mul a⁻¹

Premises used: IsIntegralCurveOn.comp_mul, Inv.inv
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ :
  v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
h₂ : s = {t : ℝ | t * a⁻¹ ∈ a⁻¹ • s}
⊢ IsIntegralCurveOn γ v s

Tactic:
convert! hγ.comp_mul a⁻¹

Premises used: IsIntegralCurveOn.comp_mul, Inv.inv
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t

Tactic:
simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]

Premises used: mul_assoc, inv_mul_eq_div, Function.comp_apply, mul_one, div_self
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
h :
  ∀ (t : ℝ) (x : E),
    v t x =
      HSMul.hSMul (β := ℝ → E → E) a⁻¹
        (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹) t x
⊢ v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
t : ℝ
x : E
⊢ v t x =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
      t x

Tactic:
simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

Premises used: mul_assoc, inv_mul_eq_div, smul_smul, one_smul, Function.comp_apply, mul_one, div_self, Pi.smul_apply
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
⊢ s = {t : ℝ | t * a⁻¹ ∈ a⁻¹ • s}

Tactic:
simp only [mul_comm _ a⁻¹, ← smul_eq_mul, mem_inv_smul_set_iff₀ ha, smul_inv_smul₀ ha,
      setOf_mem_eq]

Premises used: Set.mem_inv_smul_set_iff₀, smul_inv_smul₀, Set.setOf_mem_eq, Inv.inv, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a) ↔
    IsIntegralCurveAt γ v t₀

Tactic:
⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul_ne_zero ha⟩

Premises used: IsIntegralCurveAt.comp_mul_ne_zero, Iff.intro
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
refine :
  ∀
    (hγ :
      IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)),
    IsIntegralCurveAt γ v t₀
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a) ↔
    IsIntegralCurveAt γ v t₀

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul_ne_zero ha⟩
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
⊢ IsIntegralCurveAt (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹)
    (HSMul.hSMul (β := ℝ → E → E) a⁻¹
      (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹))
    (t₀ / a / a⁻¹)

Tactic:
hγ.comp_mul_ne_zero (inv_ne_zero ha)

Premises used: IsIntegralCurveAt.comp_mul_ne_zero, inv_ne_zero
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ :
  v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
h₂ : t₀ = t₀ / a / a⁻¹
⊢ IsIntegralCurveAt γ v t₀

Tactic:
convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)

Premises used: IsIntegralCurveAt.comp_mul_ne_zero, inv_ne_zero
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t

Tactic:
simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]

Premises used: mul_assoc, inv_mul_eq_div, Function.comp_apply, mul_one, div_self
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
h :
  ∀ (t : ℝ) (x : E),
    v t x =
      HSMul.hSMul (β := ℝ → E → E) a⁻¹
        (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹) t x
⊢ v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
t : ℝ
x : E
⊢ v t x =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
      t x

Tactic:
simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

Premises used: mul_assoc, inv_mul_eq_div, smul_smul, one_smul, Function.comp_apply, mul_one, div_self, Pi.smul_apply
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (t₀ / a)
⊢ t₀ = t₀ / a / a⁻¹

Tactic:
simp only [div_inv_eq_mul, div_mul_cancel₀ _ ha]

Premises used: div_mul_cancel₀, div_inv_eq_mul
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
a : ℝ
rw :
  ∀ (hγ : IsIntegralCurveOn γ v univ) (a : ℝ),
    IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) univ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))

Tactic:
rw [← isIntegralCurveOn_univ] at *

Premises used: isIntegralCurveOn_univ
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurveOn γ v univ
a : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) univ

Tactic:
hγ.comp_mul _

Premises used: Set.Mem, IsIntegralCurveOn.comp_mul, Set.univ, setOf
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurveOn γ v univ
a : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) univ

Tactic:
exact hγ.comp_mul _

Premises used: IsIntegralCurveOn.comp_mul
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) ↔
    IsIntegralCurve γ v

Tactic:
⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩

Premises used: IsIntegralCurve.comp_mul, Iff.intro
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
refine :
  ∀ (hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))),
    IsIntegralCurve γ v
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) ↔
    IsIntegralCurve γ v

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
⊢ IsIntegralCurve (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹)
    (HSMul.hSMul (β := ℝ → E → E) a⁻¹
      (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹))

Tactic:
hγ.comp_mul a⁻¹

Premises used: IsIntegralCurve.comp_mul, Inv.inv
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ :
  v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
⊢ IsIntegralCurve γ v

Tactic:
convert! hγ.comp_mul a⁻¹

Premises used: IsIntegralCurve.comp_mul, Inv.inv
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t

Tactic:
simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]

Premises used: mul_assoc, inv_mul_eq_div, Function.comp_apply, mul_one, div_self
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
h :
  ∀ (t : ℝ) (x : E),
    v t x =
      HSMul.hSMul (β := ℝ → E → E) a⁻¹
        (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹) t x
⊢ v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
a : ℝ
ha : a ≠ 0
hγ : IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a))
t : ℝ
x : E
⊢ v t x =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
      t x

Tactic:
simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
      smul_smul, one_smul]

Premises used: mul_assoc, inv_mul_eq_div, smul_smul, one_smul, Function.comp_apply, mul_one, div_self, Pi.smul_apply
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
x : E
h : ∀ (t : ℝ), v t x = 0
⊢ IsIntegralCurve (fun (x_1 : ℝ) ↦ x) v

Tactic:
fun t ↦ (h t) ▸ hasDerivAt_const _ _

Premises used: Eq.rec, hasDerivAt_const, IsIntegralCurve, Eq.symm