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

Goal state before:
pp: case neg
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
ha : a ≤ 0
⊢ 0 < a

Tactic:
grind [mul_le_mul_of_nonpos_right hbc ha]

Goal state after:
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
⊢ a < b * c⁻¹ ↔ c * a < b

Tactic:
by
  rw [lt_mul_inv_iff₀ hc, mul_comm]

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

Goal state before:
pp: case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
induction ac with | intro _ _ IH => ?_

Goal state after:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x✝⟧
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
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α × γ},
    Prod.Lex s u ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } b) ↔
      Prod.Lex r t a b

Tactic:
simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]

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 β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
⊢ ∀ (a : α), a = g (f a)

Tactic:
intro
    rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]

Goal state after:
Module: Mathlib.Data.Nat.Cast.NeZero

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 ≤ n

Tactic:
have := NeZero.ne n; lia

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑(y ^ n) = ↑1
hm : ↑(y ^ (m + 1)) = ↑1
⊢ ↑(y ^ (m + 1).gcd n) = ↑1

Tactic:
← zpow_natCast,

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑(y ^ ↑n) = ↑1
hm : ↑(y ^ ↑(m + 1)) = ↑1
⊢ ↑(y ^ ↑((m + 1).gcd n)) = ↑1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases m = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| a ^ 1

Tactic:
← zpow_natCast,

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| a ^ ↑1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| b ^ 1

Tactic:
← zpow_natCast,

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
| b ^ ↑1
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * a = b * 0

Tactic:
ha

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * 0 = b * 0
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ a * b = 0 * b

Tactic:
ha

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ 0 * b = 0 * b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommMonoidWithTop α
a : α
ha : a ≠ ⊤
⊢ IsAddRegular a

Tactic:
by
  simpa using LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top ha

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a - b
h₂ : 0 < b
h : a - b = a
⊢ False

Tactic:
tsub_pos_iff_lt

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝ : AddMonoid α
⊢ (match ⊤, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0

Tactic:
simp [zero_nsmul]

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

Goal state before:
pp: case coe
α : Type u
β : Type v
inst✝ : AddMonoid α
a✝ : α
⊢ (match ↑a✝, 0 with
    | Option.some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    0

Tactic:
simp [zero_nsmul]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
⊢ 0 ≤ x + ↑n

Tactic:
by
    have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
    rwa [neg_add_cancel] at this

Goal state after:
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
hnm : n ≤ m
⊢ p (m - n + n)

Tactic:
Nat.sub_add_cancel hnm

Goal state after:
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
hnm : n ≤ m
⊢ p m
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithBot α
⊢ x ≤
    match x, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

Tactic:
by cases x <;> cases y <;> simp

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

Goal state before:
pp: m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
⊢ P (findGreatest P n)

Tactic:
by_cases h : Nat.findGreatest P n = 0
  · cases m
    · rwa [h]
    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim
  · exact (findGreatest_eq_iff.1 rfl).2.1 h

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithBot α
⊢ y ≤
    match x, y with
    | none, none => ⊥
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊔ b)

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithTop α
⊢ (match x, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    x

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithTop α
⊢ (match x, y with
    | none, none => ⊤
    | Option.some a, none => ↑a
    | none, Option.some b => ↑b
    | Option.some a, Option.some b => ↑(a ⊓ b)) ≤
    y

Tactic:
by cases x <;> cases y <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y : WithZero α
⊢ x ≤
    match x, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ x

Tactic:
by cases x <;> cases y <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y : WithZero α
⊢ y ≤
    match x, y with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y : WithBot α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ y

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithTop α
⊢ x ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
by cases x <;> cases y <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ x

Tactic:
by cases x <;> cases y <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) x y ≤ y

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ ⌊0⌋₊ = 0

Tactic:
← Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ ⌊↑0⌋₊ = 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ ⌈0⌉₊ = 0

Tactic:
← Nat.cast_zero,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ ⌈↑0⌉₊ = 0
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Tactic:
· obtain ⟨w, hws, hwr⟩ := hd x hx y hy
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
⊢ a ∈ Set.univ.pi d →
    ∀ y ∈ Set.univ.pi d,
      ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) y z

Tactic:
ha

Goal state after:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
⊢ ∀ y ∈ Set.univ.pi d,
    ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) y z
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithBot α
⊢ WithBot.toDual x ≤ WithBot.toDual y ↔ y ≤ x

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ WithBot.toDual x < WithBot.toDual y ↔ y < x

Tactic:
by cases x <;> cases y <;> simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x < WithBot.ofDual y ↔ y < x

Tactic:
by cases x <;> cases y <;> simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
obtain ⟨ib⟩ := hb.nonempty_invertible

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
obtain ⟨ib⟩ := hb.nonempty_invertible

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Module: Mathlib.Algebra.Field.Basic

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

Tactic:
rw [← mul_eq_one_iff_inv_eq₀ ha, ← pow_two, sq_eq_one_iff]

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a = 1 ∨ a = -1 ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
⊢ a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f₂ a ≤ f₂ b

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
⊢ ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f₂ a ≤ f₂ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
⊢ a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f₂ a < f₂ b

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
⊢ ∀ ⦃b : α⦄, b ∈ s → a < b → f₂ a < f₂ b
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ RightInverse (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)) (Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯)

Tactic:
rintro ⟨⟨_⟩, ⟨_⟩⟩; rfl

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
h : IsWellOrder α r
s : Set α
hs : s.Nonempty
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

pp: case refine_2
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
⊢ WellFounded r

pp: case refine_3
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ ¬r a b → ¬r b a → a = b

Tactic:
· grind [h.wf.has_min, trichotomous_of r]

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
⊢ WellFounded r

case refine_3
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ ¬r a b → ¬r b a → a = b
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.12
a : α
x✝ : ↑{a}
x : α
h : x ∈ {a}
⊢ (fun x ↦ ⟨a, ⋯⟩) ((fun x ↦ PUnit.unit) ⟨x, h⟩) = ⟨x, h⟩

Tactic:
by
    subst x
    rfl

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
simpa using inv_lt_inv_of_neg ha (inv_lt_zero'.2 hb)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ Forall₂ (fun a b ↦ p a ∧ R a b) (a :: l) u ↔ (∀ (a_1 : α), a_1 ∈ a :: l → p a_1) ∧ Forall₂ R (a :: l) u

Tactic:
simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc,
      exists_and_left]

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ (p a ∧ ∃ x, R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ x_1, Forall₂ R l x_1 ∧ u = x :: x_1) ↔
    p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ b, R a b ∧ ∃ x, Forall₂ R l x ∧ u = b :: x
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : b ≠ a
⊢ idxOf a (b :: l) = (idxOf a l).succ

Tactic:
by
  simp [idxOf_cons, beq_false_of_ne h]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
l : List α
⊢ filterMap f l = flatMap (fun a ↦ (f a).toList) l

Tactic:
induction l with | nil => ?_ | cons a l ih => ?_ <;> simp [filterMap_cons]
  rcases f a <;> simp [ih]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case h₁
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

pp: case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d

Tactic:
· simp [div_def', Rat.divInt_le_divInt b_pos d_pos]

Goal state after:
case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = ↑↑q.num / ↑(↑q).den

Tactic:
← NNRat.num_coe

Goal state after:
q : ℚ≥0
⊢ ↑q = ↑(↑q).num / ↑(↑q).den
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋂ x, ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ x, ⋂ (h : p x), s x ⋯

Tactic:
simp only [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i

Tactic:
by
  simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) = sSup ((fun a ↦ ↑a) '' s)

Tactic:
by
  classical
  change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ min a b = if a ≤ b then a else b

Tactic:
rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)

Goal state after:
case neg.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₁ : a ≤ b
⊢ min a b = if a ≤ b then a else b

case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ min a b = if a ≤ b then a else b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ max a b = if a ≤ b then b else a

Tactic:
rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)

Goal state after:
case neg.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₁ : a ≤ b
⊢ max a b = if a ≤ b then b else a

case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ max a b = if a ≤ b then b else a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup s = sSup univ

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove univ
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
⊢ a ∈ (fun a ↦ ↑a) ⁻¹' s → a ≤ b

Tactic:
ha

Goal state after:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
⊢ a ∈ (fun a ↦ ↑a) ⁻¹' s → a ≤ b

Tactic:
ha

Goal state after:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
⊢ a ∈ s → ⊤ ≤ a

Tactic:
ha

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
ha : a ∈ s
⊢ ⊤ ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
⊢ a ∈ t → sInf (f '' s) ≤ f a

Tactic:
ha

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
⊢ sInf (f '' s) ≤ f a