awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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 γ v s
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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⁻¹
⊢ IsMIntegralCurveOn γ v s
have h₁ : v = a⁻¹ • a • v
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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
⊢ IsMIntegralCurveOn γ v s
have h₂ : s = {t : ℝ | Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} (t * a⁻¹)}
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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}
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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
⊢ IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)
have rw : ∀ (hγ : ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) {a : ℝ} (ha : a ≠ 0),
  ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)
Tactic: rw [isMIntegralCurveAt_iff'] at *
Cleared hypotheses: hγ, a, ha
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)
have obtain : ∀ (ε : ℝ) (hε : ε > 0) (h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)),
  ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)
Tactic: obtain ⟨ε, hε, h⟩ := hγ
Cleared hypotheses: hγ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀ ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) ε)
have refine : IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (Metric.ball (t₀ / a) (ε / |a|))
Tactic: refine ⟨ε / |a|, by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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) (Metric.ball (t₀ / a) (ε / |a|))
have h₁ : Metric.ball (t₀ / a) (ε / |a|) = {t : ℝ | t * a ∈ Metric.ball t₀ ε}
Tactic: convert! h.comp_mul a
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀ ε)
⊢ Metric.ball (t₀ / a) (ε / |a|) = {t : ℝ | t * a ∈ Metric.ball t₀ ε}
have h₁ : ∀ (t : ℝ), t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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 : ℝ
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₁ : t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ t * a ∈ Metric.ball 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀ ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₂ : dist t (t₀ / a) < ε / |a| ↔ t * a ∈ Metric.ball 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀ ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₃ : dist t (t₀ / a) < ε / |a| ↔ dist (t * a) 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀ < ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₄ : |t - t₀ / a| < ε / |a| ↔ dist (t * a) 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀ < ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₅ : |t - t₀ / a| < ε / |a| ↔ |t * a - 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀| < ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₆ : |t - t₀ / a| * |a| < ε ↔ |t * a - 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀| < ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₇ : |(t - t₀ / a) * a| < ε ↔ |t * a - 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀| < ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₈ : |t * a - t₀ / a * a| < ε ↔ |t * a - 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀| < ε
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ Metric.ball t₀ ε} t
have h₉ : |t * a - t₀| < ε ↔ |t * a - 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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₀
have refine : ∀ (hγ : IsMIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) (t₀ / a)), IsMIntegralCurveAt γ v t₀
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul_ne_zero ha⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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 γ v t₀
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
Tactic: convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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⁻¹
⊢ IsMIntegralCurveAt γ v t₀
have h₁ : v = a⁻¹ • a • v
Tactic: convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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
⊢ IsMIntegralCurveAt γ v t₀
have h₂ : t₀ = t₀ / a / a⁻¹
Tactic: convert! hγ.comp_mul_ne_zero (inv_ne_zero ha)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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)
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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 : ℝ
⊢ IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v)
have rw : ∀ (hγ : IsMIntegralCurveOn γ v univ) (a : ℝ), IsMIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (a • v) univ
Tactic: rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *
Cleared hypotheses: hγ, a
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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
have refine : ∀ (hγ : IsMIntegralCurve (γ ∘ fun (x : ℝ) ↦ x * a) (a • v)), IsMIntegralCurve γ v
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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 γ v
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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⁻¹
⊢ IsMIntegralCurve γ v
have h₁ : v = a⁻¹ • a • v
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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)
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Transform (goal)
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
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
t : ℝ
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (fun (x_1 : ℝ) ↦ x) t (smulRight (S := ℝ) 1 (v ((fun (x_1 : ℝ) ↦ x) t)))
have rw : HasMFDerivAt.{0, 0, 0, 0, u_1, u_2, u_3} (modelWithCornersSelf ℝ ℝ) I (M' := M) (fun (x_1 : ℝ) ↦ x) t 0
Tactic: rw [h, smulRight_one_eq_toSpanSingleton, toSpanSingleton_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
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
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ γ a' 0 = γ a 0
have rw : γ a' 0 = x
Tactic: rw [hγx a, hγx a']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
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
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
rw : γ a' 0 = x
⊢ γ a' 0 = γ a 0
have rw₁ : x = x
Tactic: rw [hγx a, hγx a']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
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
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ EqOn (γ a') (γ a) (Ioo (-a') a')
have apply : 0 ∈ Ioo (-a') a'
Tactic: apply isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless _ hv
    (hγ a' (by positivity)) ((hγ a (lt_of_lt_of_le hpos hle)).mono _)
    (by rw [hγx a, hγx a'])
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.UniformTime (goal)
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
inst_5 : IsManifold I 1 M
inst_6 : T2Space M
v : (x : M) → TangentSpace I x
inst_7 : BoundarylessManifold I M
hv :
  ContMDiff I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1 fun (x : M) ↦
    ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
apply : 0 ∈ Ioo (-a') a'
⊢ EqOn (γ a') (γ a) (Ioo (-a') a')
have apply₁ : Ioo (-a') a' ⊆ Ioo (-a) a
Tactic: apply isMIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless _ hv
    (hγ a' (by positivity)) ((hγ a (lt_of_lt_of_le hpos hle)).mono _)
    (by rw [hγx a, hγx a'])