mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
⊢ (∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k x ↦ Int.strongRec lt ge k

Tactic:
refine n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_) <;> ext l hl

Goal state after:
case refine_1
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
x✝ : ∀ (k : ℤ), k < m → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
l : ℤ
hl : l < m
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) m m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l

case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k + 1) m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l

case refine_3
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
x✝ : ∀ (k_1 : ℤ), k_1 < k - 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k - 1
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) l hl =
    Int.strongRec lt ge l
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
hf : Function.Surjective ⇑f
b : β
x✝ : b ∈ {b | IsSquare b}
s : β
h✝ : b = s * s
⊢ b ∈ ⇑f '' {a | IsSquare a}

Tactic:
rcases hf s with ⟨r, rfl⟩
  exact ⟨r * r, by simp [*]⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

pp: case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
· subst x
    simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
    simp [h.resolve_right ha]

Goal state after:
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c

Tactic:
by
  rw [div_eq_mul_inv]
  exact hac.mul_left hbc.inv_left₀

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ x⁻¹ʳ * y = z

Tactic:
rw [h1, inverse_mul_cancel_left _ _ h]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R
h : Commute a b
⊢ (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Tactic:
by
  simp [sq, add_mul, sub_mul, mul_sub, two_mul, h.eq, ← sub_add, ← sub_sub]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ n • b + b = n • b + 1 • b

Tactic:
one_smul

Goal state after:
case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ n • b + b = n • b + b
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (a ^ 2) ^ c * -a = -((a ^ 2) ^ c * a)

Tactic:
mul_neg

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

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

Tactic:
rw [← odd_add_two (a := a - 2), add_comm_sub, sub_self, add_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
ha : a < 0
hb : 0 < b
⊢ a * b < 0

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_pos_right ha hb

Goal state after:
Module: Mathlib.Data.Prod.PProd

Goal state before:
pp: α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
x₂ : α
y₂ : β
h : (x₁, y₁) = (x₂, y₂)
P : Sort u_7
w : x₁ = x₂ → y₁ = y₂ → P
⊢ P

Tactic:
cases h

Goal state after:
case refl
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
P : Sort u_7
w : x₁ = x₁ → y₁ = y₁ → P
⊢ P
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a : M₀
n : ℕ
inst✝ : ZeroLEOneClass M₀
ha : 0 ≤ a
hn : n ≠ 0
⊢ 1 ≤ a ^ n ↔ 1 ≤ a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ one_le_pow₀ h⟩
  contrapose! h
  exact pow_lt_one₀ ha h hn

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
⊢ MonotoneOn (fun a ↦ a ^ n) {a | 0 ≤ a}

Tactic:
lift n to ℕ using hn

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
⊢ MonotoneOn (fun a ↦ a ^ ↑n) {a | 0 ≤ a}
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
a b : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
this✝ : a ≤ 0 ∨ 0 ≤ a
this : b ≤ 0 ∨ 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
tauto

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

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

Tactic:
apply lt_of_mul_lt_mul_right _ ha.le

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ 0 * a < a⁻¹ * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ 0 * a < a⁻¹ * a

Tactic:
apply lt_of_mul_lt_mul_right _ ha.le

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ 0 * a * a < a⁻¹ * a * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
⊢ c * a / (c * b) ≤ a / b

Tactic:
mul_div_mul_left _ _ hc

Goal state after:
case inr
G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
⊢ a / b ≤ a / b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ c * a / (c * b)

Tactic:
mul_div_mul_left _ _ hc

Goal state after:
case inr
G₀ : Type u_3
inst✝¹ : CommGroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ a / b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
⊢ Acc s (f a) → Acc r a

Tactic:
by
  generalize h : f a = b
  intro ac
  induction ac generalizing a with | intro _ H IH => ?_
  subst h
  exact ⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
f : α → β
g : β → α
hf : f = ⇑e
hg : g = ⇑e.symm
⊢ ∀ {a b : α},
    s ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a)
        ({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b) ↔
      r a b

Tactic:
by simp [hf, e.map_rel_iff]

Goal state after:
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 β
e : α ≃ β
h₁ : Monotone ⇑e
h₂ : Monotone ⇑e.symm
a✝ b✝ : α
h : e a✝ ≤ e b✝
⊢ a✝ ≤ b✝

Tactic:
by simpa only [e.symm_apply_apply] using h₂ h

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

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ x ^ n

Tactic:
lift n to ℕ using hn

Goal state after:
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ ↑n
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n + 1

Tactic:
apply zero_lt_one.trans_le
  convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
  <;> simp

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n % k * (m * r % k % k) % k = r % k

Tactic:
mod_mod,

Goal state after:
case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n % k * (m * r % k) % k = r % k
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:
Int.natCast_toNat_eq_self.mpr
    (Int.emod_nonneg _ <| by lia),

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_n % ↑q.succ * ↑(p + 1) + ↑b.toNat * ↑(q + 1) = ↑n
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - a = 0 ↔ a ≠ ⊤

Tactic:
by
  rw [sub_eq_add_neg, add_neg_cancel_iff_ne_top]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z) → (fun x1 x2 ↦ x1 < x2) y z

Tactic:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using lt_of_add_lt_add_left

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ IsAddLeftRegular ↑a

Tactic:
rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]; simpa using @ha _ _

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ IsAddRightRegular ↑a

Tactic:
rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]; simpa using @ha _ _

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z) → (fun x1 x2 ↦ x1 < x2) y z

Tactic:
by
    cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using lt_of_add_lt_add_left

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case mp
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ Nat.find h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n

pp: case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m

Tactic:
· grind [Nat.find_min]

Goal state after:
case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case refine_1
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₘ + n
hpm : p m
⊢ Nat.find hₘ + n ≤ m

Tactic:
have hnm : n ≤ m := le_trans hn (find_le hpm)
    refine Nat.add_le_of_le_sub hnm (find_le ?_)
    rwa [Nat.sub_add_cancel hnm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst✝ : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial αˣ ∧ DenselyOrdered αˣ
⊢ Nontrivial αˣ

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
inst✝ : DenselyOrdered α
this : DenselyOrdered α ↔ Nontrivial αˣ ∧ DenselyOrdered αˣ
⊢ DenselyOrdered αˣ

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : Nontrivial αˣ
this : DenselyOrdered α ↔ Nontrivial αˣ ∧ DenselyOrdered αˣ
⊢ DenselyOrdered αˣ ↔ DenselyOrdered α

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
⊢ x = ⊥ ↔ ∀ (b : α), x ≤ ↑b

Tactic:
refine ⟨by simp +contextual, fun h ↦ (x.eq_bot_iff_forall_ne).2 fun y => ?_⟩
  rintro rfl
  exact not_isBot y fun z => coe_le_coe.1 (h z)

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ (m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n) ↔ m = findGreatest P 0

Tactic:
simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]

Goal state after:
case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ m = 0 → (¬m = 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n = 0 → ¬P n
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ DirectedOn r (Set.range f) ↔ Directed r f

Tactic:
simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b) ↔ -2 + 1 = ⅟b * a + ⅟a * b

Tactic:
by rw [← add_assoc, ← add_assoc, neg_add_cancel, zero_add]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl.inl
h h' : 1 * 1 = 1
⊢ 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl.inr
h : 1 * -1 = 1
h' : -1 * 1 = 1
⊢ 1 = 1 ∧ -1 = 1 ∨ 1 = -1 ∧ -1 = -1

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inr.inl
h : -1 * 1 = 1
h' : 1 * -1 = 1
⊢ -1 = 1 ∧ 1 = 1 ∨ -1 = -1 ∧ 1 = -1

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inr.inr
h h' : -1 * -1 = 1
⊢ -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s

Tactic:
rw [strictMonoOn_insert_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
rw [strictMonoOn_insert_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a

Tactic:
tauto

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b

pp: case refine_2
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s

pp: case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Tactic:
· suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩

Goal state after:
case refine_2
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s

case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
y : ↑(⇑e '' s)
⊢ e.symm ↑y ∈ s

Tactic:
rcases y with ⟨-, ⟨a, ⟨m, rfl⟩⟩⟩

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ e.symm ↑⟨e a, ⋯⟩ ∈ s
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
x : α
⊢ (ofInjective f hf).symm ⟨f x, ⋯⟩ = rangeSplitting f ⟨f x, ⋯⟩

Tactic:
apply hf

Goal state after:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
x : α
⊢ f ((ofInjective f hf).symm ⟨f x, ⋯⟩) = f (rangeSplitting f ⟨f x, ⋯⟩)
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB s (f.symm (f x)) ↔ IsLUB s x

Tactic:
f.symm_apply_apply

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB s x ↔ IsLUB s x
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t

Tactic:
tauto

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []

Tactic:
exact Forall₂.nil

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take l₁.length l) l₁

Tactic:
by
  have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
    forall₂_take (length l₁) h
  rwa [take_left] at h'

Goal state after: