mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case pos
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

pp: case neg
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
·

Goal state after:
case pos
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case neg
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
·

Goal state after:
case neg
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
a✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹

pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
·

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ m ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
·

Goal state after:
case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
⊢ 0⁻¹ʳ = 0⁻¹

pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹

Tactic:
·

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
⊢ 0⁻¹ʳ = 0⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹

Tactic:
·

Goal state after:
case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a⁻¹ʳ = a⁻¹
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(ofNat a✝) = 0
⊢ ofNat a✝ = 0

pp: case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0

Tactic:
·

Goal state after:
case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(ofNat a✝) = 0
⊢ ofNat a✝ = 0
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0

Tactic:
·

Goal state after:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case ofNat
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (ofNat x) = g (ofNat x)

pp: case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]

Tactic:
·

Goal state after:
case ofNat
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f (ofNat x) = g (ofNat x)
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]

Tactic:
·

Goal state after:
case negSucc
M : Type u_5
inst✝ : Monoid M
f g : ℤ →* M
h_neg_one : f (-1) = g (-1)
h_nat : f.comp ↑ofNatHom = g.comp ↑ofNatHom
x : ℕ
⊢ f -[x+1] = g -[x+1]
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
·

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)

Tactic:
·

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 ↦ x1 * x2) a b) ((fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c

pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
·

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r b c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
·

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b

pp: case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
·

Goal state after:
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
·

Goal state after:
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 < x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 < x2) b c

pp: case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 = x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 = x2) b c

pp: case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
·

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 < x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 < x2) b c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 = x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 = x2) b c

pp: case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
·

Goal state after:
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 ↦ x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 = x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 = x2) b c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
·

Goal state after:
case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 ↦ x1 < x2) ∧ Contravariant M N μ fun x1 x2 ↦ x1 = x2
a : M
b c : N
bc : (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
⊢ Odd (a + 2) ↔ Odd a

Tactic:
rw [← one_add_one_eq_two, ← add_assoc, odd_add_one, even_add_one]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ n % 2 = 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: n : ℕ
h : n % 2 = 1
⊢ n = 2 * (n / 2) + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inl
k : ℕ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
·

Goal state after:
case inl
k : ℕ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inr
k : ℕ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
·

Goal state after:
case inr
k : ℕ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: m : ℕ
⊢ m % 2 + (m + 1) % 2 = 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: m : ℕ
⊢ (m + 1) % 2 + m % 2 = 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case zero
⊢ 2 ∣ 0 * (0 - 1)

pp: case succ
k : ℕ
⊢ 2 ∣ (k + 1) * (k + 1 - 1)

Tactic:
·

Goal state after:
case zero
⊢ 2 ∣ 0 * (0 - 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inr
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
rw [h.neg_one_pow, if_neg (by simpa using h)]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inl
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Even n
⊢ ↑n = 0 ∨ ↑n = 1

pp: case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
·

Goal state after:
case inl
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Even n
⊢ ↑n = 0 ∨ ↑n = 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
·

Goal state after:
case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - (a + c)

pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - (a + c)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
a c b : α
⊢ a + c - (b + c) = a - b

Tactic:
by
  refine add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| ?_)
  apply le_of_add_le_add_right
  rw [add_assoc]
  exact le_tsub_add

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : IsMulCommutative α
⊢ PosMulStrictMono α ↔ MulPosStrictMono α

Tactic:
by
  simp [posMulStrictMono_iff, mulPosStrictMono_iff, mul_comm']

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.NatCast

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono α
⊢ 1 < 1 + 1

Tactic:
exact lt_add_one _

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬a * c = a * b

pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬a * c = a * b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

pp: case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d ∨ a < a ∨ b < d

pp: case inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d ∨ a < a ∨ b < d

pp: case inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d ∨ a < a ∨ b < d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hbd : b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

pp: case inr.inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
hca : c < a
h : a * b = c * b
⊢ a = c ∧ b = b ∨ a < c ∨ b < b

pp: case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
·

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hbd : b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
hca : c < a
h : a * b = c * b
⊢ a = c ∧ b = b ∨ a < c ∨ b < b

pp: case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
·

Goal state after:
case inr.inr.inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
hca : c < a
h : a * b = c * b
⊢ a = c ∧ b = b ∨ a < c ∨ b < b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
·

Goal state after:
case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

pp: case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ b, b * b ≤ a

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ b, b * b ≤ a

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ b, b * b ≤ a
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a c : α
h : a ≤ a
⊢ a * c ≤ a * c

pp: case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a c : α
h : a ≤ a
⊢ a * c ≤ a * c
Module: Mathlib.Algebra.Order.Monoid.Defs

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h✝ : a ≤ b
c : α
h : a < b
⊢ a * c ≤ b * c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

pp: case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂
Module: Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: case inl
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a

pp: case inr
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a

Tactic:
·

Goal state after:
case inl
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a