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 : Add G
inst_2 : Add H
inst_3 : AddConstMapClass F G H a b
f : F
⊢ Semiconj (⇑f : (a : G) → H) (fun (x : G) ↦ x + a) fun (x : H) ↦ x + b

Tactic:
map_add_const f

Premises used: AddConstMapClass.map_add_const, Function.Semiconj
-- 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 : AddMonoid G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ (f : (a : G) → H) (x + n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)

Tactic:
simpa using (AddConstMapClass.semiconj f).iterate_right n x

Premises used: AddConstMapClass.semiconj, Function.Semiconj.iterate_right
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
b : H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoid 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)

Tactic:
simp [← map_add_nsmul]

Premises used: AddConstMapClass.map_add_nsmul
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
b : H
inst_1 : AddMonoidWithOne G
inst_2 : Add H
inst_3 : AddConstMapClass F G H 1 b
f : F
x : G
⊢ (f : (a : G) → H) (x + 1) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b

Tactic:
map_add_const f x

Premises used: AddConstMapClass.map_add_const
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
b : H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
inst_4 : n.AtLeastTwo
⊢ (f : (a : G) → H) (x + OfNat.ofNat n) =
    HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (HSMul.hSMul (α := ℕ) (OfNat.ofNat n) b)

Tactic:
map_add_nat' f x n

Premises used: AddConstMapClass.map_add_nat'
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoidWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
x : G
n : ℕ
⊢ (f : (a : G) → H) (x + (↑n : G)) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) x : H) ((↑n : H) : H)

Tactic:
simp
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoidWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
x : G
n : ℕ
inst_4 : n.AtLeastTwo
⊢ (f : (a : G) → H) (x + OfNat.ofNat n) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) x : H) (OfNat.ofNat n : H)

Tactic:
map_add_nat f x n

Premises used: AddConstMapClass.map_add_nat
-- 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 : AddZeroClass G
inst_2 : Add H
inst_3 : AddConstMapClass F G H a b
f : F
⊢ (f : (a : G) → H) a = HAdd.hAdd (α := H) ((f : (a : G) → H) 0 : H) b

Tactic:
simpa using map_add_const f 0

Premises used: AddConstMapClass.map_add_const, 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
b : H
inst_1 : AddZeroClass G
inst_2 : One G
inst_3 : Add H
inst_4 : AddConstMapClass F G H 1 b
f : F
⊢ (f : (a : G) → H) 1 = HAdd.hAdd (α := H) ((f : (a : G) → H) 0 : H) b

Tactic:
map_const f

Premises used: AddConstMapClass.map_const
-- 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 : AddMonoid G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H a b
f : F
n : ℕ
⊢ (f : (a : G) → H) (n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) 0 : H) (n • b)

Tactic:
simpa using map_add_nsmul f 0 n

Premises used: AddConstMapClass.map_add_nsmul, 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
b : H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H 1 b
f : F
n : ℕ
⊢ (f : (a : G) → H) (↑n : G) = HAdd.hAdd (α := H) ((f : (a : G) → H) 0 : H) (n • b)

Tactic:
simpa using map_add_nat' f 0 n

Premises used: AddConstMapClass.map_add_nat', 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
b : H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H 1 b
f : F
n : ℕ
inst_4 : n.AtLeastTwo
⊢ (f : (a : G) → H) (OfNat.ofNat n) =
    HAdd.hAdd (α := H) ((f : (a : G) → H) 0 : H) (HSMul.hSMul (α := ℕ) (OfNat.ofNat n) b)

Tactic:
map_nat' f n

Premises used: AddConstMapClass.map_nat'
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoidWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
n : ℕ
⊢ (f : (a : G) → H) (↑n : G) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) 0 : H) ((↑n : H) : H)

Tactic:
simp
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddMonoidWithOne G
inst_2 : AddMonoidWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
n : ℕ
inst_4 : n.AtLeastTwo
⊢ (f : (a : G) → H) (OfNat.ofNat n) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) 0 : H) (OfNat.ofNat n : H)

Tactic:
map_nat f n

Premises used: AddConstMapClass.map_nat
-- 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 : 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
rw₁ rw₂ : HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b = 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

Tactic:
rw [add_comm, map_add_const]

Premises used: AddConstMapClass.map_add_const, add_comm
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
b : H
inst_1 : AddCommMonoidWithOne G
inst_2 : Add H
inst_3 : AddConstMapClass F G H 1 b
f : F
x : G
⊢ (f : (a : G) → H) (1 + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) b

Tactic:
map_const_add f x

Premises used: AddConstMapClass.map_const_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 : 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)
rw₁ rw₂ : HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b) = 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)

Tactic:
rw [add_comm, map_add_nsmul]

Premises used: AddConstMapClass.map_add_nsmul, add_comm
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
b : H
inst_1 : AddCommMonoidWithOne G
inst_2 : AddMonoid 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)

Tactic:
simpa using map_nsmul_add f n x

Premises used: AddConstMapClass.map_nsmul_add
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
b : H
inst_1 : AddCommMonoidWithOne G
inst_2 : AddMonoid H
inst_3 : AddConstMapClass F G H 1 b
f : F
n : ℕ
inst_4 : n.AtLeastTwo
x : G
⊢ (f : (a : G) → H) (OfNat.ofNat n + x) =
    HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (HSMul.hSMul (α := ℕ) (OfNat.ofNat n) b)

Tactic:
map_nat_add' f n x

Premises used: AddConstMapClass.map_nat_add'
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddCommMonoidWithOne G
inst_2 : AddMonoidWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
n : ℕ
x : G
⊢ (f : (a : G) → H) ((↑n : G) + x) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) x : H) ((↑n : H) : H)

Tactic:
simp
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddCommMonoidWithOne G
inst_2 : AddMonoidWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
n : ℕ
inst_4 : n.AtLeastTwo
x : G
⊢ (f : (a : G) → H) (OfNat.ofNat n + x) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) x : H) (OfNat.ofNat n : H)

Tactic:
map_nat_add f n x

Premises used: AddConstMapClass.map_nat_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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
rw : ((f : (a : G) → H) (x - n • a) : H)
| HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)

Tactic:
rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]

Premises used: AddConstMapClass.map_add_nsmul, HSMul.hSMul, add_sub_cancel_right, 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 : 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)
conv_rhs₁ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x - n • a) : H) ((f : (a : G) → H) (x - n • a) : H)
⊢ (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]

Premises used: AddConstMapClass.map_add_nsmul, HSMul.hSMul, add_sub_cancel_right, 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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
⊢ (f : (a : G) → H) (x - a) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) b

Tactic:
simpa using map_sub_nsmul f x 1

Premises used: AddConstMapClass.map_sub_nsmul, 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
b : H
inst_1 : AddGroup G
inst_2 : One G
inst_3 : AddGroup H
inst_4 : AddConstMapClass F G H 1 b
f : F
x : G
⊢ (f : (a : G) → H) (x - 1) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) b

Tactic:
map_sub_const f x

Premises used: AddConstMapClass.map_sub_const
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)

Tactic:
simpa using map_sub_nsmul f x n

Premises used: AddConstMapClass.map_sub_nsmul
-- Module: Mathlib.Algebra.AddConstMap.Basic
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 : ℕ
inst_4 : n.AtLeastTwo
⊢ (f : (a : G) → H) (x - OfNat.ofNat n) =
    HSub.hSub (α := H) ((f : (a : G) → H) x : H) (HSMul.hSMul (α := ℕ) (OfNat.ofNat n) b)

Tactic:
map_sub_nat' f x n

Premises used: AddConstMapClass.map_sub_nat'
-- 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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ (f : (a : G) → H) (x + HSMul.hSMul (α := ℤ) (↑n : ℤ) a) =
    HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (HSMul.hSMul (α := ℤ) (↑n : ℤ) b)

Tactic:
simp
-- 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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ (f : (a : G) → H) (x + Int.negSucc n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (Int.negSucc n • b)

Tactic:
simp [← sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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 : AddGroup G
inst_2 : AddGroup H
inst_3 : AddConstMapClass F G H a b
f : F
n : ℤ
⊢ (f : (a : G) → H) (n • a) = HAdd.hAdd (α := H) ((f : (a : G) → H) 0 : H) (n • b)

Tactic:
simpa using map_add_zsmul f 0 n

Premises used: AddConstMapClass.map_add_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
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x + (↑n : G)) : H) ((f : (a : G) → H) (x + (↑n : G)) : H)
⊢ (f : (a : G) → H) (x + (↑n : G)) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)

Tactic:
rw [← map_add_zsmul f x n, zsmul_one]

Premises used: AddConstMapClass.map_add_zsmul, zsmul_one
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddGroupWithOne G
inst_2 : AddGroupWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
x : G
n : ℤ
⊢ (f : (a : G) → H) (x + (↑n : G)) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) x : H) ((↑n : H) : H)

Tactic:
simp
-- 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 : 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)

Tactic:
simpa [sub_eq_add_neg] using map_add_zsmul f x (-n)

Premises used: AddConstMapClass.map_add_zsmul, sub_eq_add_neg, Neg.neg
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (x - (↑n : G)) : H) ((f : (a : G) → H) (x - (↑n : G)) : H)
⊢ (f : (a : G) → H) (x - (↑n : G)) = HSub.hSub (α := H) ((f : (a : G) → H) x : H) (n • b)

Tactic:
rw [← map_sub_zsmul, zsmul_one]

Premises used: AddConstMapClass.map_sub_zsmul, zsmul_one
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddGroupWithOne G
inst_2 : AddGroupWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
x : G
n : ℤ
⊢ (f : (a : G) → H) (x - (↑n : G)) = HSub.hSub (α := H) (β := H) ((f : (a : G) → H) x : H) ((↑n : H) : H)

Tactic:
simp
-- 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 : 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)
rw₁ rw₂ : HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b) = 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)

Tactic:
rw [add_comm, map_add_zsmul]

Premises used: AddConstMapClass.map_add_zsmul, add_comm
-- Module: Mathlib.Algebra.AddConstMap.Basic
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) ((↑n : G) + x) : H) ((f : (a : G) → H) ((↑n : G) + x) : H)
⊢ (f : (a : G) → H) ((↑n : G) + x) = HAdd.hAdd (α := H) ((f : (a : G) → H) x : H) (n • b)

Tactic:
rw [← map_zsmul_add, zsmul_one]

Premises used: zsmul_one, AddConstMapClass.map_zsmul_add
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
G : Type u_2
H : Type u_3
inst : FunLike F G H
inst_1 : AddCommGroupWithOne G
inst_2 : AddGroupWithOne H
inst_3 : AddConstMapClass F G H 1 1
f : F
n : ℤ
x : G
⊢ (f : (a : G) → H) ((↑n : G) + x) = HAdd.hAdd (α := H) (β := H) ((f : (a : G) → H) x : H) ((↑n : H) : H)

Tactic:
simp
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
F : Type u_1
H : Type u_3
b : H
R : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : AddGroup H
inst_4 : FunLike F R H
inst_5 : AddConstMapClass F R H 1 b
f : F
x : R
⊢ (f : (a : R) → H) (Int.fract x) = HSub.hSub (α := H) ((f : (a : R) → H) x : H) (⌊x⌋ • b)

Tactic:
map_sub_int' ..

Premises used: Int.fract, AddConstMapClass.map_sub_int'
-- 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
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
replace : ∀ (hR : Covariant H H (fun (x y : H) ↦ y + x) R), R ((f : (a : G) → H) x) ((f : (a : G) → H) y)
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)

Tactic:
replace hR := hR.elim
-- 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)
x y : G
hxy : (fun (x1 x2 : G) ↦ x1 < x2) x y
hR : Covariant H H (fun (x y : H) ↦ y + x) R
⊢ 0 ≤ a

Tactic:
have ha' : 0 ≤ a := ha.le
-- 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)
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)
wlog : ∀ (x y : G) (hxy : x < 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)

Tactic:
wlog hx : x ∈ Ico l (l + a) generalizing x y

Premises used: Set.Ico, HAdd.hAdd
-- 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)
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)
inr : ∀ (m : ℤ) (hm : x - m • a ∈ 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)

Tactic:
rcases existsUnique_sub_zsmul_mem_Ico ha x l with ⟨m, hm, -⟩

Premises used: existsUnique_sub_zsmul_mem_Ico
-- 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)
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_1 : ∀ (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)
this : R ((f : (a : G) → H) (x - m • a)) ((f : (a : G) → H) (y - m • a))
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)

Tactic:
simpa using hR (m • b) this

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)
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)
inr : R ((f : (a : G) → H) (x - m • a)) ((f : (a : G) → H) (y - m • a))
⊢ R ((f : (a : G) → H) x) ((f : (a : G) → H) y)

Tactic:
suffices R (f (x - m • a)) (f (y - m • a)) by simpa using hR (m • b) this
-- 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)
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)
⊢ x - m • a < y - m • 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)
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 - m • a)) ((f : (a : G) → H) (y - m • a))

Tactic:
exact this _ _ (by simpa) hm
-- 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)
rcases : ∀ (n : ℤ) (hny : y - n • 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)

Tactic:
rcases existsUnique_sub_zsmul_mem_Ioc ha y l with ⟨n, hny, -⟩

Premises used: existsUnique_sub_zsmul_mem_Ioc