awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ)))) ∘SL
      ContinuousLinearMap.smulRight (S := ℝ) 1 a)

Tactic:
HasMFDerivWithinAt.comp t (hγ (t * a) ht)
    ⟨(continuous_mul_const _).continuousWithinAt, ?_⟩ subset_rfl

Premises used: HMul.hMul, instModuleTangentSpace._aux_1, And.intro, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, Continuous.continuousWithinAt, HasMFDerivWithinAt.comp, subset_rfl, continuous_mul_const
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
refine :
  HasFDerivWithinAt (𝕜 := ℝ)
    (writtenInExtChartAt (M' := ℝ) (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun (x : ℝ) ↦
      HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    (ContinuousLinearMap.smulRight (S := ℝ) 1 a)
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t).symm : ℝ → ℝ) ⁻¹'
        {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} ∩
      range (↑(modelWithCornersSelf ℝ ℝ) : ℝ → ℝ))
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) : ℝ → ℝ) t)
⊢ HasMFDerivWithinAt (modelWithCornersSelf ℝ ℝ) I (γ ∘ fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ (HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ)))) ∘SL
      ContinuousLinearMap.smulRight (S := ℝ) 1 a)

Tactic:
refine HasMFDerivWithinAt.comp t (hγ (t * a) ht)
    ⟨(continuous_mul_const _).continuousWithinAt, ?_⟩ subset_rfl

Premises used: And.intro, Continuous.continuousWithinAt, HasMFDerivWithinAt.comp, subset_rfl, continuous_mul_const
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
simp :
  HasFDerivWithinAt (𝕜 := ℝ) (fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    (ContinuousLinearMap.smulRight (S := ℝ) 1 a) {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t
⊢ HasFDerivWithinAt (𝕜 := ℝ)
    (writtenInExtChartAt (M' := ℝ) (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) t fun (x : ℝ) ↦
      HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    (ContinuousLinearMap.smulRight (S := ℝ) 1 a)
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t).symm : ℝ → ℝ) ⁻¹'
        {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} ∩
      range (↑(modelWithCornersSelf ℝ ℝ) : ℝ → ℝ))
    ((↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) : ℝ → ℝ) t)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasFDerivWithinAt (𝕜 := ℝ) (fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    (ContinuousLinearMap.smulRight (S := ℝ) 1 a) {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t

Tactic:
HasFDerivWithinAt.mul_const' (hasFDerivWithinAt_id _ _) _

Premises used: ContinuousLinearMap.smulRight, HasFDerivWithinAt.mul_const', instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, MulOpposite.unop, LinearMap.smulRight, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasFDerivWithinAt (𝕜 := ℝ) (fun (x : ℝ) ↦ HMul.hMul (β := ℝ) x ((1 : (a : ℝ) → ℝ) a : ℝ))
    (ContinuousLinearMap.smulRight (S := ℝ) 1 a) {t : ℝ | HMul.hMul (β := ℝ) t ((1 : (a : ℝ) → ℝ) a : ℝ) ∈ s} t

Tactic:
exact HasFDerivWithinAt.mul_const' (hasFDerivWithinAt_id _ _) _

Premises used: HasFDerivWithinAt.mul_const'
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s} ↔ IsMIntegralCurveOn γ v s

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

Premises used: IsMIntegralCurveOn.comp_mul, Iff.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
refine : ∀ (hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s}), IsMIntegralCurveOn γ v s
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s} ↔ IsMIntegralCurveOn γ v s

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul a⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s}
⊢ IsMIntegralCurveOn (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹) (a⁻¹ • a • v)
    {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} (t * a⁻¹)}

Tactic:
hγ.comp_mul a⁻¹

Premises used: IsMIntegralCurveOn.comp_mul, Inv.inv
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s}
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ : v = a⁻¹ • a • v
h₂ : s = {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} (t * a⁻¹)}
⊢ IsMIntegralCurveOn γ v s

Tactic:
convert! hγ.comp_mul a⁻¹

Premises used: IsMIntegralCurveOn.comp_mul, Inv.inv
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * 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.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s}
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t

Tactic:
simp only [Function.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.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s}
⊢ v = a⁻¹ • a • v

Tactic:
simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]

Premises used: inv_mul_eq_div, smul_smul, one_smul, div_self
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ s}
⊢ s = {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} (t * a⁻¹)}

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

Premises used: mul_assoc, inv_mul_eq_div, Set.mem_setOf_eq, Set.setOf_mem_eq, mul_one, div_self
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγ : IsMIntegralCurveAt γ v t₀
a : ℝ
ha : a ≠ 0
rw :
  ∀ (hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) {a : ℝ} (ha : a ≠ 0),
    ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)

Tactic:
rw [isMIntegralCurveAt_iff'] at *

Premises used: isMIntegralCurveAt_iff'
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
a : ℝ
ha : a ≠ 0
obtain :
  ∀ (ε : ℝ) (hε : ε > 0) (h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)),
    ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)

Tactic:
obtain ⟨ε, hε, h⟩ := hγ
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ε / |a| > 0

Tactic:
positivity
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
refine : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) (ε / |a|))
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)

Tactic:
refine ⟨ε / |a|, by positivity, ?_⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) {t : ℝ | t * a ∈ Metric.ball t₀ ε}

Tactic:
h.comp_mul a

Premises used: IsMIntegralCurveOn.comp_mul
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
h₁ : Metric.ball (t₀ / a) (ε / |a|) = {t : ℝ | t * a ∈ Metric.ball t₀ ε}
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) (ε / |a|))

Tactic:
convert! h.comp_mul a

Premises used: IsMIntegralCurveOn.comp_mul
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
h₁ : ∀ (t : ℝ), t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
⊢ Metric.ball (t₀ / a) (ε / |a|) = {t : ℝ | t * a ∈ Metric.ball t₀ ε}

Tactic:
ext t
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
t : ℝ
h₁ : t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ t * a ∈ Metric.ball t₀ ε
h₂ : dist t (t₀ / a) < ε / |a| ↔ t * a ∈ Metric.ball t₀ ε
h₃ : dist t (t₀ / a) < ε / |a| ↔ dist (t * a) t₀ < ε
h₄ : |t - t₀ / a| < ε / |a| ↔ dist (t * a) t₀ < ε
h₅ : |t - t₀ / a| < ε / |a| ↔ |t * a - t₀| < ε
h₆ : |t - t₀ / a| * |a| < ε ↔ |t * a - t₀| < ε
h₇ : |(t - t₀ / a) * a| < ε ↔ |t * a - t₀| < ε
h₈ : |t * a - t₀ / a * a| < ε ↔ |t * a - t₀| < ε
h₉ h₁₀ : |t * a - t₀| < ε ↔ |t * a - t₀| < ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t

Tactic:
rw [mem_setOf_eq, Metric.mem_ball, Metric.mem_ball, Real.dist_eq, Real.dist_eq,
    lt_div_iff₀ (abs_pos.mpr ha), ← abs_mul, sub_mul, div_mul_cancel₀ _ ha]

Premises used: Iff.mpr, div_mul_cancel₀, lt_div_iff₀, abs_mul, Set.mem_setOf_eq, Metric.mem_ball, sub_mul, abs_pos, Real.dist_eq
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a) ↔ IsMIntegralCurveAt γ v t₀

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

Premises used: Iff.intro, IsMIntegralCurveAt.comp_mul_ne_zero
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
refine : ∀ (hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)), IsMIntegralCurveAt γ v t₀
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a) ↔ IsMIntegralCurveAt γ v t₀

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul_ne_zero ha⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)
⊢ IsMIntegralCurveAt (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹) (a⁻¹ • a • v) (t₀ / a / a⁻¹)

Tactic:
hγ.comp_mul_ne_zero (inv_ne_zero ha)

Premises used: IsMIntegralCurveAt.comp_mul_ne_zero, inv_ne_zero
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ : v = a⁻¹ • a • v
h₂ : t₀ = t₀ / a / a⁻¹
⊢ IsMIntegralCurveAt γ v t₀

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

Premises used: IsMIntegralCurveAt.comp_mul_ne_zero, inv_ne_zero
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (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.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t

Tactic:
simp only [Function.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.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)
⊢ v = a⁻¹ • a • v

Tactic:
simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]

Premises used: inv_mul_eq_div, smul_smul, one_smul, div_self
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (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.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurve γ v
a : ℝ
rw : ∀ (hγ : IsMIntegralCurveOn γ v univ) (a : ℝ), IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) univ
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v)

Tactic:
rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *

Premises used: isMIntegralCurve_iff_isMIntegralCurveOn
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurveOn γ v univ
a : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) univ

Tactic:
hγ.comp_mul _

Premises used: Set.Mem, Set.univ, setOf, IsMIntegralCurveOn.comp_mul
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurveOn γ v univ
a : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) univ

Tactic:
exact hγ.comp_mul _

Premises used: IsMIntegralCurveOn.comp_mul
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) ↔ IsMIntegralCurve γ v

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

Premises used: IsMIntegralCurve.comp_mul, Iff.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
refine : ∀ (hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v)), IsMIntegralCurve γ v
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) ↔ IsMIntegralCurve γ v

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v)
⊢ IsMIntegralCurve (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹) (a⁻¹ • a • v)

Tactic:
hγ.comp_mul a⁻¹

Premises used: Inv.inv, IsMIntegralCurve.comp_mul
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ : v = a⁻¹ • a • v
⊢ IsMIntegralCurve γ v

Tactic:
convert! hγ.comp_mul a⁻¹

Premises used: Inv.inv, IsMIntegralCurve.comp_mul