awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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)
h₁ : Eq (α := E' × ℝ) (0, 1) (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) v)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)

Tactic:
convert! hf.of_comp using 1

Premises used: HasLineDerivAt.of_comp
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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
⊢ x = ((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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
⊢ Eq (α := E' × ℝ) (0, 1) (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) v)

Tactic:
simp [← hL]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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
h :
  ∀ (y : E),
    g y =
      Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
        (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) y
⊢ g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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
y : E
⊢ g y =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) y

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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' × ℝ)

Tactic:
have : g = (g ∘ L.symm) ∘ (L : E →ₗ[ℝ] (E' × ℝ)) := by ext y; simp
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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' × ℝ)
⊢ 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
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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 ℝ g (g' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v

Tactic:
specialize hg (L.symm x) h2x

Premises used: ContinuousLinearEquiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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 ℝ
    (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
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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 ℝ (E := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E) : E' × ℝ → G) (g' ((L.symm : (a : E' × ℝ) → E) x))
    (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x) : E' × ℝ)
    (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) v : E' × ℝ)

Tactic:
hg.of_comp

Premises used: HasLineDerivAt.of_comp
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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
h : x = ((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x)
h₁ : Eq (α := E' × ℝ) (0, 1) (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) v)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)

Tactic:
convert! hg.of_comp using 1

Premises used: HasLineDerivAt.of_comp
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
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
⊢ x = ((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x)

Tactic:
simp