awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have trans : R ((f : (a : G) → H) x) ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a))
Tactic: trans f (l + (1 : ℤ) • a)
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
trans : R ((f : (a : G) → H) x) ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a))
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have trans₁ : R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
Tactic: trans f (l + (1 : ℤ) • a)
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
have rw : R (HAdd.hAdd (α := H) ((f : (a : G) → H) l : H) (n • b))
  (HAdd.hAdd (α := H) ((f : (a : G) → H) (y - n • a) : H) (n • b))
Tactic: rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (HAdd.hAdd (α := H) ((f : (a : G) → H) l : H) (n • b))
    (HAdd.hAdd (α := H) ((f : (a : G) → H) (y - n • a) : H) (n • b))
have refine : l ∈ Icc l (l + a)
Tactic: refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
have have : ∀ (hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)),
  R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
Tactic: have hy : R (f (l + n • a)) (f y) := by
        rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]
        refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1; simpa
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (hypothesis)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
have hn₁ : 1 ≤ n
Tactic: rw [← Int.add_one_le_iff, zero_add] at hn
Cleared hypotheses: hn, hy
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
have inl : ∀ (hny : y - HSMul.hSMul (α := ℤ) 1 a ∈ Ioc l (l + a)) (hn : LE.le (α := ℤ) 1 1)
  (hy : R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)),
  R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
Tactic: rcases hn.eq_or_lt with rfl | hn
Cleared hypotheses: n, hny, hn, hy
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
inl :
  ∀ (hny : y - HSMul.hSMul (α := ℤ) 1 a ∈ Ioc l (l + a)) (hn : LE.le (α := ℤ) 1 1)
    (hy : R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)),
    R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
have inr : ∀ (hn : 1 < n), R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
Tactic: rcases hn.eq_or_lt with rfl | hn
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
⊢ R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
have trans : R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) (l + n • a))
Tactic: trans f (l + n • a)
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
⊢ R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) (l + n • a))
have refine : ∀ (k : ℤ),
  R ((fun (x : ℤ) ↦ ((f : (a : G) → H) (l + x • a) : H)) k)
    ((fun (x : ℤ) ↦ ((f : (a : G) → H) (l + x • a) : H)) (k + 1))
Tactic: refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
k : ℤ
⊢ R ((fun (x : ℤ) ↦ ((f : (a : G) → H) (l + x • a) : H)) k)
    ((fun (x : ℤ) ↦ ((f : (a : G) → H) (l + x • a) : H)) (k + 1))
have simp_rw : R (HAdd.hAdd (α := H) ((f : (a : G) → H) l : H) (k • b)) (HAdd.hAdd (α := H) ((f : (a : G) → H) (l + a) : H) (k • b))
Tactic: simp_rw [add_comm k 1, add_zsmul, ← add_assoc, one_zsmul, map_add_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
k : ℤ
⊢ R (HAdd.hAdd (α := H) ((f : (a : G) → H) l : H) (k • b)) (HAdd.hAdd (α := H) ((f : (a : G) → H) (l + a) : H) (k • b))
have refine_1 : l ∈ Icc l (l + a)
Tactic: refine hR (k • b) (hf _ ?_ _ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
k : ℤ
refine_1 : l ∈ Icc l (l + a)
⊢ R (HAdd.hAdd (α := H) ((f : (a : G) → H) l : H) (k • b)) (HAdd.hAdd (α := H) ((f : (a : G) → H) (l + a) : H) (k • b))
have refine_2 : l + a ∈ Icc l (l + a)
Tactic: refine hR (k • b) (hf _ ?_ _ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
a : G
b : H
inst_1 : AddCommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedAddMonoid G
inst_4 : Archimedean G
inst_5 : AddGroup H
inst_6 : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst_7 : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
k : ℤ
refine_1 : l ∈ Icc l (l + a)
refine_2 : l + a ∈ Icc l (l + a)
⊢ R (HAdd.hAdd (α := H) ((f : (a : G) → H) l : H) (k • b)) (HAdd.hAdd (α := H) ((f : (a : G) → H) (l + a) : H) (k • b))
have refine_3 : l < l + a
Tactic: refine hR (k • b) (hf _ ?_ _ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
G : Type u_1
inst : AddMonoid G
a : G
⊢ HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) 1 : G) AddConstMap.id =
    1
have h : ∀ (x : G),
  Eq (α := G)
    ((HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) 1 : G)
            AddConstMap.id :
          (a : G) → G)
        x :
      G)
    ((1 : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
G : Type u_1
inst : AddMonoid G
a : G
x x_1 : Multiplicative G
⊢ HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) (x * x_1) : G)
      AddConstMap.id =
    HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) x : G)
        AddConstMap.id *
      HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) x_1 : G)
        AddConstMap.id
have h : ∀ (x_2 : G),
  Eq (α := G)
    ((HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) (x * x_1) : G)
            AddConstMap.id :
          (a : G) → G)
        x_2 :
      G)
    ((HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) x : G)
              AddConstMap.id *
            HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) x_1 : G)
              AddConstMap.id :
          (a : G) → G)
        x_2 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
inst_4 : AddGroup G
a : G
x : (↑(Ico 0 1) : Type u_1) → G
⊢ (fun (f : R →+c[1, a] G) (x : (↑(Ico 0 1) : Type u_1)) ↦ ((f : (a : R) → G) (↑x : R) : G))
      ((fun (f : (↑(Ico 0 1) : Type u_1) → G) ↦
          ({
              toFun := fun (x : R) ↦
                f (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ico 0 1) x) (Int.fract x) ⋯) + ⌊x⌋ • a,
              map_add_const' := ⋯ } :
            R →+c[1, a] G))
        x) =
    x
have h : ∀ (x_1 : (↑(Ico 0 1) : Type u_1)),
  (fun (f : R →+c[1, a] G) (x : (↑(Ico 0 1) : Type u_1)) ↦ ((f : (a : R) → G) (↑x : R) : G))
      ((fun (f : (↑(Ico 0 1) : Type u_1) → G) ↦
          ({
              toFun := fun (x : R) ↦
                f (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ico 0 1) x) (Int.fract x) sorry) + ⌊x⌋ • a,
              map_add_const' := sorry } :
            R →+c[1, a] G))
        x)
      x_1 =
    x x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.AddConstMap.Basic (goal)
Goal:
R : Type u_1
G : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorRing R
inst_4 : AddGroup G
a : G
f : R →+c[1, a] G
⊢ (fun (f : (↑(Ico 0 1) : Type u_1) → G) ↦
        ({
            toFun := fun (x : R) ↦
              f (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ico 0 1) x) (Int.fract x) ⋯) + ⌊x⌋ • a,
            map_add_const' := ⋯ } :
          R →+c[1, a] G))
      ((fun (f : R →+c[1, a] G) (x : (↑(Ico 0 1) : Type u_1)) ↦ ((f : (a : R) → G) (↑x : R) : G)) f) =
    f
have h : ∀ (x : R),
  Eq.{u_2 + 1} (α := G)
    (((fun (f : (↑(Ico 0 1) : Type u_1) → G) ↦
              ({
                  toFun := fun (x : R) ↦
                    f (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ico 0 1) x) (Int.fract x) sorry) +
                      ⌊x⌋ • a,
                  map_add_const' := sorry } :
                R →+c[1, a] G))
            ((fun (f : R →+c[1, a] G) (x : (↑(Ico 0 1) : Type u_1)) ↦ ((f : (a : R) → G) (↑x : R) : G)) f) :
          (a : R) → G)
        x :
      G)
    ((f : (a : R) → G) x : G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
⊢ VSub.vsub (P := Set P) {p} {p} = {0}
have rw : Eq (α := Set G) {p -ᵥ p} {0}
Tactic: rw [Set.singleton_vsub_singleton, vsub_self]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
rw : Eq (α := Set G) {p -ᵥ p} {0}
⊢ VSub.vsub (P := Set P) {p} {p} = {0}
have rw₁ : Eq (α := Set G) {0} {0}
Tactic: rw [Set.singleton_vsub_singleton, vsub_self]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p₁ -ᵥ p = p₂ -ᵥ p
⊢ p₁ = p₂
have rwa : ∀ (h : p₁ -ᵥ p - (p₂ -ᵥ p) = 0), p₁ = p₂
Tactic: rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p₁ -ᵥ p = p₂ -ᵥ p
rwa : ∀ (h : p₁ -ᵥ p - (p₂ -ᵥ p) = 0), p₁ = p₂
⊢ p₁ = p₂
have rwa₁ : ∀ (h : p₁ -ᵥ p₂ = 0), p₁ = p₂
Tactic: rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p₁ -ᵥ p = p₂ -ᵥ p
rwa : ∀ (h : p₁ -ᵥ p - (p₂ -ᵥ p) = 0), p₁ = p₂
rwa₁ : ∀ (h : p₁ -ᵥ p₂ = 0), p₁ = p₂
⊢ p₁ = p₂
have rwa₂ : ∀ (h : p₁ = p₂), p₁ = p₂
Tactic: rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p -ᵥ p₁ = p -ᵥ p₂
⊢ p₁ = p₂
have refine : (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂
Tactic: refine vadd_left_cancel (p -ᵥ p₂) ?_
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p -ᵥ p₁ = p -ᵥ p₂
⊢ (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂
have rw : (p -ᵥ p₂) +ᵥ p₁ = p
Tactic: rw [vsub_vadd, ← h, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p -ᵥ p₁ = p -ᵥ p₂
rw : (p -ᵥ p₂) +ᵥ p₁ = p
⊢ (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂
have rw₁ : (p -ᵥ p₁) +ᵥ p₁ = p
Tactic: rw [vsub_vadd, ← h, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p -ᵥ p₁ = p -ᵥ p₂
rw : (p -ᵥ p₂) +ᵥ p₁ = p
rw₁ : (p -ᵥ p₁) +ᵥ p₁ = p
⊢ (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂
have rw₂ : p = p
Tactic: rw [vsub_vadd, ← h, vsub_vadd]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
have rw : p₃ -ᵥ p₂ + -(p₃ -ᵥ p₁) = p₁ -ᵥ p₂
Tactic: rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ : P
rw : p₃ -ᵥ p₂ + -(p₃ -ᵥ p₁) = p₁ -ᵥ p₂
⊢ p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
have rw₁ : p₃ -ᵥ p₂ + (p₁ -ᵥ p₃) = p₁ -ᵥ p₂
Tactic: rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ : P
rw : p₃ -ᵥ p₂ + -(p₃ -ᵥ p₁) = p₁ -ᵥ p₂
rw₁ : p₃ -ᵥ p₂ + (p₁ -ᵥ p₃) = p₁ -ᵥ p₂
⊢ p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
have rw₂ : p₁ -ᵥ p₃ + (p₃ -ᵥ p₂) = p₁ -ᵥ p₂
Tactic: rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ : P
rw : p₃ -ᵥ p₂ + -(p₃ -ᵥ p₁) = p₁ -ᵥ p₂
rw₁ : p₃ -ᵥ p₂ + (p₁ -ᵥ p₃) = p₁ -ᵥ p₂
rw₂ : p₁ -ᵥ p₃ + (p₃ -ᵥ p₂) = p₁ -ᵥ p₂
⊢ p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
have rw₃ : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
Tactic: rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v : G
p₁ p₂ : P
⊢ (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂
have rw : (v +ᵥ p₁) -ᵥ p₂ - v = p₁ -ᵥ p₂
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v : G
p₁ p₂ : P
rw : (v +ᵥ p₁) -ᵥ p₂ - v = p₁ -ᵥ p₂
⊢ (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂
have rw₁ : v + (p₁ -ᵥ p₂) - v = p₁ -ᵥ p₂
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v : G
p₁ p₂ : P
rw : (v +ᵥ p₁) -ᵥ p₂ - v = p₁ -ᵥ p₂
rw₁ : v + (p₁ -ᵥ p₂) - v = p₁ -ᵥ p₂
⊢ (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂
have rw₂ : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
have rw : (v₁ +ᵥ p₁) -ᵥ p₂ - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_assoc, ← add_comm_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
⊢ (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
have rw₁ : v₁ + (p₁ -ᵥ p₂) - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_assoc, ← add_comm_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
rw₁ : v₁ + (p₁ -ᵥ p₂) - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
⊢ (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
have rw₂ : v₁ + (p₁ -ᵥ p₂ - v₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_assoc, ← add_comm_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
rw : (v₁ +ᵥ p₁) -ᵥ p₂ - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
rw₁ : v₁ + (p₁ -ᵥ p₂) - v₂ = v₁ - v₂ + (p₁ -ᵥ p₂)
rw₂ : v₁ + (p₁ -ᵥ p₂ - v₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
⊢ (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
have rw₃ : v₁ - v₂ + (p₁ -ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
Tactic: rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_assoc, ← add_comm_sub]
-- Lean 4 proof step from Mathlib.Algebra.AddTorsor.Basic (goal)
Goal:
G : Type u_1
P : Type u_2
inst : AddCommGroup G
inst_1 : AddTorsor G P
p₁ p₂ p₃ : P
⊢ (p₁ -ᵥ p₂) +ᵥ p₃ = (p₃ -ᵥ p₂) +ᵥ p₁
have rw : p₁ -ᵥ p₂ + (p₃ -ᵥ p₁ - (p₃ -ᵥ p₂)) = 0
Tactic: rw [← @vsub_eq_zero_iff_eq G, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub]