awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
inr₁ : ∀ (hn : 0 < n), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)

Tactic:
rcases lt_trichotomy n 0 with hn | rfl | hn

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)

Tactic:
absurd ?_ hxy.not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
inl : y ≤ x
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)

Tactic:
refine absurd ?_ hxy.not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Algebra.AddConstMap.Basic
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

Tactic:
sub_le_iff_le_add.1 hny.2

Premises used: sub_le_iff_le_add, And.right, Iff.mp
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
rw₃ rw₄ : l + (a + n • a) = l + (a + n • a)
⊢ l + a + n • a = l + (n + 1) • a

Tactic:
rw [add_comm n, add_smul, one_smul, add_assoc]

Premises used: add_assoc, add_comm, one_smul, add_smul
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
bc : n + 1 ≤ 0
⊢ l + (n + 1) • a ≤ l + HSMul.hSMul (α := ℤ) 0 a

Tactic:
gcongr
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
⊢ n + 1 ≤ 0

Tactic:
lia
-- Module: Mathlib.Algebra.AddConstMap.Basic
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 + HSMul.hSMul (α := ℤ) 0 a ≤ x

Tactic:
simpa using hx.1

Premises used: And.left
-- Module: Mathlib.Algebra.AddConstMap.Basic
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₃ : l + HSMul.hSMul (α := ℤ) 0 a ≤ x
⊢ y ≤ 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

Premises used: sub_le_iff_le_add, And.right, HAdd.hAdd, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
hny : y - HSMul.hSMul (α := ℤ) 0 a ∈ Ioc l (l + a)
⊢ y ∈ Icc l (l + a)

Tactic:
simpa using Ioc_subset_Icc_self hny

Premises used: Set.Ioc_subset_Icc_self
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
hny : y - HSMul.hSMul (α := ℤ) 0 a ∈ Ioc l (l + a)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)

Tactic:
exact hf x (Ico_subset_Icc_self hx) y (by simpa using Ioc_subset_Icc_self hny) hxy

Premises used: Set.Ico_subset_Icc_self
-- Module: Mathlib.Algebra.AddConstMap.Basic
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))
trans₁ : R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)

Tactic:
trans f (l + (1 : ℤ) • a)

Premises used: HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.AddConstMap.Basic
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) (l + HSMul.hSMul (α := ℤ) 1 a))

Tactic:
grind
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
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))
⊢ R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)

Tactic:
rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]

Premises used: AddConstMapClass.map_add_zsmul, HSMul.hSMul, sub_add_cancel
-- Module: Mathlib.Algebra.AddConstMap.Basic
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))

Tactic:
hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1

Premises used: Set.Ioc_subset_Icc_self, And.left
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
refine : l ∈ Icc l (l + a)
⊢ 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:
refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1

Premises used: Set.Ioc_subset_Icc_self, And.left
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
⊢ l ∈ Icc l (l + a)

Tactic:
simpa
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
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)
⊢ 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
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
⊢ 1 ≤ n

Tactic:
rw [← Int.add_one_le_iff, zero_add] at hn

Premises used: Int.add_one_le_iff, zero_add
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
hn₁ : 1 ≤ n
⊢ R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)

Tactic:
rw [← Int.add_one_le_iff, zero_add] at hn

Premises used: Int.add_one_le_iff, zero_add
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
inr : ∀ (hn : 1 < n), 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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
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:
assumption
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
trans : R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) (l + n • a))
trans₁ : 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:
trans f (l + n • a)

Premises used: HAdd.hAdd, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Algebra.AddConstMap.Basic
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))

Tactic:
Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn

Premises used: Int.rel_of_forall_rel_succ_of_lt
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
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))
⊢ R ((f : (a : G) → H) (l + HSMul.hSMul (α := ℤ) 1 a)) ((f : (a : G) → H) (l + n • a))

Tactic:
refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn

Premises used: Int.rel_of_forall_rel_succ_of_lt
-- Module: Mathlib.Algebra.AddConstMap.Basic
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 : ℤ
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))
⊢ 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:
simp_rw [add_comm k 1, add_zsmul, ← add_assoc, one_zsmul, map_add_zsmul]

Premises used: add_assoc, AddConstMapClass.map_add_zsmul, add_zsmul, add_comm, one_zsmul, OfNat.ofNat
-- Module: Mathlib.Algebra.AddConstMap.Basic
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))

Tactic:
hR (k • b) (hf _ ?_ _ ?_ ?_)

Premises used: HSMul.hSMul
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
refine_3 : 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))

Tactic:
refine hR (k • b) (hf _ ?_ _ ?_ ?_)

Premises used: HSMul.hSMul
-- Module: Mathlib.Algebra.AddConstMap.Basic
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 : ℤ
⊢ l ∈ Icc l (l + a)

Tactic:
simpa