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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b⁻¹ * a < c ↔ a < b * c

Tactic:
by
  rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ a * a⁻¹ < a * b ↔ 1 < a * b

Tactic:
by rw [mul_inv_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ b * a < b * b⁻¹ ↔ b * a < 1

Tactic:
by rw [mul_inv_cancel]

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c d : α
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

Tactic:
mul_comm c,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c d : α
⊢ a * b⁻¹ ≤ d⁻¹ * c ↔ a * d ≤ c * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b

Tactic:
mul_comm c,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a * b⁻¹ < d⁻¹ * c ↔ a * d < c * b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩; rw [mul_one]

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

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

Tactic:
by
  by_cases! h : a < 1
  · use a
    have : a * a < a * 1 := mul_lt_mul_right h a
    rw [mul_one] at this
    exact le_of_lt this
  · use 1
    rwa [mul_one]

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ c * a ≤ c * b

Tactic:
mul_comm c,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ c * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
h : a ≠ 0
⊢ 0 < a * a

Tactic:
rcases h.lt_or_gt with h | h

Goal state after:
case mpr.inl
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
h✝ : a ≠ 0
h : a < 0
⊢ 0 < a * a

case mpr.inr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
h✝ : a ≠ 0
h : 0 < a
⊢ 0 < a * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
⊢ 0 ≤ a * a

Tactic:
simpa only [sq] using sq_nonneg a

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 b : G₀
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
lt_div_iff₀ hb,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ 1 * b < a ↔ b < a
Module: Mathlib.Algebra.Order.Archimedean.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℕ
h : x < ↑n
⊢ x < ↑↑n

Tactic:
by rwa [Int.cast_natCast]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

Tactic:
rcases le_total 1 a with (ha | ha) <;> simp [ha]

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b < x ∧ x < a} = {x | x < a ∧ b < x}

Tactic:
by simp only [and_comm]

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b < x ∧ x ≤ a} = {x | x ≤ a ∧ b < x}

Tactic:
by simp only [and_comm]

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b ≤ x ∧ x < a} = {x | x < a ∧ b ≤ x}

Tactic:
by simp only [and_comm]

Goal state after:
Module: Mathlib.Order.Interval.Set.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ {x | b ≤ x ∧ x ≤ a} = {x | x ≤ a ∧ b ≤ x}

Tactic:
by simp only [and_comm]

Goal state after:
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 = 0 ^ n ∧ b = 0 ^ m

Tactic:
by have := h.symm; simp_all

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

Goal state before:
pp: β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)

Tactic:
ext x; induction x <;> rfl

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

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

Tactic:
add_comm a c,

Goal state after:
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : AddLeftMono α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a c : α
inst✝ : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - d = c + a - (c + d)
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ Nat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m

Tactic:
by
  simp only [← Nat.lt_succ_iff, find_lt_iff]

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:
by
  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.Order.WithBot

Goal state before:
pp: case none
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), none ≤ ↑a → x ≤ ↑a) ↔ x ≤ none

pp: case some
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
y : α
⊢ (∀ (a : α), Option.some y ≤ ↑a → x ≤ ↑a) ↔ x ≤ Option.some y

Tactic:
· simp [WithBot.none_eq_bot, eq_bot_iff_forall_le]

Goal state after:
case some
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
y : α
⊢ (∀ (a : α), Option.some y ≤ ↑a → x ≤ ↑a) ↔ x ≤ Option.some y
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
⊢ findGreatest P n ≤ findGreatest Q n

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
⊢ StrictMono Int.cast

Tactic:
obtain ⟨h⟩ : NeZero (1 : α) := inferInstance

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
h : 1 ≠ 0
⊢ StrictMono Int.cast
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

Tactic:
rw [floor_of_nonpos, floor_of_nonpos ha]

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ 0 / n = 0

case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ a * ↑n ≤ 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case inr.inl
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : 0 < b
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
· exact (hn.pow_nonpos ha).trans_lt (pow_pos hb _)

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n : ℕ
inst✝ : IsOrderedRing α
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n

Tactic:
induction n with

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |geomSum a b (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| + |b ^ (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)

Tactic:
abs_pow,

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
induction n with

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) * geomSum a b (n + 1)
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x ↦ x ∈ s
inst✝ : DecidablePred fun x ↦ x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), e ↑x = ↑(e₀ x) }
⊢ (fun e₁ ↦ ⟨Trans.trans (Trans.trans (Set.sumCompl s).symm (e₀.sumCongr e₁)) (Set.sumCompl t), ⋯⟩)
      ((fun e ↦ (↑e).subtypeEquiv ⋯) e) =
    e

Tactic:
ext x
    by_cases hx : x ∈ s
    · simp only [Set.sumCompl_symm_apply_of_mem hx, ← e.prop ⟨x, hx⟩, Sum.map_inl, sumCongr_apply,
        trans_apply, Set.sumCompl_apply_inl, Trans.trans]
    · simp only [Set.sumCompl_symm_apply_of_notMem hx, Sum.map_inr, subtypeEquiv_apply,
        Set.sumCompl_apply_inr, trans_apply, sumCongr_apply, Trans.trans]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds {a} ∩ upperBounds s = Ici a ∩ upperBounds s

Tactic:
upperBounds_singleton

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ Ici a ∩ upperBounds s = Ici a ∩ upperBounds s
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
lt_div_iff₀ hb,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 * b < a ↔ b < a
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ l[n] :: take 0 (drop (n + 1) l) = [l.get ⟨n, h⟩]

Tactic:
take

Goal state after:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ [l[n]] = [l.get ⟨n, h⟩]
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2

Tactic:
refine (inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))
  -- move `1 / a` to the left and `2⁻¹` to the right.
  rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]
  -- take inverses on both sides and use the assumption `2 ≤ a`.
  convert (one_div a).le.trans (inv_anti₀ zero_lt_two a2)
    -- show `1 - 1 / 2 = 1 / 2`.

  -- show `1 - 1 / 2 = 1 / 2`.
  rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd : a * b < d
⊢ c ≤ d

Tactic:
obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝ : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = 0 ↔ a = 0

Tactic:
simp [zpow']

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ zpow' 1 n = 1

Tactic:
simp [zpow']

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 1 = a

Tactic:
simp [zpow']

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = a / a

Tactic:
simp [zpow']

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : Group G
n : ℕ
f : ℕ → G
⊢ (map (fun k ↦ f k / f (k + 1)) (range n)).prod = f 0 / f n

Tactic:
induction n with

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

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a * b = 0 * b ↔ a = 0

Tactic:
Int.zero_mul,

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a * b = 0 ↔ a = 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
h : q.isInt = true
⊢ q = ↑q.num

Tactic:
Rat.isInt,

Goal state after:
q : ℚ
h : (q.den == 1) = true
⊢ q = ↑q.num
Module: Mathlib.Algebra.Field.Rat

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

Tactic:
rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_natCast]

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

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ q.toNNRat ≤ p.toNNRat ↔ q ≤ p

Tactic:
by
  simp [← coe_le_coe, toNNRat, hp]

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p : ℚ
q : ℚ≥0
hq : 0 < q
hp : p < 0
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
simp only [(hp.trans_le q.coe_nonneg).not_ge, toNNRat_eq_zero.2 hp.le, hq.not_ge]

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

Goal state before:
pp: case a
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ q₁.den

Tactic:
exact Nat.gcd_dvd_left _ _

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

Goal state before:
pp: ⊢ {0} ∪ range succ = univ

Tactic:
ext n

Goal state after:
n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ n ∈ univ
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case e'_4
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLinearOrder α
s : Set α
⊢ sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a

Tactic:
by
  rw [eq_top_iff, le_sSup_iff_forall_lt]

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
gi : GaloisInsertion l u
a b : β
⊢ l (u a) ⊔ l (u b) = a ⊔ b

Tactic:
simp only [gi.l_u_eq]

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
gi : GaloisInsertion l u
a b : β
⊢ l (u (a ⊓ b)) = a ⊓ b

Tactic:
simp only [gi.l_u_eq]

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

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Tactic:
have : Nonempty s := hs.to_subtype

Goal state after:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
this : Nonempty ↑s
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
g : (a : ↑(range fun x ↦ range (f x))) → ↑↑a
⊢ ⨅ a, ↑(g a) ≤ ⨅ i, f i ((fun a ↦ Classical.choose ⋯) i)

Tactic:
refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
g : (a : ↑(range fun x ↦ range (f x))) → ↑↑a
a : ι
⊢ ↑(g ⟨range (f a), ⋯⟩) ≤ f a ((fun a ↦ Classical.choose ⋯) a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₁, h₂⟩⟩.snd

Tactic:
subst a_eq

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₁, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn ⋯ ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₁, ⟨b₁, h₂⟩⟩.snd
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
a b : α
inst✝ : Fact (a < b)
x y : ↑(Ico a b)
⊢ Disjoint x y ↔ ↑x ⊓ ↑y = a

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint x y ↔ Disjoint ↑x ↑y

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a : α
x y : ↑(Ici a)
⊢ Disjoint x y ↔ ↑x ⊓ ↑y = a

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : SemilatticeInf α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ Disjoint x y ↔ ↑x ⊓ ↑y = a

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := e.completeLattice
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
⊢ Coframe α

Tactic:
apply e.injective.coframe

Goal state after:
case le
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_sSup
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sSup s) = ⨆ a ∈ s, e a

case map_sInf
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (s : Set α), e (sInf s) = ⨅ a ∈ s, e a

case map_top
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊤ = ⊤

case map_bot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ e ⊥ = ⊥

case map_hnot
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a : α), e (￢a) = ￢e a

case map_sdiff
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
completeLattice : CompleteLattice α := ⋯
coheytingAlgebra : CoheytingAlgebra α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
by
  classical
  constructor
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro a ha
      exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
    · rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
      · refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = ⨅ a ∈ s, ↑a

Tactic:
coe_sInf' hs h's,

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ sInf ((fun a ↦ ↑a) '' s) = ⨅ a ∈ s, ↑a