mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
⊢ Icc a b = Icc c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun heq ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  have h' : c ≤ d := by
    by_contra contra; rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq; contradiction
  simp only [Set.ext_iff, mem_Icc] at heq
  obtain ⟨-, h₁⟩ := (heq b).mp ⟨h, le_refl _⟩
  obtain ⟨h₂, -⟩ := (heq a).mp ⟨le_refl _, h⟩
  obtain ⟨h₃, -⟩ := (heq c).mpr ⟨le_refl _, h'⟩
  obtain ⟨-, h₄⟩ := (heq d).mpr ⟨h', le_refl _⟩
  exact ⟨le_antisymm h₃ h₂, le_antisymm h₁ h₄⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds s'
⊢ a ≤ b

Tactic:
by
  have ⟨x, hx, hx'⟩ := h
  exact le_trans (ha hx) (hb hx')

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l : ℕ
r : α
tl : ℕ
zl : ℤ
tr t : α
prl₁ : l = tl
prl₂ : ↑tl = zl
prr : r = tr
prt : smulg zl tr = t
⊢ smul l r = t

Tactic:
simp [← prt, prl₁, ← prl₂, prr, smul, smulg, natCast_zsmul]

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
⊢ 1 / a < b ↔ 1 / b < a

Tactic:
simpa using inv_lt_of_neg ha hb

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l → SublistForall₂ R l₁ l₂

Tactic:
induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.length
⊢ l[n] :: l.eraseIdx n ~ l

Tactic:
by
  simpa [h] using (set_perm_cons_eraseIdx h l[n]).symm

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

Goal state before:
pp: case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
exact SublistForall₂.cons_right (ih _ _ h1 btc)

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
by
  by_cases ha : a = 0
  · simp [ha]
  by_cases hn : n = 0
  · rw [hn]
    simp [zpow', ha, zpow_ne_zero ]
  by_cases hm : m = 0
  · rw [hm]
    simp [zpow', ha]
  simpa [zpow', ha, hm, hn] using zpow_mul a m n

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
a : M
inst✝ : DecidableEq M
ha : a ∈ l
comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
by
  induction l with
  | nil => simp only [not_mem_nil] at ha
  | cons b l ih =>
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
    · simp only [erase_cons_head, prod_cons]
    rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
l : List M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
⊢ l.prod = (map id l).prod

Tactic:
map_id

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
l : List M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
⊢ l.prod = l.prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map f (filter (fun b ↦ decide (p b)) l)).prod * (map f (filter (fun x ↦ decide ¬p x) l)).prod = (map f l).prod

Tactic:
← prod_map_ite

Goal state after:
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map (fun a ↦ if p a then f a else f a) l).prod = (map f l).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (map f) ∧ Surjective (map f) ↔ Injective f ∧ Surjective f

Tactic:
map_injective_iff,

Goal state after:
α : Type u
β : Type v
f : α → β
⊢ Injective f ∧ Surjective (map f) ↔ Injective f ∧ Surjective f
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
hq : q.den = 1
| q

Tactic:
rw [← num_divInt_den q, hq]

Goal state after:
q : ℚ
hq : q.den = 1
| q.num /. ↑1
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ x✝¹.succ = x✝ ^ x✝¹ * x✝

Tactic:
Rat.pow_succ

Goal state after:
x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ x✝¹ * x✝ = x✝ ^ x✝¹ * x✝
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a b : ℕ
⊢ divNat a b = ↑a / ↑b

Tactic:
by
  ext
  simp [Rat.mkRat_eq_div]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ OfScientific.ofScientific m b d = ↑(m * 10 ^ d)

Tactic:
rw [← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_def, if_neg ‹_›]

Goal state after:
case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑(OfNat.ofNat m * 10 ^ OfNat.ofNat d) = ↑(m * 10 ^ d)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ { num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den ∣
    q₁.den * q₂.den

Tactic:
apply Nat.div_dvd_of_dvd

Goal state after:
q₁ q₂ : ℚ
⊢ (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) ∣ q₁.den * q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ (q * q).num = q.num * q.num

Tactic:
rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]

Goal state after:
q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑p.den ≠ 0

pp: case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ↑q.den ≠ 0

pp: case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

pp: case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑p.den ≠ 0

pp: case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ↑q.den ≠ 0

Tactic:
any_goals norm_cast

Goal state after:
case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ¬p.den = 0

case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num * ↑q.den = ↑q.num * ↑p.den
⊢ ¬q.den = 0

case hbd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ Commute ↑p.den ↑q.den

case hb
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ¬p.den = 0

case hd
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ ¬q.den = 0
Module: Mathlib.Order.CompleteLattice.Lemmas

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
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sInf s).down = ⨅ a ∈ s, a.down

Tactic:
rw [sInf_eq_iInf', down_iInf, iInf_subtype'']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ f a ⊔ ⨆ x ∈ {b}, f x = f a ⊔ f b

Tactic:
iSup_singleton

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ f a ⊔ f b = f a ⊔ f b
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
π : α → Type u_12
ι : α → Type u_13
t : (a : α) → ι a → Set (π a)
⊢ (⋃ x, univ.pi fun a ↦ t a (x a)) = univ.pi fun a ↦ ⋃ j, t a j

Tactic:
ext
  simp [Classical.skolem]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs

Tactic:
rcases h with ⟨x, hr, hl⟩
      suffices rhs ≥ x from nomatch not_lt.2 this hr
      have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
      choose f hf using this
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => le_of_lt (hf a)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a, ⨆ (_ : ∃ i, a ∈ s i), f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j

Tactic:
iSup_exists

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s))
⊢ ↑(sInf s) = ↑(sInf ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s))

Tactic:
rw [preimage_image_eq]
    exact Option.some_injective _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a

Tactic:
by
  simp only [disjoint_iff, iSup_inf_eq, iSup_eq_bot]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : NoZeroDivisors α
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
⊢ ⟨a, ha⟩ * ⟨b, hb⟩ = 0 → ⟨a, ha⟩ = 0 ∨ ⟨b, hb⟩ = 0

Tactic:
simp only [mk_mul_mk, mk_eq_zero, mul_eq_zero, imp_self]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : CharZero α
num✝¹ num✝ denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul denom✝ = num✝.mul denom✝¹) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝

Tactic:
rw [NNRat.invOf_denom_swap]

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : CharZero α
num✝¹ num✝ denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul denom✝ = num✝.mul denom✝¹) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ g (Classical.choose hf) = 1

Tactic:
← notMem_mulSupport

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ ¬Classical.choose hf ∈ mulSupport g
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s

Tactic:
by
  rw [disjoint_comm, mulSupport_disjoint_iff]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
op : M → N → P
op1 : op 1 1 = 1
f : ι → M
g : ι → N
x : ι
hx : x ∈ mulSupport fun x ↦ op (f x) (g x)
hf : f x = 1
hg : g x = 1
⊢ (fun x ↦ op (f x) (g x)) x = 1

Tactic:
simp only [hf, hg, op1]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊓ 1⁻¹ = a ⊓ 1

Tactic:
inv_one

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊓ 1 = a ⊓ 1
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a✝ n✝ : ℕ
⊢ OfScientific.ofScientific (↑a✝) false ↑n✝ = ↑(a✝ * 10 ^ n✝)

Tactic:
by
    rw [NNRatCast.ofScientific_eq_ite, if_neg Bool.false_ne_true]
    norm_cast

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

Goal state before:
pp: case succ.zero
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : 0 < 0 + 1
hk : (m : ℕ+) → m < ⟨0 + 1, kprop⟩ → p m
⊢ p ⟨0 + 1, kprop⟩

pp: case succ.succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1 + 1
hk : (m : ℕ+) → m < ⟨k + 1 + 1, kprop⟩ → p m
⊢ p ⟨k + 1 + 1, kprop⟩

Tactic:
· exact hz

Goal state after:
case succ.succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1 + 1
hk : (m : ℕ+) → m < ⟨k + 1 + 1, kprop⟩ → p m
⊢ p ⟨k + 1 + 1, kprop⟩
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ fract (-x) = 1 - fract x

Tactic:
rw [fract_eq_iff]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b

Tactic:
by
  rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]

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

Goal state before:
pp: case h₁
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a ≤ ↑⌈a⌉

Tactic:
apply le_ceil

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

Goal state before:
pp: case h₂
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ b ≤ ↑⌈b⌉

Tactic:
apply le_ceil

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ 0 < 1 - b

Tactic:
by linarith

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

Goal state before:
pp: case pos
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x

pp: case neg
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x

Tactic:
· use 1
    simp only [pow_one]
    exact y_pos.trans_lt hx

Goal state after:
case neg
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a, b}.card = 2

Tactic:
by
  rw [insert_eq_cons, card_cons, card_singleton]

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
a✝ : ∀ (x : α), x ∈ 0 → r x x
⊢ Rel r 0 0

Tactic:
apply Rel.zero

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

Goal state before:
pp: α : Type u
a : α
l : List α
IH : (∀ (a : α), ¬[a, a] <+ l) → l.Nodup
h : ∀ (a_1 : α), ¬[a_1, a_1] <+ a :: l
⊢ (a :: l).Nodup

Tactic:
exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons
          fun al => h a <| (singleton_sublist.2 al).cons_cons _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ range (map f) = {l | ∀ (x : β), x ∈ l → x ∈ range f}

Tactic:
refine antisymm (range_subset_iff.2 fun l => forall_mem_map.2 fun y _ => mem_range_self _)
      fun l hl => ?_

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
l : List β
hl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ l ∈ range (map f)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s.erase a

Tactic:
rw [erase_of_notMem h]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
· simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
      rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
      simp [List.getLast_eq_getElem]

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α), b ∈ filter (fun a ↦ f x = f a) s → f x = f b

Tactic:
simp only [mem_filter, and_imp, @eq_comm _ (f x), imp_self, implies_true]

Goal state after:
Module: Mathlib.Data.Finset.SymmDiff

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \ t ⊔ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
sup_eq_union,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \ t ∪ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x : Prop), x ∈ { val := {True, False}, nodup := fintype._proof_1 }

Tactic:
simpa using em

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s

Tactic:
ext x
  simp [@and_comm _ (_ = _), @and_comm (p x) (x ∈ s)]

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

Goal state before:
pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
exact H

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
ha₂ : a₂ ∈ ↑s
⊢ f' a₁ = f' a₂ → a₁ = a₂

Tactic:
haa

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
ha₂ : a₂ ∈ ↑s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < b ↔ a ≤ b

Tactic:
by
  rw [pred_lt_iff, castSucc_lt_succ_iff]

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

Goal state before:
pp: n : ℕ
⊢ image succ univ = {0}ᶜ

Tactic:
by
  rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
append_left,

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = (u ∘ Fin.cast ⋯) (castAdd n l)
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ y :: l₁✝
⊢ x ∈+ y :: l₂✝

Tactic:
duplicate_cons_iff

Goal state after:
case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : y = x ∧ x ∈ l₁✝ ∨ x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
| cons _ _ IH =>

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑t

Tactic:
rw [← inter_eq_self_of_subset_right h]

Goal state after:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑(s ∩ t)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Antisymm r
x : α
xs : List α
hx : x ∈ xs
hxs : Pairwise r xs
⊢ orderedInsert r x (xs.erase x) = xs

Tactic:
by
  induction xs with grind +splitIndPred

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

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
ih : c.erase a <+ insertionSort r tail✝
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
hm : a ∈ c
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
have he := orderedInsert_erase _ _ hm hs

Goal state after:
case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
ih : c.erase a <+ insertionSort r tail✝
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
hm : a ∈ c
he : orderedInsert r a (c.erase a) = c
⊢ c <+ insertionSort r (a :: tail✝)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
⊢ ¬InjOn f s

Tactic:
have : Finite (f '' s) := finite_coe_iff.mpr h_fin

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this : Finite ↑(f '' s)
⊢ ¬InjOn f s
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedLE ↔ l.SortedGE

Tactic:
by
  grind [OrderDual.ofDual_le_ofDual]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedGE ↔ l.SortedLE

Tactic:
by
  grind [OrderDual.ofDual_le_ofDual]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ Pairwise R (a :: b :: l) ↔ R a b ∧ Pairwise R (b :: l)

Tactic:
simp_rw [← isChain_iff_pairwise, isChain_cons_cons]

Goal state after: