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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x

Tactic:
and_iff_left_of_imp h.trans',

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ b ≤ x ∨ x ≤ a ↔ x ≤ a ∨ b ≤ x
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
hx : 1 < x
n : ℕ
hn : 0 < ↑n
⊢ 1 < x ^ n

Tactic:
exact one_lt_pow' hx (Int.natCast_pos.mp hn).ne'

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 c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))

Tactic:
← inf_sup_right,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
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 * (m * r % k) % k = r % k

Tactic:
rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]

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

Goal state before:
pp: 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
⊢ a * ↑p.succ + a_n / ↑q.succ * ↑q.succ * ↑p.succ + b_n * ↑q.succ = ↑n

Tactic:
← add_mul,

Goal state after:
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
⊢ (a + a_n / ↑q.succ * ↑q.succ) * ↑p.succ + b_n * ↑q.succ = ↑n
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a ≠ a * c

Tactic:
← (self_le_mul_right a c).lt_iff_ne

Goal state after:
case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a < a * c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithBot α
inst✝ : IsRightCancelAdd α
hz : z ≠ ⊥
⊢ x + z = y + z ↔ x = y

Tactic:
by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]

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

Goal state before:
pp: case pos.mpr
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ (m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n) → k + 1 = m

Tactic:
· rintro ⟨hle, h0, hm⟩
        rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
        exacts [(hm hlt (le_refl _) hk).elim, rfl]

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

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P k = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
ihk

Goal state after:
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) ↔
    m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
z : α
hlt : ↑z < ↑(unzero hx)
⊢ ∃ y, y ≠ 0 ∧ y < x

Tactic:
WithZero.coe_unzero hx

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
z : α
hlt : ↑z < x
⊢ ∃ y, y ≠ 0 ∧ y < x
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 z : WithBot α
⊢ x ≤ z →
    y ≤ z →
      (match x, y with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        z

Tactic:
by cases x <;> cases y <;> cases z <;> simp; simpa using sup_le

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a✝ n✝ : ℕ
x✝ : 0 ≤ a✝
⊢ n✝ ≤ id a✝ ↔ ↑n✝ ≤ a✝

Tactic:
rw [Nat.cast_id, id_def]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
n a : ℕ
⊢ id n ≤ a ↔ n ≤ ↑a

Tactic:
rw [Nat.cast_id, id_def]

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

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

Tactic:
by cases x <;> cases y <;> cases z <;> simp; simpa using sup_le

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x ≤ ↑(Multiplicative.ofAdd a) ↔ x ≤ exp a

Tactic:
exp

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x ≤ ↑(Multiplicative.ofAdd a) ↔ x ≤ ↑(Multiplicative.ofAdd a)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x < ↑(Multiplicative.ofAdd a) ↔ x < exp a

Tactic:
exp

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x < ↑(Multiplicative.ofAdd a) ↔ x < ↑(Multiplicative.ofAdd a)
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 z : WithTop α
⊢ x ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) x y ≤ z

Tactic:
by cases x <;> cases y <;> cases z <;> simp; simpa using sup_le

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
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + 1

Tactic:
← Nat.cast_one,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + ↑1
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
⊢ ⌊1⌋₊ = 1

Tactic:
← Nat.cast_one,

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + 1

Tactic:
← Nat.cast_one,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + ↑1
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
⊢ ⌈1⌉₊ = 1

Tactic:
← Nat.cast_one,

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

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
· rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ si * r = 1

Tactic:
hsi,

Goal state after:
α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ ⅟r * r = 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ r * si = 1

Tactic:
hsi,

Goal state after:
α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ r * ⅟r = 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ ⅟c * a = b ↔ a = c * b

Tactic:
rw [← mul_right_inj_of_invertible (c := c), mul_invOf_cancel_left]

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)
⊢ ⅟(a + b) = ⅟a + ⅟b ↔ ⅟(a + b) * (a + b) = (⅟a + ⅟b) * (a + b)

Tactic:
mul_left_inj_of_invertible

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ ⅟(a + b) = ⅟a + ⅟b ↔ ⅟(a + b) = ⅟a + ⅟b
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ f 0 = g 0

Tactic:
map_zero,

Goal state after:
case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ 0 = g 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
n : ℕ
hx : 0 ≤ x
hy : 0 ≤ y
hn : n ≠ 0
⊢ x ^ n + y ^ n ≤ (x + y) ^ n

Tactic:
rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩

Goal state after:
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
hn : k + 1 ≠ 0
⊢ x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a / b + b * c / (b * d)

Tactic:
hbc.eq,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a / b + c * b / (b * d)
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ (↑u).natAbs * (↑u⁻¹).natAbs = 1

Tactic:
← natAbs_mul,

Goal state after:
u : ℤˣ
⊢ (↑u * ↑u⁻¹).natAbs = 1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ (↑u⁻¹).natAbs * (↑u).natAbs = 1

Tactic:
← natAbs_mul,

Goal state after:
u : ℤˣ
⊢ (↑u⁻¹ * ↑u).natAbs = 1
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ b - a / c = (b * c - a) / c

Tactic:
by
  simpa using div_sub_div b a one_ne_zero hc

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → (fun b ↦ f a b) '' t ⊆ u

Tactic:
image_subset_iff,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → t ⊆ (fun b ↦ f a b) ⁻¹' u
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → (fun a ↦ f a b) '' s ⊆ u

Tactic:
image_subset_iff,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → s ⊆ (fun a ↦ f a b) ⁻¹' u
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
⊢ image2 f (range g) (range h) = range fun x ↦ f (g x.1) (h x.2)

Tactic:
by
  simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)

Tactic:
geomSum,

Goal state after:
case succ
α : Type u_1
inst✝ : CommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (a * geomSum a b n + b ^ (n + 1))
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ ⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s

Tactic:
image_subset_iff,

Goal state after:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ t ⊆ ⇑e.symm ⁻¹' s ↔ t ⊆ ⇑e '' s
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
y' : α
hy' : y' ∈ t
hyy' : y ≤ y'
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨z, hz, hx'z, hy'z⟩ := ht x' hx' y' hy'

Goal state after:
case refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
y' : α
hy' : y' ∈ t
hyy' : y ≤ y'
z : α
hz : z ∈ t
hx'z : x' ≤ z
hy'z : y' ≤ z
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case neg
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∀ j ∈ upperBounds (Iio i), i ≤ j
⊢ i ∈ lowerBounds (upperBounds (Iio i))

Tactic:
rw [mem_lowerBounds]

Goal state after:
case neg
γ : Type u_3
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∀ j ∈ upperBounds (Iio i), i ≤ j
⊢ ∀ x ∈ upperBounds (Iio i), i ≤ x
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ IsLeast {w | a ≤ b ⊔ w} (a \ b)

Tactic:
by
  simp [IsLeast, mem_lowerBounds]

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (f a b) nc dc

Tactic:
hf,

Goal state after:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a - b) nc dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / c * c ≤ a ↔ b ≤ a

Tactic:
div_mul_cancel₀ _ hc.ne

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b ≤ a ↔ b ≤ a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / c * c < a ↔ b < a

Tactic:
div_mul_cancel₀ _ hc.ne

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b < a ↔ b < a
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ (pmap f l hl).insertIdx 0 (f a ha) = pmap f (l.insertIdx 0 a) ⋯

Tactic:
cases l <;> simp

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

Goal state before:
pp: case mp.nil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l✝ : List β
⊢ ∃ l, Forall₂ R [] l ∧ l <+ l✝

Tactic:
exact ⟨nil, Forall₂.nil, nil_sublist _⟩

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

Goal state before:
pp: case nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a✝ : List α
h1 : SublistForall₂ Rₐ a✝ []
⊢ SublistForall₂ Rₐ a✝ []

Tactic:
exact h1

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
⊢ l[0]?.getD 1 * l.tail.prod = l.prod

Tactic:
cases l <;> simp

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
· simp [zpow', ha, zpow_add₀]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval

Tactic:
rw [eval_pow, hx]
  rw [zpow'_ofNat _ hr]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ a == x) l) = eraseP (fun x ↦ f a == x) (map f l)

Tactic:
eraseP_map,

Goal state after:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ a == x) l) = map f (eraseP ((fun x ↦ f a == x) ∘ f) l)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
rw [← coe_inj]

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁) = ↑(divNat n₂ d₂) ↔ n₁ * d₂ = n₂ * d₁
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
Int.isSquare_natCast_iff

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat (n₁ * ↑d + n₂ * ↑d) (d * d) = mkRat (n₁ + n₂) d

Tactic:
← add_mul,

Goal state after:
n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat ((n₁ + n₂) * ↑d) (d * d) = mkRat (n₁ + n₂) d
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q / r) = ↑q / ↑r

Tactic:
rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _),
    inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
rw [add_def', cast_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
    (Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ a * 0 < b * d

pp: case inr
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d

Tactic:
· rw [mul_zero]
    exact mul_pos hab.pos hcd

Goal state after:
case inr
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b) * c + b * c = a * c

Tactic:
← add_mul,

Goal state after:
case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b + b) * c = a * c
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ a ≤ sInf {b, c}

Tactic:
by
    apply (isGLB_sInf _).2
    simp [*]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
this : InfSet α := { sInf := fun s ↦ if hs : s.Nonempty then ⋯.min s hs else ⊥ }
s : Set α
x✝ : BddBelow s
hn : s.Nonempty
⊢ IsGLB s (sInf s)

Tactic:
simp only [dif_pos hn]
      exact IsLeast.isGLB ⟨h.wf.min_mem s hn, fun _ hx ↦ h.wf.min_le hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
i₀ : β
⊢ ⨆ i, f i = f i₀ ⊔ ⨆ i, ⨆ (_ : i ≠ i₀), f i

Tactic:
convert! iSup_split f (fun i => i = i₀)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
i₀ : β
⊢ f i₀ = ⨆ i, ⨆ (_ : i = i₀), f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set (WithTop α)
h : ¬BddAbove (some ⁻¹' s)
hmem : ⊤ ∈ s
⊢ sSup s = ⊤

Tactic:
exact sSup_of_top_mem hmem

Goal state after: