awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c

Tactic:
Contravariant.AddLECancellable.le_tsub_iff_right h

Premises used: AddLECancellable.le_tsub_iff_right, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
hbc : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
Contravariant.AddLECancellable.tsub_lt_iff_left hbc

Premises used: AddLECancellable.tsub_lt_iff_left, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
hbc : b ≤ a
⊢ a - b < c ↔ a < c + b

Tactic:
Contravariant.AddLECancellable.tsub_lt_iff_right hbc

Premises used: AddLECancellable.tsub_lt_iff_right, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < c ↔ a - c < b

Tactic:
Contravariant.AddLECancellable.tsub_lt_iff_tsub_lt Contravariant.AddLECancellable h₁ h₂

Premises used: AddLECancellable.tsub_lt_iff_tsub_lt, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a

Tactic:
Contravariant.AddLECancellable.le_tsub_iff_le_tsub Contravariant.AddLECancellable h₁ h₂

Premises used: AddLECancellable.le_tsub_iff_le_tsub, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
Contravariant.AddLECancellable.lt_tsub_iff_right_of_le h

Premises used: AddLECancellable.lt_tsub_iff_right_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : c ≤ b
⊢ a < b - c ↔ c + a < b

Tactic:
Contravariant.AddLECancellable.lt_tsub_iff_left_of_le h

Premises used: AddLECancellable.lt_tsub_iff_left_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
inst_7 : AddLeftReflectLT α
hca : c ≤ a
h : a - b < a - c
⊢ c < b

Tactic:
Contravariant.AddLECancellable.lt_of_tsub_lt_tsub_left_of_le hca h

Premises used: AddLECancellable.lt_of_tsub_lt_tsub_left_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
⊢ b ≤ a → c < b → a - b < a - c

Tactic:
Contravariant.AddLECancellable.tsub_lt_tsub_left_of_le

Premises used: AddLECancellable.tsub_lt_tsub_left_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : c ≤ a
h2 : a < b
⊢ a - c < b - c

Tactic:
Contravariant.AddLECancellable.tsub_lt_tsub_right_of_le h h2

Premises used: AddLECancellable.tsub_lt_tsub_right_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c

Tactic:
Contravariant.AddLECancellable.tsub_inj_right h₁ h₂ h₃

Premises used: Contravariant.AddLECancellable, AddLECancellable.tsub_inj_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
inst_7 : AddLeftReflectLT α
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < a - c ↔ c < b

Tactic:
Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le Contravariant.AddLECancellable h₁
    h₂

Premises used: AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
hcb : c ≤ b
⊢ a + c + (b - c) = a + b

Tactic:
Contravariant.AddLECancellable.add_add_tsub_cancel hcb

Premises used: AddLECancellable.add_add_tsub_cancel, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : c ≤ a
⊢ a + b - (a - c) = b + c

Tactic:
Contravariant.AddLECancellable.add_tsub_tsub_cancel h

Premises used: AddLECancellable.add_tsub_tsub_cancel, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b : α
inst_6 : AddLeftReflectLE α
h : a ≤ b
⊢ b - (b - a) = a

Tactic:
Contravariant.AddLECancellable.tsub_tsub_cancel_of_le h

Premises used: AddLECancellable.tsub_tsub_cancel_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : b ≤ a
⊢ a - c - (a - b) = b - c

Tactic:
Contravariant.AddLECancellable.tsub_tsub_tsub_cancel_left h

Premises used: AddLECancellable.tsub_tsub_tsub_cancel_left, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : c ≤ b
obtain : ∀ (d : α) (h : c ≤ c + d), a - (c + d - c) = a + c - (c + d)
⊢ a - (b - c) = a + c - b

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a c : α
inst_6 : AddLeftReflectLE α
d : α
h : c ≤ c + d
rw : a - d = a + c - (c + d)
rw₁ : a - d = c + a - (c + d)
rw₂ rw₃ : a - d = a - d
⊢ a - (c + d - c) = a + c - (c + d)

Tactic:
rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]

Premises used: add_tsub_cancel_left, add_comm, add_tsub_add_eq_tsub_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Add α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : Preorder β
inst_5 : Add β
inst_6 : Sub β
inst_7 : OrderedSub β
f : α →ₙ+ β
hf : Monotone.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
a b : α
rw : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (a - b + b) : β)
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ≤ (f : (a : α) → β) (a - b)

Tactic:
rw [tsub_le_iff_right, ← f.map_add]

Premises used: tsub_le_iff_right, AddHom.map_add
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Add α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : Preorder β
inst_5 : Add β
inst_6 : Sub β
inst_7 : OrderedSub β
f : α →ₙ+ β
hf : Monotone.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
a b : α
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (a - b + b) : β)

Tactic:
hf le_tsub_add

Premises used: le_tsub_add
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Add α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : Preorder β
inst_5 : Add β
inst_6 : Sub β
inst_7 : OrderedSub β
f : α →ₙ+ β
hf : Monotone.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
a b : α
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (a - b + b) : β)

Tactic:
exact hf le_tsub_add

Premises used: le_tsub_add
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
R : Type u_3
inst : Distrib R
inst_1 : Preorder R
inst_2 : Sub R
inst_3 : OrderedSub R
inst_4 : MulLeftMono R
a b c : R
⊢ a * b - a * c ≤ a * (b - c)

Tactic:
(AddHom.mulLeft a).le_map_tsub (monotone_id.const_mul' a) _ _

Premises used: monotone_id, Monotone.const_mul', AddHom.mulLeft, AddHom.le_map_tsub
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
R : Type u_3
inst : NonUnitalCommSemiring R
inst_1 : Preorder R
inst_2 : Sub R
inst_3 : OrderedSub R
inst_4 : MulLeftMono R
a b c : R
⊢ a * c - b * c ≤ (a - b) * c

Tactic:
simpa only [mul_comm _ c] using le_mul_tsub

Premises used: le_mul_tsub, mul_comm
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
lhs : HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
| HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)

Tactic:
lhs
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
rw : HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β)
| HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
rw [← tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
rw : HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β)
| HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)

Tactic:
lhs; rw [← tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
conv :
  HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)

Tactic:
conv => lhs; rw [← tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
rw :
  HSub.hSub (β := β) (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (a - b) : β) ((f : (a : α) → β) b : β))
      ((f : (a : α) → β) b : β) =
    (f : (a : α) → β) (a - b)
rw₁ rw₂ : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (a - b) : β) ((f : (a : α) → β) (a - b) : β)
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)

Tactic:
rw [map_add, add_tsub_cancel_right]

Premises used: map_add, add_tsub_cancel_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
⊢ (e : (a : M) → N) (a - b) = HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)

Tactic:
le_antisymm ?_ (e_add.toAddHom.le_map_tsub e.monotone a b)

Premises used: OrderIso.monotone, le_antisymm, AddHom.le_map_tsub, AddEquiv.toAddHom
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
refine : (e : (a : M) → N) (a - b) ≤ HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
⊢ (e : (a : M) → N) (a - b) = HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)

Tactic:
refine le_antisymm ?_ (e_add.toAddHom.le_map_tsub e.monotone a b)

Premises used: OrderIso.monotone, le_antisymm, AddHom.le_map_tsub, AddEquiv.toAddHom
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
this :
  LE.le.{u_4} (α := N)
    ((e : (a : M) → N)
        (HSub.hSub (α := M) (β := M) ((e.symm : (a : N) → M) ((e : (a : M) → N) a : N) : M)
          ((e.symm : (a : N) → M) ((e : (a : M) → N) b : N) : M)) :
      N)
    ((e : (a : M) → N)
        ((e.symm : (a : N) → M) (HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)) : M) :
      N)
⊢ (e : (a : M) → N) (a - b) ≤ HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
suffices :
  LE.le.{u_4} (α := N)
    ((e : (a : M) → N)
        (HSub.hSub (α := M) (β := M) ((e.symm : (a : N) → M) ((e : (a : M) → N) a : N) : M)
          ((e.symm : (a : N) → M) ((e : (a : M) → N) b : N) : M)) :
      N)
    ((e : (a : M) → N)
        ((e.symm : (a : N) → M) (HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)) : M) :
      N)
⊢ (e : (a : M) → N) (a - b) ≤ HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)

Tactic:
suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
⊢ LE.le.{u_4} (α := N)
    ((e : (a : M) → N)
        (HSub.hSub (α := M) (β := M) ((e.symm : (a : N) → M) ((e : (a : M) → N) a : N) : M)
          ((e.symm : (a : N) → M) ((e : (a : M) → N) b : N) : M)) :
      N)
    ((e : (a : M) → N)
        ((e.symm : (a : N) → M) (HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)) : M) :
      N)

Tactic:
e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)

Premises used: OrderIso.monotone, OrderIso.symm, AddHom.le_map_tsub, AddEquiv.symm, AddEquiv.toAddHom
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
⊢ LE.le.{u_4} (α := N)
    ((e : (a : M) → N)
        (HSub.hSub (α := M) (β := M) ((e.symm : (a : N) → M) ((e : (a : M) → N) a : N) : M)
          ((e.symm : (a : N) → M) ((e : (a : M) → N) b : N) : M)) :
      N)
    ((e : (a : M) → N)
        ((e.symm : (a : N) → M) (HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)) : M) :
      N)

Tactic:
exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)

Premises used: OrderIso.monotone, OrderIso.symm, AddHom.le_map_tsub, AddEquiv.symm, AddEquiv.toAddHom
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : AddCommMonoid α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : Preorder β
inst_5 : AddZeroClass β
inst_6 : Sub β
inst_7 : OrderedSub β
f : α →+ β
hf : Monotone.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
a b : α
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ≤ (f : (a : α) → β) (a - b)

Tactic:
f.toAddHom.le_map_tsub hf a b

Premises used: AddMonoidHom.toAddHom, AddHom.le_map_tsub
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a b : α
⊢ (↑(a - b) : WithTop α) = (↑a : WithTop α) - (↑b : WithTop α)

Tactic:
rfl

Premises used: WithTop.some, WithTop.sub, rfl
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a : α
⊢ ⊤ - (↑a : WithTop α) = ⊤

Tactic:
rfl

Premises used: WithTop.sub, rfl
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a : WithTop α
top : HSub.hSub (α := WithTop α) ⊤ ⊤ = (↑⊥ : WithTop α)
coe : ∀ (a : α), (↑a : WithTop α) - ⊤ = (↑⊥ : WithTop α)
⊢ a - ⊤ = (↑⊥ : WithTop α)

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
⊢ HSub.hSub (α := WithTop α) ⊤ ⊤ = (↑⊥ : WithTop α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a : α
⊢ (↑a : WithTop α) - ⊤ = (↑⊥ : WithTop α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a b : WithTop α
top : ⊤ - b = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ b ≠ ⊤
coe : ∀ (a : α), (↑a : WithTop α) - b = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ b ≠ ⊤
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Tactic:
induction a
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
b : WithTop α
top : HSub.hSub (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤
top₁ : ∀ (a : α), ⊤ - (↑a : WithTop α) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ (↑a : WithTop α) ≠ ⊤
⊢ ⊤ - b = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ b ≠ ⊤

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
b : WithTop α
a : α
coe : (↑a : WithTop α) - ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤
coe₁ : ∀ (a_1 : α), (↑a : WithTop α) - (↑a_1 : WithTop α) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ (↑a_1 : WithTop α) ≠ ⊤
⊢ (↑a : WithTop α) - b = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ b ≠ ⊤

Tactic:
induction b
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
⊢ HSub.hSub (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

Premises used: and_self, false_and, not_true_eq_false, Ne, WithTop.coe_ne_top, WithTop.top_sub_coe, and_false, WithTop.coe_sub, not_false_eq_true, WithTop.sub_top
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a : α
⊢ ⊤ - (↑a : WithTop α) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ (↑a : WithTop α) ≠ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

Premises used: and_self, false_and, not_true_eq_false, Ne, WithTop.coe_ne_top, WithTop.top_sub_coe, and_false, WithTop.coe_sub, not_false_eq_true, WithTop.sub_top
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a : α
⊢ (↑a : WithTop α) - ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

Premises used: and_self, false_and, not_true_eq_false, Ne, WithTop.coe_ne_top, WithTop.top_sub_coe, and_false, WithTop.coe_sub, not_false_eq_true, WithTop.sub_top
-- Module: Mathlib.Algebra.Order.Sub.WithTop
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a a_1 : α
⊢ (↑a : WithTop α) - (↑a_1 : WithTop α) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ (↑a_1 : WithTop α) ≠ ⊤

Tactic:
simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false,
      not_false_eq_true, and_false, and_self]

Premises used: and_self, false_and, not_true_eq_false, Ne, WithTop.coe_ne_top, WithTop.top_sub_coe, and_false, WithTop.coe_sub, not_false_eq_true, WithTop.sub_top