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)
hn_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
k : ℤ
⊢ l + a ∈ 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_1 : 1 ≤ n
hy : R ((f : (a : G) → H) (l + n • a)) ((f : (a : G) → H) y)
hn : 1 < n
k : ℤ
⊢ 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_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 + n • 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 : AddCommGroup H
inst_6 : PartialOrder H
inst_7 : IsOrderedAddMonoid H
inst_8 : AddConstMapClass F G H a b
f : F
ha : 0 < a
l : G
⊢ Monotone.{u_2, u_3} (α := G) (β := H) (⇑f : (a : G) → H) ↔
    MonotoneOn.{u_2, u_3} (β := H) (⇑f : (a : G) → H) (Icc l (l + a))

Tactic:
⟨(Monotone.monotoneOn · _), fun hf ↦ monotone_iff_forall_lt.2 <|
    AddConstMapClass.rel_map_of_Icc ha fun _x hx _y hy hxy ↦ hf hx hy hxy.le⟩

Premises used: Iff.mpr, LT.lt.le, AddConstMapClass.rel_map_of_Icc, Set.Icc, HAdd.hAdd, Iff.intro, monotone_iff_forall_lt, Monotone.monotoneOn
-- 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 : AddCommGroup H
inst_6 : PartialOrder H
inst_7 : IsOrderedAddMonoid H
inst_8 : AddConstMapClass F G H a b
f : F
ha : 0 < a
l : G
⊢ Antitone.{u_2, u_3} (α := G) (β := H) (⇑f : (a : G) → H) ↔
    AntitoneOn.{u_2, u_3} (β := H) (⇑f : (a : G) → H) (Icc l (l + a))

Tactic:
monotone_iff_Icc (H := Hᵒᵈ) ha l

Premises used: AddConstMapClass.monotone_iff_Icc, Antitone, AntitoneOn
-- 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 : AddCommGroup H
inst_6 : PartialOrder H
inst_7 : IsOrderedAddMonoid H
inst_8 : AddConstMapClass F G H a b
f : F
ha : 0 < a
l : G
⊢ StrictMono.{u_2, u_3} (α := G) (β := H) (⇑f : (a : G) → H) ↔
    StrictMonoOn.{u_2, u_3} (β := H) (⇑f : (a : G) → H) (Icc l (l + a))

Tactic:
⟨(StrictMono.strictMonoOn · _), AddConstMapClass.rel_map_of_Icc ha⟩

Premises used: AddConstMapClass.rel_map_of_Icc, Set.Icc, HAdd.hAdd, StrictMono.strictMonoOn, Iff.intro
-- 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 : AddCommGroup H
inst_6 : PartialOrder H
inst_7 : IsOrderedAddMonoid H
inst_8 : AddConstMapClass F G H a b
f : F
ha : 0 < a
l : G
⊢ StrictAnti.{u_2, u_3} (α := G) (β := H) (⇑f : (a : G) → H) ↔
    StrictAntiOn.{u_2, u_3} (β := H) (⇑f : (a : G) → H) (Icc l (l + a))

Tactic:
strictMono_iff_Icc (H := Hᵒᵈ) ha l

Premises used: StrictAntiOn, StrictAnti, AddConstMapClass.strictMono_iff_Icc
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
f : G → H
hf : ∀ (x : G), f (x + a) = f x + b
⊢ (⇑{ toFun := f, map_add_const' := hf : G →+c[a, b] H } : (a : G) → H) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
f : G →+c[a, b] H
⊢ { toFun := (⇑f : (a : G) → H), map_add_const' := ⋯ : G →+c[a, b] H } = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
f : G →+c[a, b] H
⊢ f.toFun = (⇑f : (a : G) → H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
f g : G →+c[a, b] H
h : ∀ (x : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) x : H) ((g : (a : G) → H) x : H)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
K : Type u_3
inst_2 : Add K
c : K
g : H →+c[b, c] K
f : G →+c[a, b] H
⊢ ∀ (x : G),
    Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := H) (⇑g : (a : H) → K) (⇑f : (a : G) → H) (x + a) =
      Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := H) (⇑g : (a : H) → K) (⇑f : (a : G) → H) x + c

Tactic:
simp
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
f : G →+c[a, b] H
⊢ f.comp AddConstMap.id = f

Tactic:
rfl

Premises used: AddConstMap.comp, rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
f : G →+c[a, b] H
⊢ comp AddConstMap.id f = f

Tactic:
rfl

Premises used: AddConstMap.comp, rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
K : Type u_3
inst_2 : VAdd K H
inst_3 : VAddAssocClass K H H
c : K
f : G →+c[a, b] H
x : G
⊢ HVAdd.hVAdd (β := (a : G) → H) c (⇑f : (a : G) → H) (x + a) =
    HVAdd.hVAdd (β := (a : G) → H) c (⇑f : (a : G) → H) x + b

Tactic:
simp [vadd_add_assoc]

Premises used: vadd_add_assoc
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
K : Type u_3
inst_2 : VAdd K H
inst_3 : VAddAssocClass K H H
c : K
f : G →+c[a, b] H
⊢ (⇑(c +ᵥ f) : (a : G) → H) = HVAdd.hVAdd (β := (a : G) → H) c (⇑f : (a : G) → H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : Add G
a : G
f g : G →+c[a, a] G
⊢ f * g = f.comp g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : Add G
a : G
f g : G →+c[a, a] G
⊢ Eq (α := (a : G) → G) (⇑(f * g) : (a : G) → G) (Function.comp (β := G) (⇑f : (a : G) → G) (⇑g : (a : G) → G))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : Add G
a : G
⊢ Eq.{u_1 + 1} (α := G →+c[a, a] G) 1 AddConstMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : Add G
a : G
⊢ Eq.{u_1 + 1} (α := (a : G) → G) (⇑1 : (a : G) → G) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : Add G
a : G
f : G →+c[a, a] G
n : ℕ
⊢ Eq (α := (a : G) → G) (⇑(f ^ n) : (a : G) → G) (⇑f : (a : G) → G)^[n]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : Add G
a : G
f : G →+c[a, a] G
n : ℕ
x : G
⊢ (f ^ n : (a : G) → G) x = (⇑f : (a : G) → G)^[n] x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
K : Type u_3
inst : Add G
inst_1 : AddZeroClass H
a : G
b : H
inst_2 : DistribSMul K H
c : K
f : G →+c[a, b] H
x : G
⊢ HSMul.hSMul (β := (a : G) → H) c (⇑f : (a : G) → H) (x + a) =
    HSMul.hSMul (β := (a : G) → H) c (⇑f : (a : G) → H) x + c • b

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : AddMonoid G
a : G
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)
⊢ HVAdd.hVAdd (α := G) (β := G →+c[a, a] G) ((Multiplicative.toAdd : (a : Multiplicative G) → G) 1 : G) AddConstMap.id =
    1

Tactic:
ext
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : AddMonoid G
a 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:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : AddMonoid G
a : G
x x_1 : Multiplicative G
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)
⊢ 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

Tactic:
ext
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
inst : AddMonoid G
a : G
x x_1 : Multiplicative G
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:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : AddCommGroup H
a : G
b : H
f : G →+c[a, b] H
x : G
⊢ (fun (x : G) ↦ (-(f : (a : G) → H) (-x) : H)) (x + a) = (fun (x : G) ↦ (-(f : (a : G) → H) (-x) : H)) x + b

Tactic:
simp [neg_add_eq_sub]

Premises used: neg_add_eq_sub
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : AddCommGroup H
a : G
b : H
x : G →+c[a, b] H
x_1 : G
⊢ Eq.{u_2 + 1} (α := H)
    (((fun (f : G →+c[a, b] H) ↦
              ({ toFun := fun (x : G) ↦ -(f : (a : G) → H) (-x), map_add_const' := ⋯ } : G →+c[a, b] H))
            ((fun (f : G →+c[a, b] H) ↦
                ({ toFun := fun (x : G) ↦ -(f : (a : G) → H) (-x), map_add_const' := ⋯ } : G →+c[a, b] H))
              x) :
          (a : G) → H)
        x_1 :
      H)
    ((x : (a : G) → H) x_1 : H)

Tactic:
simp
-- Module: Mathlib.Algebra.AddConstMap.Basic
Goal:
G : Type u_1
H : Type u_2
inst : AddCommGroup G
inst_1 : AddCommGroup H
a : G
b : H
⊢ Eq (α := (G →+c[a, b] H) ≃ (G →+c[a, b] H)) (Equiv.symm conjNeg) conjNeg

Tactic:
rfl

Premises used: AddConstMap.conjNeg, Function.Involutive.toPerm, Equiv.symm, rfl
-- Module: Mathlib.Algebra.AddConstMap.Basic
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 : (↑(Ico 0 1) : Type u_1) → G
x : R
⊢ (fun (x : R) ↦ f (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ico 0 1) x) (Int.fract x) ⋯) + ⌊x⌋ • a)
      (x + 1) =
    (fun (x : R) ↦
          f (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ico 0 1) x) (Int.fract x) ⋯) + ⌊x⌋ • a)
        x +
      a

Tactic:
simp [add_one_zsmul, add_assoc]

Premises used: add_assoc, add_one_zsmul
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
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) ⋯) + ⌊x⌋ • a,
                map_add_const' := ⋯ } :
              R →+c[1, a] G))
          x)
        x_1 =
      x x_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) ⋯) + ⌊x⌋ • a,
              map_add_const' := ⋯ } :
            R →+c[1, a] G))
        x) =
    x

Tactic:
ext x
-- Module: Mathlib.Algebra.AddConstMap.Basic
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_1 : (↑(Ico 0 1) : Type u_1) → G
x : (↑(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) ⋯) + ⌊x⌋ • a,
              map_add_const' := ⋯ } :
            R →+c[1, a] G))
        x_1)
      x =
    x_1 x

Tactic:
simp [Int.fract_eq_self.2 x.2, Int.floor_eq_zero_iff.2 x.2]

Premises used: Iff.mpr, Int.floor_eq_zero_iff, Int.fract_eq_self, Subtype.property
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
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) ⋯) +
                        ⌊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) :
            (a : R) → G)
          x :
        G)
      ((f : (a : R) → G) x : 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

Tactic:
ext x
-- Module: Mathlib.Algebra.AddConstMap.Basic
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
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) ⋯) +
                      ⌊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) :
          (a : R) → G)
        x :
      G)
    ((f : (a : R) → G) x : G)

Tactic:
simp [map_fract]

Premises used: AddConstMapClass.map_fract
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e₁ e₂ : G ≃+c[a, b] H
h : ∀ (x : G), Eq.{u_2 + 1} (α := H) ((e₁ : (a : G) → H) x : H) ((e₂ : (a : G) → H) x : H)
⊢ e₁ = e₂

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e₁ e₂ : G ≃+c[a, b] H
⊢ e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

Tactic:
toEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, AddConstEquiv.toEquiv_injective
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ Eq (α := (a : G) → H) (⇑e.toEquiv : (a : G) → H) (⇑e : (a : G) → H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: AddConstEquiv.symm, Equiv.symm, rfl
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
inst : Add G
a : G
⊢ Eq (α := G ≃+c[a, a] G) (symm (refl a)) (refl a)

Tactic:
rfl

Premises used: AddConstEquiv.symm, AddConstEquiv.refl, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ e.trans (refl b) = e

Tactic:
rfl

Premises used: Equiv.trans, AddConstEquiv.trans, rfl
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ trans (refl a) e = e

Tactic:
rfl

Premises used: Equiv.trans, AddConstEquiv.trans, rfl
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ e.trans e.symm = refl a

Tactic:
toEquiv_injective e.toEquiv.self_trans_symm

Premises used: AddConstEquiv.toEquiv_injective, AddConstEquiv.toEquiv, Equiv.self_trans_symm
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ e.symm.trans e = refl b

Tactic:
toEquiv_injective e.toEquiv.symm_trans_self

Premises used: AddConstEquiv.toEquiv_injective, AddConstEquiv.toEquiv, Equiv.symm_trans_self
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ Eq (α := (a : H) → G) (⇑e.symm : (a : H) → G) (⇑e.symm : (a : H) → G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : Add G
inst_1 : Add H
a : G
b : H
e : G ≃+c[a, b] H
⊢ e.symm.toEquiv = e.symm

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.Algebra.AddConstMap.Equiv
Goal:
G : Type u_1
H : Type u_2
K : Type u_3
inst : Add G
inst_1 : Add H
inst_2 : Add K
a : G
b : H
c : K
e₁ : G ≃+c[a, b] H
e₂ : H ≃+c[b, c] K
⊢ (e₁.trans e₂).toEquiv = e₁.trans e₂.toEquiv

Tactic:
rfl

Premises used: Equiv.trans, rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
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}
rw₁ rw₂ : Eq (α := Set G) {0} {0}
⊢ VSub.vsub (P := Set P) {p} {p} = {0}

Tactic:
rw [Set.singleton_vsub_singleton, vsub_self]

Premises used: Set.singleton_vsub_singleton, vsub_self
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : p₁ = p₂), p₁ = p₂
⊢ p₁ = p₂

Tactic:
rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h

Premises used: sub_eq_zero, vsub_eq_zero_iff_eq, vsub_sub_vsub_cancel_right
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
⊢ p₁ -ᵥ p = p₂ -ᵥ p ↔ p₁ = p₂

Tactic:
⟨vsub_left_cancel, fun h => h ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, vsub_left_cancel, rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (β := G) fun (x : P) ↦ x -ᵥ p

Tactic:
fun _ _ =>
  vsub_left_cancel

Premises used: Function.Injective, vsub_left_cancel
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂

Tactic:
vadd_left_cancel (p -ᵥ p₂) ?_

Premises used: VSub.vsub, vadd_left_cancel
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂
refine : (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂
⊢ p₁ = p₂

Tactic:
refine vadd_left_cancel (p -ᵥ p₂) ?_

Premises used: VSub.vsub, vadd_left_cancel
-- Module: Mathlib.Algebra.AddTorsor.Basic
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
rw₂ rw₃ : p = p
⊢ (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂

Tactic:
rw [vsub_vadd, ← h, vsub_vadd]

Premises used: vsub_vadd
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
⊢ p -ᵥ p₁ = p -ᵥ p₂ ↔ p₁ = p₂

Tactic:
⟨vsub_right_cancel, fun h => h ▸ rfl⟩

Premises used: vsub_right_cancel, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Algebra.AddTorsor.Basic
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
T : AddTorsor G P
p : P
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (β := G) fun (x : P) ↦ p -ᵥ x

Tactic:
fun _ _ =>
  vsub_right_cancel

Premises used: vsub_right_cancel, Function.Injective
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂
rw₃ rw₄ : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
⊢ p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂

Tactic:
rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]

Premises used: sub_eq_add_neg, vsub_add_vsub_cancel, add_comm, neg_vsub_eq_vsub_rev
-- Module: Mathlib.Algebra.AddTorsor.Basic
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₂
rw₂ rw₃ : p₁ -ᵥ p₂ = p₁ -ᵥ p₂
⊢ (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂

Tactic:
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]

Premises used: vadd_vsub_assoc, add_sub_cancel_left, vsub_vadd_eq_vsub_sub