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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
← inv_lt_inv₀ (inv_pos.2 hb) ha,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹⁻¹ < a⁻¹ ↔ b < a⁻¹
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * r ≤ a + b

Tactic:
apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 2 * r * (2 * r) ≤ (a + b) * (a + b)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b < a ↔ b < a * c

Tactic:
inv_mul_lt_iff₀ hc,

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b < c * a ↔ b < a * c
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : α →o β
⊢ ⇑((fun p ↦ (↑g.symm).comp (p.comp ↑f)) ((fun p ↦ (↑g).comp (p.comp ↑f.symm)) p)) = ⇑p

Tactic:
change (g.symm ∘ g) ∘ p ∘ (f.symm ∘ f) = p

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : α →o β
⊢ (⇑g.symm ∘ ⇑g) ∘ ⇑p ∘ ⇑f.symm ∘ ⇑f = ⇑p
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b

Tactic:
apply le_iff_le_of_cmp_eq_cmp

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ cmp ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a)
      ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b) =
    cmp a b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a * a ^ k < 1

Tactic:
exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

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

Goal state before:
pp: a : ℤ
⊢ |a|.natAbs = a.natAbs

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) ^ 2)

Tactic:
inv_mul_cancel_left

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) ^ 2 = (a ⊔ b) ^ 2
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ

Tactic:
by
  let : DistribLattice α := CommGroup.toDistribLattice α
  calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]

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

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

Tactic:
by grind

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

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

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
by grind

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

Goal state before:
pp: ⊢ ¬Odd 0

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Odd n ↔ Even n

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Even n ↔ Odd n

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Even n ∨ Odd n

Tactic:
by grind

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < |1|ₘ ↔ 1 ≠ 1

pp: case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
· simp

Goal state after:
case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: m n : ℤ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Even (2 * n + 1)

Tactic:
by grind

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

Goal state before:
pp: m n : ℤ
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)

Tactic:
by grind

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ Odd (m ^ n) ↔ Odd m ∨ n = 0

Tactic:
by grind

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

Goal state before:
pp: m : ℤ
n : ℕ
h : n ≠ 0
⊢ Odd (m ^ n) ↔ Odd m

Tactic:
by grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
by grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
by grind

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

Goal state before:
pp: m n : ℤ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
by grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)

Tactic:
by grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Even (n * (n + 1))

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Even (n * (n - 1))

Tactic:
by grind

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

Goal state before:
pp: n : ℕ
⊢ Odd ↑n ↔ Odd n

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Even n.natAbs ↔ Even n

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n.natAbs ↔ Odd n

Tactic:
by grind

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

Goal state before:
pp: a b : ℤ
ha : Odd a
hb : Odd b
⊢ 4 ∣ a + b ∨ 4 ∣ a - b

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n → 2 * (n / 2) + 1 = n

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n → 1 + n / 2 * 2 = n

Tactic:
by grind

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

Goal state before:
pp: n : ℤ
h : Odd n
⊢ 2 * (n / 2) = n - 1

Tactic:
by grind

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

Goal state before:
pp: z : ℤ
⊢ Even z.sign ↔ z = 0

Tactic:
by grind

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

Goal state before:
pp: z : ℤ
⊢ Odd z.sign ↔ z ≠ 0

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑(a.toNat * (p + 1) + b.toNat * (q + 1)) = ↑n

Tactic:
Nat.cast_add,

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑(a.toNat * (p + 1)) + ↑(b.toNat * (q + 1)) = ↑n
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : β
⊢ map₂ f a (some b) = Option.map (fun a ↦ f a b) a

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = map₂ (fun a b ↦ f b a) b a

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → β → γ
g : γ → δ
⊢ Option.map g (map₂ f a b) = map₂ (fun a b ↦ g (f a b)) a b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : γ → β → δ
g : α → γ
⊢ map₂ f (Option.map g a) b = map₂ (fun a b ↦ f (g a) b) a b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → γ → δ
g : β → γ
⊢ map₂ f a (Option.map g b) = map₂ (fun a b ↦ f a (g b)) a b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
a : Option α
b : Option β
⊢ map₂ (curry f) a b = Option.map f (map₂ Prod.mk a b)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x : Option (α × β)
⊢ Option.map (uncurry f) x = map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
ε : Type u_8
ε' : Type u_9
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ a) (Option.map g₂ b)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' a) b

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' a b)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ b) (Option.map g₂ a)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
β' : Type u_6
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' b) a

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ Option.map g (map₂ f a b) = map₂ f' b (Option.map g' a)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
α' : Type u_5
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' b a)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' b a)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
o : Option β
⊢ map₂ f (some a) o = o

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
o : Option α
⊢ map₂ f o (some b) = o

Tactic:
by grind

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

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ⊥ + ↑a✝

pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹

Tactic:
· simp

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ↑a✝ + ⊥

pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝

Tactic:
· simp

Goal state after:
case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝¹ + ↑a✝
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b c : α
⊢ - -⊤ = ⊤

pp: case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a = a

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a = a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b✝ c b : α
⊢ -(⊤ + b) = -b + -⊤

pp: case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
⊢ -(a + b) = -b + -a

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
⊢ -(a + b) = -b + -a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr.inl
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ -(a + ⊤) = -⊤ + -a

pp: case inr.inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) = -b + -a

Tactic:
· simp

Goal state after:
case inr.inr
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) = -b + -a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 < a - ⊤ ↔ ⊤ < a ∨ ⊤ = ⊤

pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
· simp

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ 0 ≤ ⊤ - ⊤

pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a

Tactic:
· simp

Goal state after:
case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ a - a
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case inl
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
⊢ f (1 0) = 1 0

pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f (1 x) = 1 x

Tactic:
· simp

Goal state after:
case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ f (1 x) = 1 x
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < ⊤
⊢ x + ⊤ ≤ z + ⊤

pp: case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝

Tactic:
· simp

Goal state after:
case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : 0 ≤ c
⊢ a ≤ c + b

pp: case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c

Tactic:
· simpa using add_le_add h' h.le

Goal state after:
case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑m ≤ ↑n

Tactic:
exact mono_cast h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Tactic:
· exact Or.inl ⟨mod_cast h.le, hnx h⟩

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
b a✝ : α
h : ↑a✝ ≠ ⊥
⊢ (↑a✝).unbot h = b ↔ ↑a✝ = ↑b

Tactic:
· simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
a a✝ : α
h : ↑a✝ ≠ ⊥
⊢ a = (↑a✝).unbot h ↔ ↑a = ↑a✝

Tactic:
· simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab : a ≤ b
⊢ a * 0 ≤ b * 0

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab : a ≤ b
c : α
hc : c ≠ 0
⊢ a * c ≤ b * c

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab : a ≤ b
c : α
hc : c ≠ 0
⊢ a * c ≤ b * c