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 : AddCommMagma G
inst_2 : Add H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
⊢ (f : (a : G) → H) (a + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b
have rw : (f : (a : G) → H) (x + a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b
Tactic: rw [add_comm, map_add_const]
-- 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 : AddCommMagma G
inst_2 : Add H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
rw : (f : (a : G) → H) (x + a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b
⊢ (f : (a : G) → H) (a + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b
have rw₁ : HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b
Tactic: rw [add_comm, map_add_const]
-- 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 : AddCommMonoid G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H a b
f : F
n : ℕ
x : G
⊢ (f : (a : G) → H) (n • a + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw : (f : (a : G) → H) (x + n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
Tactic: rw [add_comm, map_add_nsmul]
-- 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 : AddCommMonoid G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H a b
f : F
n : ℕ
x : G
rw : (f : (a : G) → H) (x + n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
⊢ (f : (a : G) → H) (n • a + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw₁ : HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
Tactic: rw [add_comm, map_add_nsmul]
-- 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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
| HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw : ((f : (a : G) → H) (x - n • a) : H)
Tactic: rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]
-- 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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ (f : (a : G) → H) (x - n • a) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)
have conv_rhs : (f : (a : G) → H) (x - n • a) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)
Tactic: conv_rhs => rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]
-- 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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
conv_rhs : (f : (a : G) → H) (x - n • a) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)
⊢ (f : (a : G) → H) (x - n • a) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)
have conv_rhs₁ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x - n • a) : H) ((f : (a : G) → H) (x - n • a) : H)
Tactic: conv_rhs => rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]
-- 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
b : H
inst_1 : AddGroupWithOne G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ (f : (a : G) → H) (x + (↑n : G)) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x + (↑n : G)) : H) ((f : (a : G) → H) (x + HSMul.hSMul (β := G) n 1) : H)
Tactic: rw [← map_add_zsmul f x n, zsmul_one]
-- 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
b : H
inst_1 : AddGroupWithOne G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
rw : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x + (↑n : G)) : H) ((f : (a : G) → H) (x + HSMul.hSMul (β := G) n 1) : H)
⊢ (f : (a : G) → H) (x + (↑n : G)) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw₁ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x + (↑n : G)) : H) ((f : (a : G) → H) (x + (↑n : G)) : H)
Tactic: rw [← map_add_zsmul f x n, zsmul_one]
-- 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
b : H
inst_1 : AddGroupWithOne G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ (f : (a : G) → H) (x - (↑n : G)) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x - (↑n : G)) : H) ((f : (a : G) → H) (x - HSMul.hSMul (β := G) n 1) : H)
Tactic: rw [← map_sub_zsmul, zsmul_one]
-- 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
b : H
inst_1 : AddGroupWithOne G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
rw : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x - (↑n : G)) : H) ((f : (a : G) → H) (x - HSMul.hSMul (β := G) n 1) : H)
⊢ (f : (a : G) → H) (x - (↑n : G)) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw₁ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x - (↑n : G)) : H) ((f : (a : G) → H) (x - (↑n : G)) : H)
Tactic: rw [← map_sub_zsmul, zsmul_one]
-- 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 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
n : ℤ
x : G
⊢ (f : (a : G) → H) (n • a + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw : (f : (a : G) → H) (x + n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
Tactic: rw [add_comm, 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 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
n : ℤ
x : G
rw : (f : (a : G) → H) (x + n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
⊢ (f : (a : G) → H) (n • a + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw₁ : HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
Tactic: rw [add_comm, 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
b : H
inst_1 : AddCommGroupWithOne G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H 1 b
f : F
n : ℤ
x : G
⊢ (f : (a : G) → H) ((↑n : G) + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) ((↑n : G) + x) : H) ((f : (a : G) → H) (HSMul.hSMul (β := G) n 1 + x) : H)
Tactic: rw [← map_zsmul_add, zsmul_one]
-- 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
b : H
inst_1 : AddCommGroupWithOne G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H 1 b
f : F
n : ℤ
x : G
rw : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) ((↑n : G) + x) : H) ((f : (a : G) → H) (HSMul.hSMul (β := G) n 1 + x) : H)
⊢ (f : (a : G) → H) ((↑n : G) + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)
have rw₁ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) ((↑n : G) + x) : H) ((f : (a : G) → H) ((↑n : G) + x) : H)
Tactic: rw [← map_zsmul_add, zsmul_one]
-- 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
hR : CovariantClass H H (fun (x y : H) ↦ y + x) 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)
x y : G
hxy : (fun (x1 x2 : G) ↦ x1 < x2) x y
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have replace : ∀ (hR : Covariant H H (fun (x y : H) ↦ y + x) R), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: replace hR := hR.elim
Cleared hypotheses: hR
-- 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)
x y : G
hxy : (fun (x1 x2 : G) ↦ x1 < x2) x y
hR : Covariant H H (fun (x y : H) ↦ y + x) R
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have ha' : 0 ≤ a
Tactic: have ha' : 0 ≤ a := ha.le
-- 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)
x y : G
hxy : (fun (x1 x2 : G) ↦ x1 < x2) x y
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have inr : ∀ (this : ∀ (x y : G) (hxy : x < y) (hx : x ∈ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y))
  (hx : x ∉ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: wlog hx : x ∈ Ico l (l + a) generalizing x y
-- 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)
x y : G
hxy : (fun (x1 x2 : G) ↦ x1 < x2) x y
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
inr :
  ∀ (this : ∀ (x y : G) (hxy : x < y) (hx : x ∈ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y))
    (hx : x ∉ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have wlog : ∀ (x y : G) (hxy : x < y) (hx : x ∈ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: wlog hx : x ∈ Ico l (l + a) generalizing x y
Cleared hypotheses: x, y, hxy
-- 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)
x y : G
hxy : (fun (x1 x2 : G) ↦ x1 < x2) x y
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G) (hxy : x < y) (hx : x ∈ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hx : x ∉ Ico l (l + a)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have inr : ∀ (m : ℤ) (hm : x - m • a ∈ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: rcases existsUnique_sub_zsmul_mem_Ico ha x l with ⟨m, hm, -⟩
-- 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)
x y : G
hxy : (fun (x1 x2 : G) ↦ x1 < x2) x y
hR : Covariant H H (fun (x y : H) ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G) (hxy : x < y) (hx : x ∈ Ico l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have inr : R ((f : (a : G) → H) (x - m • a)) ((f : (a : G) → H) (y - m • a))
Tactic: suffices R (f (x - m • a)) (f (y - m • a)) by simpa using hR (m • b) this
-- 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)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have rcases : ∀ (n : ℤ) (hny : y - n • a ∈ Ioc l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: rcases existsUnique_sub_zsmul_mem_Ioc ha y l with ⟨n, hny, -⟩
-- 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)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have inl : ∀ (hn : n < 0), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: rcases lt_trichotomy n 0 with hn | 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)
inl : ∀ (hn : n < 0), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have inr : ∀ (hny : y - HSMul.hSMul (α := ℤ) 0 a ∈ Ioc l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: rcases lt_trichotomy n 0 with hn | rfl | hn
Cleared hypotheses: n, hny
-- 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)
inl : ∀ (hn : n < 0), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
inr : ∀ (hny : y - HSMul.hSMul (α := ℤ) 0 a ∈ Ioc l (l + a)), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have inr₁ : ∀ (hn : 0 < n), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
Tactic: rcases lt_trichotomy n 0 with hn | 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 : n < 0
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
have inl : y ≤ x
Tactic: refine absurd ?_ hxy.not_ge
-- 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 : n < 0
⊢ l + a + n • a = l + (n + 1) • a
have rw : l + a + n • a = l + (1 + n) • a
Tactic: rw [add_comm n, add_smul, one_smul, add_assoc]
-- 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 : n < 0
rw : l + a + n • a = l + (1 + n) • a
⊢ l + a + n • a = l + (n + 1) • a
have rw₁ : l + a + n • a = l + (HSMul.hSMul (α := ℤ) 1 a + n • a)
Tactic: rw [add_comm n, add_smul, one_smul, add_assoc]
-- 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 : n < 0
rw : l + a + n • a = l + (1 + n) • a
rw₁ : l + a + n • a = l + (HSMul.hSMul (α := ℤ) 1 a + n • a)
⊢ l + a + n • a = l + (n + 1) • a
have rw₂ : l + a + n • a = l + (a + n • a)
Tactic: rw [add_comm n, add_smul, one_smul, add_assoc]
-- 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 : n < 0
rw : l + a + n • a = l + (1 + n) • a
rw₁ : l + a + n • a = l + (HSMul.hSMul (α := ℤ) 1 a + n • a)
rw₂ : l + a + n • a = l + (a + n • a)
⊢ l + a + n • a = l + (n + 1) • a
have rw₃ : l + (a + n • a) = l + (a + n • a)
Tactic: rw [add_comm n, add_smul, one_smul, add_assoc]
-- 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 : n < 0
⊢ l + (n + 1) • a ≤ l + HSMul.hSMul (α := ℤ) 0 a
have bc : n + 1 ≤ 0
Tactic: gcongr
-- 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 : n < 0
⊢ y ≤ x
have y₁ : l + a + n • a = l + (n + 1) • a
Tactic: calc
        y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
        _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
        _ ≤ l + (0 : ℤ) • a := by gcongr; lia
        _ ≤ x := by simpa using hx.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 : n < 0
y₁ : l + a + n • a = l + (n + 1) • a
⊢ y ≤ x
have y₂ : l + (n + 1) • a ≤ l + HSMul.hSMul (α := ℤ) 0 a
Tactic: calc
        y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
        _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
        _ ≤ l + (0 : ℤ) • a := by gcongr; lia
        _ ≤ x := by simpa using hx.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 : n < 0
y₁ : l + a + n • a = l + (n + 1) • a
y₂ : l + (n + 1) • a ≤ l + HSMul.hSMul (α := ℤ) 0 a
⊢ y ≤ x
have y₃ : l + HSMul.hSMul (α := ℤ) 0 a ≤ x
Tactic: calc
        y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
        _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
        _ ≤ l + (0 : ℤ) • a := by gcongr; lia
        _ ≤ x := by simpa using hx.1