mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : Inhabited M
l : List M
h : l ≠ []
⊢ l.headI * l.tail.prod = l.prod

Tactic:
cases l

Goal state after:
case nil
M : Type u_4
inst✝¹ : Monoid M
inst✝ : Inhabited M
h : [] ≠ []
⊢ [].headI * [].tail.prod = [].prod

case cons
M : Type u_4
inst✝¹ : Monoid M
inst✝ : Inhabited M
head✝ : M
tail✝ : List M
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝).headI * (head✝ :: tail✝).tail.prod = (head✝ :: tail✝).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
⊢ l.head! = l.head?.getD default

Tactic:
cases l

Goal state after:
case nil
α : Type u
inst✝ : Inhabited α
⊢ [].head! = [].head?.getD default

case cons
α : Type u
inst✝ : Inhabited α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).head! = (head✝ :: tail✝).head?.getD default
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
k : ℕ
l : List α
h : k ≠ 0
hk : k < l.length
⊢ l[k] ∈ l.tail

Tactic:
cases l

Goal state after:
case nil
α : Type u
k : ℕ
h : k ≠ 0
hk : k < [].length
⊢ [][k] ∈ [].tail

case cons
α : Type u
k : ℕ
h : k ≠ 0
head✝ : α
tail✝ : List α
hk : k < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝)[k] ∈ (head✝ :: tail✝).tail
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ idxOf a l = 0 ↔ l = [] ∨ l.head? = some a

Tactic:
cases l

Goal state after:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ idxOf a [] = 0 ↔ [] = [] ∨ [].head? = some a

case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head✝ : α
tail✝ : List α
⊢ idxOf a (head✝ :: tail✝) = 0 ↔ head✝ :: tail✝ = [] ∨ (head✝ :: tail✝).head? = some a
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.getLast hl ∈ l.dropLast
⊢ l.length - 1 ≤ idxOf (l.getLast hl) l

Tactic:
by
    contrapose hl'
    rwa [mem_dropLast_iff_idxOf_lt <| getLast_mem hl, ← Nat.not_le]

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

Goal state before:
pp: d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ { num := 0, den := d, den_nz := h, reduced := w } = 0

Tactic:
congr; simp_all

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 α
⊢ map f (l.erase a) = (map f l).erase (f a)

Tactic:
have : (a == ·) = (f a == f ·) := by ext b; simp [finj.eq_iff]

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 (l.erase a) = (map f l).erase (f a)
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Tactic:
mul_mul_mul_comm,

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * a₂ * (b * c)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a a' : α
h : a = a'
b : α
⊢ a • b = a' * b

Tactic:
by
  subst h
  rfl

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))

Tactic:
mul_lt_mul_iff_right₀,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (bd * a' < ad * b')

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
have p : x ∈ ⊤ := Set.mem_univ x

Goal state after:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : x ∈ ⊤
⊢ ∃ i ∈ t, x ∈ s i
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃ i ∈ s, i

Tactic:
← sUnion_image,

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃₀ ((fun i ↦ i) '' s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = sInf ((fun a ↦ ↑a) '' s)

Tactic:
obtain ⟨x, hx⟩ := hs

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) = sInf ((fun a ↦ ↑a) '' s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
⊢ BddAbove t

Tactic:
rcases B with ⟨b, hb⟩ | hB

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
⊢ BddAbove t

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
hB : BddAbove t
⊢ BddAbove t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
hb : BddAbove s
⊢ a < sSup s ↔ ∃ b ∈ s, a < b

Tactic:
simpa only [not_le, not_forall₂, exists_prop] using (csSup_le_iff' hb).not

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

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

pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)

Tactic:
· 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)

Goal state after:
case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ∀ (t : Set α), t ⊆ f i → t ⊆ f j → t ⊆ ⊥
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
simp only [not_forall] at h

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ∃ x h x_1 h h x_2 h x, ¬x_2 ⊆ ⊥
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
← pairwise_univ

Goal state after:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
← pairwise_univ

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Tactic:
intro x

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
⊢ x ∈ s → ∀ y ∈ s, x ≤ y → Icc x y ⊆ s
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑e '' s).OrdConnected

Tactic:
erw [(e : α ≃o β).image_eq_preimage_symm]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑(↑e).symm ⁻¹' s).OrdConnected
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
⊢ ∀ (a : α), False

Tactic:
intro x

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
h' : s = ∅
x : α
⊢ False
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
⊢ s.Subsingleton

Tactic:
intro x

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
⊢ x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
⊢ ∀ (a : α), False

Tactic:
intro x

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
x : α
⊢ False
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
⊢ n ! < m !

Tactic:
induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case zero
l k : ℕ
⊢ ascFactorial 0 l * (0 + l).ascFactorial k = ascFactorial 0 (l + k)

Tactic:
cases l

Goal state after:
case zero.zero
k : ℕ
⊢ ascFactorial 0 0 * (0 + 0).ascFactorial k = ascFactorial 0 (0 + k)

case zero.succ
k n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) * (0 + (n✝ + 1)).ascFactorial k = ascFactorial 0 (n✝ + 1 + k)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 0).descFactorial 0 = (n + 1).ascFactorial 0

Tactic:
by rw [ascFactorial_zero, descFactorial_zero]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 0 - 1).descFactorial 0 = n.ascFactorial 0

Tactic:
by rw [ascFactorial_zero, descFactorial_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ (↑p.num * (↑p.den)⁻¹) ^ n = (↑p.num / ↑p.den) ^ n

Tactic:
← div_eq_mul_inv

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ (↑p.num / ↑p.den) ^ n = (↑p.num / ↑p.den) ^ n
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ (↑q.num * (↑q.den)⁻¹) ^ n = (↑q.num / ↑q.den) ^ n

Tactic:
← div_eq_mul_inv

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ (↑q.num / ↑q.den) ^ n = (↑q.num / ↑q.den) ^ n
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑(m.mod k) = ↑k
⊢ ↑m % ↑k = 0

Tactic:
rw [mod_coe, if_neg h'] at h

Goal state after:
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0
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
a : R
⊢ ↑⌊a⌋ = a ↔ a ∈ range Int.cast

Tactic:
by
  aesop

Goal state after:
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
s : Set R
x : R
m : ℤ
hms : x - ↑m ∈ s
hm0 : 0 ≤ x - ↑m
hm1 : x - ↑m < 1
⊢ fract x ∈ s

Tactic:
obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
hms : x - ↑⌊x⌋ ∈ s
hm0 : 0 ≤ x - ↑⌊x⌋
hm1 : x - ↑⌊x⌋ < 1
⊢ fract x ∈ s
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
a : R
⊢ ↑⌈a⌉ = a ↔ a ∈ range Int.cast

Tactic:
by
  aesop

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMagma G
inst✝¹ : Add H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f (x + a) = f x + b

Tactic:
map_add_const

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMagma G
inst✝¹ : Add H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f x + b = f x + b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + 1

Tactic:
rw [← Int.cast_one, ← Int.cast_add]

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑(⌊a⌋ + 1)
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℤ
⊢ f (n • a) = f 0 + n • b

Tactic:
simpa using map_add_zsmul f 0 n

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

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ round (↑n * (↑d)⁻¹) = ↑(round (↑n / ↑d))

Tactic:
← div_eq_mul_inv

Goal state after:
R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ round (↑n / ↑d) = ↑(round (↑n / ↑d))
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: 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 : 1 < y
he : ∃ m, y ^ m ≤ x
hb : ∃ b, ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
n : ℤ
hn₁ : y ^ n ≤ x
hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩

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 : k
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋

Tactic:
div_eq_inv_mul

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ (pointReflection x) y = (Equiv.symm (pointReflection x)) y

Tactic:
rw [pointReflection_symm]

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

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
⊢ ∀ (x : WithBot M) {y : WithBot M}, 0 < y → ∃ n, x ≤ n • y

Tactic:
intro x

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x : WithBot M
⊢ ∀ {y : WithBot M}, 0 < y → ∃ n, x ≤ n • y
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
⊢ ∀ (x : WithZero M) {y : WithZero M}, 1 < y → ∃ n, x ≤ y ^ n

Tactic:
intro x

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
x : WithZero M
⊢ ∀ {y : WithZero M}, 1 < y → ∃ n, x ≤ y ^ n
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s : Multiset α
nodup✝¹ : s.Nodup
t : Multiset α
nodup✝ : t.Nodup
h : { val := s, nodup := nodup✝¹ }.val = { val := t, nodup := nodup✝ }.val
⊢ { val := s, nodup := nodup✝¹ } = { val := t, nodup := nodup✝ }

Tactic:
by cases h; rfl

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

Goal state before:
pp: case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?

Tactic:
exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩

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

Goal state before:
pp: α : Type u_1
l : List α
d : α
⊢ (range fun n ↦ l[n]?.getD d) = (fun o ↦ o.getD d) '' range fun x ↦ l[x]?

Tactic:
by
      simp only [← range_comp, Function.comp_def]
      rfl

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

Goal state before:
pp: case cons
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
by_cases hx : tl = [x]

Goal state after:
case pos
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
hne : l ≠ []
hnd : l.Nodup
⊢ l.head hne = l.getLast hne ↔ ∃ x, l = [x]

Tactic:
cases l

Goal state after:
case nil
α : Type u
hne : [] ≠ []
hnd : [].Nodup
⊢ [].head hne = [].getLast hne ↔ ∃ x, [] = [x]

case cons
α : Type u
head✝ : α
tail✝ : List α
hne : head✝ :: tail✝ ≠ []
hnd : (head✝ :: tail✝).Nodup
⊢ (head✝ :: tail✝).head hne = (head✝ :: tail✝).getLast hne ↔ ∃ x, head✝ :: tail✝ = [x]
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → m1.card = card 0 → Rel r m1 0

pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → m1.card = s.card → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → m1.card = (a ::ₘ s).card → Rel r m1 (a ::ₘ s)

Tactic:
· intro m _h hc
    rw [rel_zero_right, ← card_eq_zero, hc, card_zero]

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → m1.card = s.card → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → m1.card = (a ::ₘ s).card → Rel r m1 (a ::ₘ s)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mp
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t) → map f s = b ::ₘ t

pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t

Tactic:
· rintro ⟨a, ha, rfl, rfl⟩
    rw [← map_cons, Multiset.cons_erase ha]

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case e_tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ ∀ (x : α), x ∈ l → elem x (take n l) = elem x (b :: List.filter (fun a ↦ elem a (take n l)) l)

Tactic:
intro x

Goal state after:
case e_tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
x : α
⊢ x ∈ l → elem x (take n l) = elem x (b :: List.filter (fun a ↦ elem a (take n l)) l)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ l.dedup ↔ a ∈ l

pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, x ≠ z → x ≠ y ∨ y ≠ z

Tactic:
· simpa only [dedup, forall_mem_ne, not_not] using this

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, x ≠ z → x ≠ y ∨ y ≠ z
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, x ≠ z → x ≠ y ∨ y ≠ z

Tactic:
intro x

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x : α
⊢ ∀ {y z : α}, x ≠ z → x ≠ y ∨ y ≠ z
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ [].bagInter l = []

Tactic:
cases l

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].bagInter [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ [].bagInter (head✝ :: tail✝) = []
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.bagInter [] = []

Tactic:
cases l

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].bagInter [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).bagInter [] = []
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
by_cases h₁ : x ∈ t₁
    · have h₂ : x ∉ t₂ := h h₁
      simp [*]
    by_cases h₂ : x ∈ t₂
    · simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
      exact perm_cons_append_cons _ l_ih
    · simp [*]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
_h : t < s
⊢ t.card < s.card

Tactic:
decreasing_by exact card_lt_card _h

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

Goal state before:
pp: case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
⊢ s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a

Tactic:
hs'

Goal state after:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
⊢ n < s'.card → ∃ a, a ∈ s' ∧ ¬P a
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
⊢ ∀ {a_1 : ℕ}, a_1 ∈ range a → ¬a_1 ∈ map (fun x ↦ a + x) m

Tactic:
intro x

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
⊢ x ∈ range a → ¬x ∈ map (fun x ↦ a + x) m