awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
rw :
  HSub.hSub (α := W) (β := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
      ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) =
    0
rw₁ :
  Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
    ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) (0 : W)
have rw₂ : Eq.{u_2 + 1} (α := W) ((f.comp φ : (a : V₁) → W) v : W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
Tactic: rw [NormedAddGroupHom.sub_apply, sub_eq_zero, ← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
rw :
  HSub.hSub (α := W) (β := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
      ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) =
    0
rw₁ :
  Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
    ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
rw₂ : Eq.{u_2 + 1} (α := W) ((f.comp φ : (a : V₁) → W) v : W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) (0 : W)
have rw₃ : Eq.{u_2 + 1} (α := W) ((g.comp φ : (a : V₁) → W) v : W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
Tactic: rw [NormedAddGroupHom.sub_apply, sub_eq_zero, ← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
rw :
  HSub.hSub (α := W) (β := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
      ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) =
    0
rw₁ :
  Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
    ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
rw₂ : Eq.{u_2 + 1} (α := W) ((f.comp φ : (a : V₁) → W) v : W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
rw₃ : Eq.{u_2 + 1} (α := W) ((g.comp φ : (a : V₁) → W) v : W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) (0 : W)
have rw₄ : Eq.{u_2 + 1} (α := W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
  ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
Tactic: rw [NormedAddGroupHom.sub_apply, sub_eq_zero, ← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v₁ v₂ : V₁
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) (v₁ + v₂)) ⋯ =
    HAdd.hAdd (α := ↥(f.equalizer g)) (β := ↥(f.equalizer g))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₁) ⋯ : ↥(f.equalizer g))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₂) ⋯ : ↥(f.equalizer g))
have a : (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) (v₁ + v₂)) sorry) : V) =
  (↑(HAdd.hAdd (α := ↥(f.equalizer g)) (β := ↥(f.equalizer g))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₁) sorry : ↥(f.equalizer g))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₂) sorry : ↥(f.equalizer g))) :
    V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
⊢ ∃ (C : ℝ),
    ∀ (v : V₁),
      norm.{u_1} (E := ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v) ⋯ : ↥(f.equalizer g)) ≤
        C * ‖v‖
have obtain : ∀ (C : ℝ) (_C_pos : 0 < C) (hC : ∀ (x : V₁), norm.{u_1} (E := V) ((φ : (a : V₁) → V) x : V) ≤ C * ‖x‖),
  ∃ (C : ℝ),
    ∀ (v : V₁),
      norm.{u_1} (E := ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v) sorry : ↥(f.equalizer g)) ≤
        C * ‖v‖
Tactic: obtain ⟨C, _C_pos, hC⟩ := φ.bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
⊢ (ι f g).comp (lift φ h) = φ
have H : ∀ (x : V₁), Eq.{u_1 + 1} (α := V) (((ι f g).comp (lift φ h) : (a : V₁) → V) x : V) ((φ : (a : V₁) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
ψ : NormedAddGroupHom.{u_3, u_1} V₁ ↥(f.equalizer g)
⊢ f.comp ((ι f g).comp ψ) = g.comp ((ι f g).comp ψ)
have rw : (f.comp (ι f g)).comp ψ = g.comp ((ι f g).comp ψ)
Tactic: rw [← comp_assoc, ← comp_assoc, comp_ι_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
ψ : NormedAddGroupHom.{u_3, u_1} V₁ ↥(f.equalizer g)
rw : (f.comp (ι f g)).comp ψ = g.comp ((ι f g).comp ψ)
⊢ f.comp ((ι f g).comp ψ) = g.comp ((ι f g).comp ψ)
have rw₁ : (f.comp (ι f g)).comp ψ = (g.comp (ι f g)).comp ψ
Tactic: rw [← comp_assoc, ← comp_assoc, comp_ι_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
ψ : NormedAddGroupHom.{u_3, u_1} V₁ ↥(f.equalizer g)
rw : (f.comp (ι f g)).comp ψ = g.comp ((ι f g).comp ψ)
rw₁ : (f.comp (ι f g)).comp ψ = (g.comp (ι f g)).comp ψ
⊢ f.comp ((ι f g).comp ψ) = g.comp ((ι f g).comp ψ)
have rw₂ : (g.comp (ι f g)).comp ψ = (g.comp (ι f g)).comp ψ
Tactic: rw [← comp_assoc, ← comp_assoc, comp_ι_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ f₂.comp (φ.comp (ι f₁ g₁)) = g₂.comp (φ.comp (ι f₁ g₁))
have simp : (ψ.comp f₁).comp (ι f₁ g₁) = (ψ.comp g₁).comp (ι f₁ g₁)
Tactic: simp only [← comp_assoc, ← hf, ← hg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst_1 : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
⊢ Eq (α := NormedAddGroupHom ↥(f₁.equalizer g₁) ↥(f₁.equalizer g₁)) (map (id V₁) (id W₁) ⋯ ⋯) (id ↥(f₁.equalizer g₁))
have H : ∀ (x : ↥(f₁.equalizer g₁)),
  Eq.{u_3 + 1} (α := V₁) (↑((map (id V₁) (id W₁) sorry sorry : (a : ↥(f₁.equalizer g₁)) → ↥(f₁.equalizer g₁)) x) : V₁)
    (↑((id ↥(f₁.equalizer g₁) : (a : ↥(f₁.equalizer g₁)) → ↥(f₁.equalizer g₁)) x) : V₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
have rw : ψ'.comp (ψ.comp f₁) = f₃.comp (φ'.comp φ)
Tactic: rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
rw : ψ'.comp (ψ.comp f₁) = f₃.comp (φ'.comp φ)
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
have rw₁ : ψ'.comp (f₂.comp φ) = f₃.comp (φ'.comp φ)
Tactic: rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
rw : ψ'.comp (ψ.comp f₁) = f₃.comp (φ'.comp φ)
rw₁ : ψ'.comp (f₂.comp φ) = f₃.comp (φ'.comp φ)
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
have rw₂ : (ψ'.comp f₂).comp φ = f₃.comp (φ'.comp φ)
Tactic: rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
rw : ψ'.comp (ψ.comp f₁) = f₃.comp (φ'.comp φ)
rw₁ : ψ'.comp (f₂.comp φ) = f₃.comp (φ'.comp φ)
rw₂ : (ψ'.comp f₂).comp φ = f₃.comp (φ'.comp φ)
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
have rw₃ : (f₃.comp φ').comp φ = f₃.comp (φ'.comp φ)
Tactic: rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
rw : ψ'.comp (ψ.comp f₁) = f₃.comp (φ'.comp φ)
rw₁ : ψ'.comp (f₂.comp φ) = f₃.comp (φ'.comp φ)
rw₂ : (ψ'.comp f₂).comp φ = f₃.comp (φ'.comp φ)
rw₃ : (f₃.comp φ').comp φ = f₃.comp (φ'.comp φ)
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
have rw₄ : f₃.comp (φ'.comp φ) = f₃.comp (φ'.comp φ)
Tactic: rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Hom (goal)
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
⊢ (map φ' ψ' hf' hg').comp (map φ ψ hf hg) = map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯
have H : ∀ (x : ↥(f₁.equalizer g₁)),
  Eq.{u_5 + 1} (α := V₃)
    (↑(((map φ' ψ' hf' hg').comp (map φ ψ hf hg) : (a : ↥(f₁.equalizer g₁)) → ↥(f₃.equalizer g₃)) x) : V₃)
    (↑((map (φ'.comp φ) (ψ'.comp ψ) sorry sorry : (a : ↥(f₁.equalizer g₁)) → ↥(f₃.equalizer g₃)) x) : V₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Rat (goal)
Goal:
r₁ r₂ : ℚ
⊢ dist r₁ r₂ = norm (E := ℝ) (↑(-r₁ + r₂) : ℝ)
have simp : |HSub.hSub (α := ℝ) (↑r₁ : ℝ) (↑r₂ : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑r₁ : ℝ)) (↑r₂ : ℝ)|
Tactic: simp only [dist_eq, norm, cast_add, cast_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Rat (goal)
Goal:
r₁ r₂ : ℚ
⊢ |HSub.hSub (α := ℝ) (↑r₁ : ℝ) (↑r₂ : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑r₁ : ℝ)) (↑r₂ : ℝ)|
have rw : |HSub.hSub (α := ℝ) (↑r₂ : ℝ) (↑r₁ : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑r₁ : ℝ)) (↑r₂ : ℝ)|
Tactic: rw [← abs_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ t ^ p * (t⁻¹ - (t + x)⁻¹)) fun (x : ℝ) ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹
have h : ∀ (x : ℝ), t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ (p - 1) - t ^ p * (t + x)⁻¹
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ (p - 1) - t ^ p * (t + x)⁻¹
have h : t ^ (p + -1) - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹
Tactic: rw [mul_sub, ← rpow_neg_one, ← rpow_add' (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)
have inr : 0 ≤ t⁻¹ - (t + x)⁻¹
Tactic: refine mul_nonneg (by positivity) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ 0 ≤ t⁻¹ - (t + x)⁻¹
have inr : (t + x)⁻¹ ≤ t⁻¹
Tactic: rw [sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ (t + x)⁻¹ ≤ t⁻¹
have inr : t ≤ t + x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ t ≤ t + x
have linarith : t + x < t → 0 - x + (t + x - t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)
have x₁ : t = 0 ∨ 0 < t
Tactic: cases eq_or_lt_of_le' ht with
  | inl ht_zero => simp [ht_zero, Real.zero_rpow (ne_of_gt hp)]
  | inr ht_pos =>
    refine mul_nonneg (by positivity) ?_
    rw [sub_nonneg]
    gcongr
    linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have by_cases : ∀ (ht' : t = 0), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Tactic: by_cases ht' : t = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
by_cases : ∀ (ht' : t = 0), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have by_cases₁ : ∀ (ht' : ¬t = 0), p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
Tactic: by_cases ht' : t = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have hxt : t + x ≠ 0
Tactic: have hxt : t + x ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))
have simp : t ^ p * (1 / t - 1 / (t + x)) = t ^ p * ((t + x - t) / (t * (t + x)))
Tactic: simp only [inv_eq_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (1 / t - 1 / (t + x)) = t ^ p * ((t + x - t) / (t * (t + x)))
have rw : t ^ p * ((1 * (t + x) - t * 1) / (t * (t + x))) = t ^ p * ((t + x - t) / (t * (t + x)))
Tactic: rw [div_sub_div _ _ (by lia) (by lia)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p / t * x / (t + x) = t ^ (p - 1) * x / (t + x)
have e_a : t ^ p / t = t ^ (p - 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have calc : t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))
Tactic: calc _ = (t : ℝ) ^ p * (t⁻¹ - (t + x)⁻¹) := rfl
      _ = (t : ℝ) ^ p * ((t + x - t) / (t * (t + x))) := by
          simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp
      _ = t ^ p / t * x / (t + x) := by simp [field]
      _ = t ^ (p - 1) * x / (t + x) := by congr; exact (Real.rpow_sub_one ht' p).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
calc : t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have calc₁ : t ^ p * ((t + x - t) / (t * (t + x))) = t ^ p / t * x / (t + x)
Tactic: calc _ = (t : ℝ) ^ p * (t⁻¹ - (t + x)⁻¹) := rfl
      _ = (t : ℝ) ^ p * ((t + x - t) / (t * (t + x))) := by
          simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp
      _ = t ^ p / t * x / (t + x) := by simp [field]
      _ = t ^ (p - 1) * x / (t + x) := by congr; exact (Real.rpow_sub_one ht' p).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
p t x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
calc : t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))
calc₁ : t ^ p * ((t + x - t) / (t * (t + x))) = t ^ p / t * x / (t + x)
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
have calc₂ : t ^ p / t * x / (t + x) = t ^ (p - 1) * x / (t + x)
Tactic: calc _ = (t : ℝ) ^ p * (t⁻¹ - (t + x)⁻¹) := rfl
      _ = (t : ℝ) ^ p * ((t + x - t) / (t * (t + x))) := by
          simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp
      _ = t ^ p / t * x / (t + x) := by simp [field]
      _ = t ^ (p - 1) * x / (t + x) := by congr; exact (Real.rpow_sub_one ht' p).symm