awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have h2x : Membership.mem (α := E) (tsupport g) ((L.symm : (a : E' × ℝ) → E) x : E)
Tactic: have h2x : L.symm x ∈ tsupport g :=
      (Set.ext_iff.mp (tsupport_comp_eq_preimage g L.symm.toHomeomorph) x).mp hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport g) ((L.symm : (a : E' × ℝ) → E) x : E)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have hf₁ : HasLineDerivAt ℝ f (f' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
Tactic: specialize hf (L.symm x) h2x
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport g) ((L.symm : (a : E' × ℝ) → E) x : E)
hf : HasLineDerivAt ℝ f (f' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have hf₁ : HasLineDerivAt ℝ
  (Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
    (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ))
  (f' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
Tactic: rw [this] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport g) ((L.symm : (a : E' × ℝ) → E) x : E)
hf :
  HasLineDerivAt ℝ
    (Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ))
    (f' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have h : x = ((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x)
Tactic: convert! hf.of_comp using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport g) ((L.symm : (a : E' × ℝ) → E) x : E)
hf :
  HasLineDerivAt ℝ
    (Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ))
    (f' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
h : x = ((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have h₁ : Eq (α := E' × ℝ) (0, 1) (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) v)
Tactic: convert! hf.of_comp using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
⊢ g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
have h : ∀ (y : E),
  g y =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have this₁ : g =
  Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
    (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
Tactic: have : g = (g ∘ L.symm) ∘ (L : E →ₗ[ℝ] (E' × ℝ)) := by ext y; simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have h2x : Membership.mem (α := E) (tsupport f) ((L.symm : (a : E' × ℝ) → E) x : E)
Tactic: have h2x : L.symm x ∈ tsupport f :=
      (Set.ext_iff.mp (tsupport_comp_eq_preimage f L.symm.toHomeomorph) x).mp hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport f) ((L.symm : (a : E' × ℝ) → E) x : E)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have hg₁ : HasLineDerivAt ℝ g (g' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
Tactic: specialize hg (L.symm x) h2x
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport f) ((L.symm : (a : E' × ℝ) → E) x : E)
hg : HasLineDerivAt ℝ g (g' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have hg₁ : HasLineDerivAt ℝ
  (Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
    (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ))
  (g' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
Tactic: rw [this] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport f) ((L.symm : (a : E' × ℝ) → E) x : E)
hg :
  HasLineDerivAt ℝ
    (Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ))
    (g' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have h : x = ((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x)
Tactic: convert! hg.of_comp using 1