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)) μ
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' × ℝ) μ
⊢ MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)

Tactic:
have L_emb : MeasurableEmbedding L := L.toHomeomorph.measurableEmbedding
-- 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' × ℝ)
pos :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₁ :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₂ :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₃ :
  ∀ (x : E' × ℝ),
    Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x))
        x →
      HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x
        (0, 1)
pos₄ :
  ∀ (x : E' × ℝ),
    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)
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)

Tactic:
apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2

Premises used: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
-- 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' × ℝ)
⊢ Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν

Tactic:
simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hf'g

Premises used: MeasurableEmbedding.integrable_map_iff, Function.comp_def
-- 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' × ℝ)
⊢ Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)))
    ν

Tactic:
simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hfg'

Premises used: MeasurableEmbedding.integrable_map_iff, Function.comp_def
-- 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' × ℝ)
⊢ Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν

Tactic:
simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hfg

Premises used: MeasurableEmbedding.integrable_map_iff, Function.comp_def
-- 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_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
h :
  ∀ (y : E),
    f y =
      Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
        (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) y
⊢ f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑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_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
y : E
⊢ f y =
    Function.comp (β := E' × ℝ) (f ∘ (⇑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_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
⊢ f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)

Tactic:
have : f = (f ∘ 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_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' × ℝ)
⊢ 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
-- 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_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 ℝ f (f' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v

Tactic:
specialize hf (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)) μ
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 ℝ
    (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
-- 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
⊢ HasLineDerivAt ℝ (E := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E) : E' × ℝ → F) (f' ((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:
hf.of_comp

Premises used: HasLineDerivAt.of_comp