mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : ℕ
h : i < l.length - 1
⊢ i + 1 < l.length

Tactic:
lia

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
i : ℕ
hlen : i ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'
⊢ (l.insertIdx i a).prod = a * l.prod

Tactic:
by
  induction i generalizing l
  case zero => rfl
  case succ i ih =>
    obtain ⟨hd, tl, rfl⟩ := exists_cons_of_length_pos (Nat.zero_lt_of_lt hlen)
    simp only [insertIdx_succ_cons, prod_cons,
      ih (Nat.le_of_lt_succ hlen) (fun a' a'_mem => hcomm a' (mem_of_mem_tail a'_mem))]
    exact Commute.left_comm (hcomm hd (mem_of_mem_head? rfl)).symm tl.prod

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ l⁻¹.eval = l.eval⁻¹

Tactic:
simp +instances only [NF.eval, List.map_map, NF.instInv, List.prod_inv]

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ (map ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (-x.1, x.2)) l).prod = (map ((fun x ↦ x⁻¹) ∘ fun x ↦ zpow' x.2 x.1) l).prod
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ (map
        (fun x ↦
          match x with
          | (r, x) => zpow' x r)
        (l ^ r)).prod =
    zpow'
      (map
          (fun x ↦
            match x with
            | (r, x) => zpow' x r)
          l).prod
      r

Tactic:
simp only [zpow_apply, list_prod_zpow', map_map]

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ (map ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (r * x.1, x.2)) l).prod =
    (map ((fun x ↦ zpow' x r) ∘ fun x ↦ zpow' x.2 x.1) l).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
h : l.length = 1
⊢ 0 < l.length

Tactic:
lia

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f a (b :: l) = a

Tactic:
rw [foldl_cons, hf b, foldl_fixed' hf l]

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

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

Tactic:
simp [filterMap_cons]

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

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

Tactic:
simp [filterMap_cons]

Goal state after:
case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun a ↦ (f a).toList) l
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
n : ℕ
⊢ q ^ n = mkRat (q.num ^ n) (q.den ^ n)

Tactic:
by
  rw [pow_def, mk_eq_mkRat]

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

Goal state before:
pp: ⊢ 1 ≠ 0

Tactic:
lia

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

Goal state before:
pp: case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n * x /. (x * d) = n /. d

Tactic:
x.mul_comm,

Goal state after:
case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n * x /. (d * x) = n /. d
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: case inr
α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
· simp [hn, dvd_pow_self]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a b : α
inst✝ : Subsingleton αˣ
⊢ a ∣ b → b ∣ a → a = b

Tactic:
rintro ⟨c, rfl⟩ ⟨d, hcd⟩
  rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
  obtain ⟨rfl, -⟩ | rfl := hcd <;> simp

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den

Tactic:
rw [mul_def, normalize_eq]
  apply Nat.div_dvd_of_dvd
  apply Nat.gcd_dvd_right

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

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

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:
· norm_cast at hpq ⊢

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.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ False

Tactic:
have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = ↑d * ↑k
⊢ False
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b

Tactic:
rcases h with ⟨c, rfl⟩
  rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul,
    intCast_div_self, Int.cast_mul, mul_div_assoc]

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

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
this : 2 ≤ a
⊢ 0 < ↑a

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsNat (a ^ nb) ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, zpow_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsInt (a ^ nb) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, zpow_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsNat b nb
pe' : IsNNRat (a ^ nb) num den
⊢ IsNNRat (a ^ b) num den

Tactic:
rwa [pb.out, zpow_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, zpow_natCast]

Goal state after:
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
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b

Tactic:
rw [← mul_add, tsub_add_cancel_of_le hcb]

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

Goal state before:
pp: case inl
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)
hab : a ≤ b
⊢ 0 * c = a * c - b * c

Tactic:
zero_mul,

Goal state after:
case inl
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)
hab : a ≤ b
⊢ 0 = a * c - b * c
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ f '' {0} ∪ range (f ∘ succ) = range f

Tactic:
range_comp,

Goal state after:
α : Type u_1
f : ℕ → α
⊢ f '' {0} ∪ f '' range succ = range f
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:
apply (isGLB_sInf _).2

Goal state after:
α✝ : 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 ∈ lowerBounds {b, c}
Module: Mathlib.Order.CompleteLattice.Defs

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

Tactic:
le_sSup_iff_forall_lt

Goal state after:
α : Type u_1
inst✝ : CompleteLinearOrder α
s : Set α
⊢ (∀ b < ⊤, ∃ a ∈ s, b < a) ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))

Tactic:
range_comp,

Goal state after:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (iSup f))
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: case mp
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s ↦ ↑(f s y)) ⟨s, hs⟩ ∈ s

Tactic:
exact (f ⟨s, hs⟩ y).2

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
σ : Type u_13
s : ι → Set α
t : σ → Set α
⊢ ⋃ x, Sum.elim s t x = (⋃ x, s x) ∪ ⋃ x, t x

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
i : Set α
s : (a : α) → Set (π a)
⊢ i.pi s = ⋂ a ∈ i, eval a ⁻¹' s a

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ ⨅ i ∈ ⋃₀ S, p i ↔ ⨅ i ∈ S, ⨅ i_2 ∈ i, p i_2

Tactic:
iInf_sUnion

Goal state after:
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:
classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ a₁, e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
simpa only [onFun, extend_apply' _ _ _ hb₁] using! disjoint_bot_left

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a

Tactic:
by
  grind [Set.Pairwise]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
  rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt
  · exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩
  · exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h✝ : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑(num✝¹.mul db) * ⅟↑db * ⅟↑da ≤ ⅟↑db * (↑(num✝.mul da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
simp only [Nat.mul_eq, Nat.cast_mul, mul_invOf_cancel_right'] at h

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h✝ : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑num✝¹ * ⅟↑da ≤ ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + (n + 1))!

Tactic:
by
    rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]
    exact Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a⁺ᵐ = if 1 ≤ a then a else 1

Tactic:
by
  rw [oneLePart_def, ← maxDefault, ← sup_eq_maxDefault]; simp_rw [sup_comm]

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

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
⊢ 0 < n

Tactic:
lia

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

Goal state before:
pp: case refine_1
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i ≤ i + n

Tactic:
lia

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

Goal state before:
pp: case refine_2
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 0 < i + n

Tactic:
lia

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

Goal state before:
pp: case refine_3
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 1 < (i + n)!

Tactic:
lia

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

Goal state before:
pp: case refine_4
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ n + 1 ≤ i + n

Tactic:
lia

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

Goal state before:
pp: n m : ℕ
h : n ≤ m
k : ℕ
ih : n.ascFactorial k ≤ m.ascFactorial k
⊢ n + k ≤ m + k

Tactic:
lia

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

Goal state before:
pp: k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ n - m = n - k - (m - k)

Tactic:
lia

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

Goal state before:
pp: k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ m - k ≤ n - k

Tactic:
lia

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

Goal state before:
pp: k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ n < m

Tactic:
lia

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

Goal state before:
pp: k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ n - k < m - k

Tactic:
lia

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

Goal state before:
pp: k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ n < k

Tactic:
lia

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

Goal state before:
pp: n : ℕ
h : 0 + 2 ≤ n
⊢ n - (0 + 1) < n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n - (k + 1) < n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ 0 < n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
⊢ 2 ^ n * n ! ≤ (2 * n)!

Tactic:
by
  obtain _ | n := n
  · simp
  rw [Nat.mul_comm, Nat.two_mul]
  calc
    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) :=
      Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (le_add_left _ _) _)
    _ ≤ _ := Nat.factorial_mul_pow_le_factorial

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

Goal state before:
pp: n k : ℕ
⊢ n.ascFactorial k = n.ascFactorialBinary k

Tactic:
fun_induction ascFactorialBinary with
  | case1 => simp
  | case2 => simp [ascFactorial]
  | case3 n k ih₁ ih₂ => grind [ascFactorial_mul_ascFactorial]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl.inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(2 * m + 1) = 2 * x
⊢ round x = (2 * m + 1) / 2

Tactic:
refine absurd ?_ hx
      exact (mul_fract_eq_one_iff_exists_int one_lt_two).mpr ⟨m, mod_cast hm.symm⟩

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

Goal state before:
pp: case pos
a b : ℕ+
hab : a < b
h : 1 < b
⊢ ↑a ≤ ↑b - ↑1

Tactic:
exact Nat.le_pred_of_lt hab

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) ≤ ↑m ∧ ↑(m.mod k) ≤ ↑k

Tactic:
rw [mod_coe]

Goal state after:
m k : ℕ+
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑m ∧ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ 1 ≤ ↑m / ↑k

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
n : ℤ
⊢ round x = n ↔ x ∈ Ico (↑n - 1 / 2) (↑n + 1 / 2)

Tactic:
norm_num [round_eq, floor_eq_iff, ← lt_sub_iff_add_lt, add_sub_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ round (f a) = round a

Tactic:
simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
this : 0 < k ∧ k < 1
⊢ False

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
this : 0 < k ∧ k < 1
⊢ False

Tactic:
lia

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✝² : AddMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x + n • a) = f x + n • b

Tactic:
simpa using (AddConstMapClass.semiconj f).iterate_right n x

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

Goal state before:
pp: case h
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ n + 1 ≤ 0

Tactic:
lia

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ ∃ q, x < ↑q ∧ ↑q < y

Tactic:
refine ⟨(z : ℚ) / n, ?_, ?_⟩ <;> simpa

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

Goal state before:
pp: α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
⊢ l[i] = l[j] ↔ i = j

Tactic:
have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩

Goal state after:
α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
this : l.get ⟨i, hi⟩ = l.get ⟨j, hj⟩ ↔ ⟨i, hi⟩ = ⟨j, hj⟩
⊢ l[i] = l[j] ↔ i = j
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
t : α
⊢ map f ∘ cons t = cons (f t) ∘ map f

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0

Tactic:
map_eq_zero

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ s = 0 ↔ s = 0
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a l' + 1 ≤ 1
⊢ False

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
by_cases h : b ∈ l₂
    · simp [h]
    · simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

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

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
this : s.card < t.card
⊢ n - t.card < n - s.card

Tactic:
lia

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u

Tactic:
exact IH ((le_cons_of_notMem <| mt (mem_of_le h₂) h).1 h₁) h₂

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ t + s ∪ (u + s) = t + s ∪ (s + u)

Tactic:
s.add_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ t + s ∪ (u + s) = t + s ∪ (u + s)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ (t + s) ∩ (u + s) = (t + s) ∩ (s + u)

Tactic:
s.add_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ (t + s) ∩ (u + s) = (t + s) ∩ (u + s)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

Tactic:
· rw [cons_inter_of_neg _ h, sub_cons, erase_of_notMem h, IH]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.toList.toFinset = s

Tactic:
ext
  simp

Goal state after: