mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

pp: case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
· rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
    exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)

Goal state after:
case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ 0 = FloorSemiring.floor a

pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0

Tactic:
H₂.floor_of_neg

Goal state after:
case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ 0 = 0

case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0

case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ a < 0
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc : 0 ≤ c
a b : G₀
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
obtain (rfl | hc) := hc.eq_or_lt
  · simp
  · exact (OrderIso.mulRight₀ c hc).map_inf a b

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n)

Tactic:
rw [pow_succ' _ n, pow_succ' _ n]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
⊢ (a + b) / c = a / c + b / c

Tactic:
by simp_rw [div_eq_mul_inv, add_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
⊢ IsCoinitialFor (f '' s) (f '' t)

Tactic:
simp only [IsCoinitialFor, forall_mem_image, exists_mem_image]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
⊢ ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x_1 ≤ f x
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : β
x : α
h' : Sum.inl x = Sum.inr val✝
⊢ False

Tactic:
cases h'

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : α
x : β
h' : Sum.inr x = Sum.inl val✝
⊢ False

Tactic:
cases h'

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * db + nb * da = k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
simpa using invertibleMul (da:α) db

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
simpa using invertibleMul (da:α) db

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

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

Tactic:
by
  simpa using one_div_le_one_div_of_le (by simpa) h

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
l : List ι
⊢ (map (fun x ↦ 1) l).prod = 1

Tactic:
by
  induction l with simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
simpa using invertibleMul (da:α) db

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
simpa using invertibleMul (da:α) db

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (take n l).tail = take (n - 1) l.tail

Tactic:
ext
  grind

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (take n l).dropLast = take (n - 1) l.dropLast

Tactic:
ext
  grind

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (drop n l).tail = drop n l.tail

Tactic:
ext
  grind

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (drop n l).dropLast = drop n l.dropLast

Tactic:
ext
  grind

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

Goal state before:
pp: case zero
α : Type u
m : ℕ
xs : List α
⊢ dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs

Tactic:
cases xs with

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

Goal state before:
pp: case succ
α : Type u
m n✝ : ℕ
a✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
xs : List α
⊢ dropSlice (n✝ + 1) m xs = take (n✝ + 1) xs ++ drop (n✝ + 1 + m) xs

Tactic:
cases xs with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂

Tactic:
induction h

Goal state after:
case nil
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
⊢ Forall₂ S [] []

case cons
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S (a✝² :: l₁✝) (b✝ :: l₂✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp
α : Type u_1
a b : List α
h : Forall₂ (fun x1 x2 ↦ x1 = x2) a b
⊢ a = b

Tactic:
induction h

Goal state after:
case mp.nil
α : Type u_1
a b : List α
⊢ [] = []

case mp.cons
α : Type u_1
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x1 x2 ↦ x1 = x2) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ (l.eraseIdx n).length

Tactic:
length_eraseIdx_of_lt h

Goal state after:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ l.length - 1
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 <;> [contradiction; simp]

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

Goal state before:
pp: α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?

Tactic:
by rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]

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

Goal state before:
pp: case inl
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod

pp: case inr
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
· simp only [map, erase_cons_head, prod_cons]

Goal state after:
case inr
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : map f (x :: xs) = map f (y :: ys)
⊢ x :: xs = y :: ys

Tactic:
injection hxy with hxy hxys

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
⊢ x :: xs = y :: ys
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ q.num ≤ ↑q.den ↔ q ≤ 1

Tactic:
by simp [Rat.le_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ q.num < ↑q.den ↔ q < 1

Tactic:
simp [Rat.lt_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H1 : IsRelPrime x z
H2 : x ∣ y * z
h : IsPrimal x
⊢ x ∣ y

Tactic:
by
  obtain ⟨a, b, ha, hb, rfl⟩ := h H2
  exact (H1.of_mul_left_right.isUnit_of_dvd hb).mul_right_dvd.mpr ha

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

Goal state before:
pp: case inl
q : ℚ
d : ℤ
hd : d ≠ 0
qdf : q = 0 /. d
⊢ ∃ c, 0 = c * q.num ∧ d = c * ↑q.den

Tactic:
simp [qdf]

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

Goal state before:
pp: case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ node v <$> pure l <*> pure r = pure (node v l r)

Tactic:
seq_pure,

Goal state after:
case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ (fun h ↦ h r) <$> node v <$> pure l = pure (node v l r)
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a b : R
⊢ a - b = a + -b

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨅ i, ⨅ (hi : p i), u (f i hi)) = ⨅ i, ⨅ (hi : p i), f i hi

Tactic:
by
  simp only [iInf_subtype', gi.l_iInf_u]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ ⨆ x, g (f x) = ⨆ y, g y

Tactic:
simp only [iSup.eq_1]

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ sSup (range fun x ↦ g (f x)) = sSup (range fun y ↦ g y)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t

Tactic:
simp_rw [iUnion_subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
s : Set β
t : Set γ
f : β → α
g : γ → α
h : β → γ
h1 : BijOn h s t
h2 : ∀ (x : β), g (h x) = f x
⊢ ⨆ x ∈ s, f x = ⨆ y ∈ t, g y

Tactic:
simpa only [h2] using h1.iSup_comp g

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ⋃ (_ : s.Nonempty), s = s

Tactic:
iUnion_nonempty_index,

Goal state after:
α : Type u_1
s : Set α
⊢ ⋃ x ∈ s, s = s
Module: Mathlib.Order.CompleteLattice.Basic

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✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsGLB ((fun {x} ↦ f x) '' x✝) (f (sInf x✝))

Tactic:
by rw [map_sInf]; exact isGLB_biInf

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ ⨆ x ∈ ⋃₀ S, p x ↔ ⨆ s ∈ S, ⨆ x ∈ s, p x

Tactic:
iSup_sUnion

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup s = sSup univ

Tactic:
csSup_of_not_bddAbove hs,

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup ∅ = sSup univ
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
· exact isGLB_sInf' hs

Goal state after:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)
Module: Mathlib.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat |a| na

Tactic:
by
  rw [pa.out, Nat.abs_cast]
  constructor
  rfl

Goal state after:
Module: Mathlib.Data.Int.CharZero

Goal state before:
pp: k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ ↑(↑m / ↑n) = ↑m / ↑n

Tactic:
by
  rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]

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

Goal state before:
pp: n k : ℕ
⊢ n ^ (k + 1) ≤ n.ascFactorial (k + 1)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]
    exact Nat.mul_le_mul (Nat.le_refl n)
      (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

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

Goal state before:
pp: m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).1 + ↑k * (k.modDivAux (↑m % ↑k) (↑m / ↑k)).2 = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
exact this.trans h₀

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

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

Tactic:
mod_coe,

Goal state after:
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) = ↑k
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:
mod_coe,

Goal state after:
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) = ↑k
⊢ ↑m % ↑k = 0
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * q.num ∧ ↑d = c * ↑q.den

Tactic:
by
    rw [q_eq]
    exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

Goal state after:
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
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ (y ^ (m + 1))⁻¹ < x

Tactic:
inv_lt_comm₀ (zpow_pos hyp _) hx

Goal state after:
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
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x⁻¹ < y ^ (m + 1)
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
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hf : Nat.find this = 0
⊢ False

Tactic:
simp only [hf, pow_zero] at H

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
hf : Nat.find this = 0
H : 1 < b * c
⊢ False
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂ : l <+ l₂
⊢ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
obtain ⟨l', h₂⟩ := h₂.exists_perm_append

Goal state after:
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂✝ : l <+ l₂
l' : List α
h₂ : l₂ ~ l ++ l'
⊢ ∃ l, l ~ l₂ ∧ l₁ <+ l
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
s t : Multiset α
h : Rel (fun x1 x2 ↦ x1 = x2) s t
⊢ s = t

Tactic:
induction h

Goal state after:
case mp.zero
α : Type u_1
s t : Multiset α
⊢ 0 = 0

case mp.cons
α : Type u_1
s t : Multiset α
a✝² b✝ : α
as✝ bs✝ : Multiset α
a✝¹ : a✝² = b✝
a✝ : Rel (fun x1 x2 ↦ x1 = x2) as✝ bs✝
a_ih✝ : as✝ = bs✝
⊢ a✝² ::ₘ as✝ = b✝ ::ₘ bs✝
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:
simp only [← range_comp, Function.comp_def]

Goal state after:
α : Type u_1
l : List α
d : α
⊢ (range fun n ↦ l[n]?.getD d) = range fun x ↦ l[x]?.getD d
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ s.card = t.card

Tactic:
induction h

Goal state after:
case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ card 0 = card 0

case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : as✝.card = bs✝.card
⊢ (a✝² ::ₘ as✝).card = (b✝ ::ₘ bs✝).card
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
x✝ : Option β
h : f a = x✝
⊢ filterMap f (a ::ₘ s) = (Option.map singleton x✝).getD 0 + filterMap f s

Tactic:
cases h : f a with

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

Goal state before:
pp: α : Type u_1
⊢ ¬∅.Nontrivial

Tactic:
simp [Finset.Nontrivial]

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ¬{a}.Nontrivial

Tactic:
simp [Finset.Nontrivial]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ ↑s = {a, b} ↔ s = {a, b}

Tactic:
← coe_pair,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ ↑s = ↑{a, b} ↔ s = {a, b}
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t u : Finset α
h : Disjoint s t
⊢ Disjoint (s.disjUnion t h) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
by
  simp only [disjoint_left, mem_disjUnion, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : α
⊢ {a} ≠ univ

Tactic:
apply SetLike.coe_ne_coe.1
  simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ

Tactic:
simp_rw [compl_insert, insert_erase (mem_compl.2 ha)]

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

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ (image f)^[n + 1] s = image f^[n + 1] s

Tactic:
rw [iterate_succ_apply', iterate_succ', ih, image_image]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
P : α → Prop
inst✝ : DecidablePred P
h : l.Nodup
⊢ #(List.filter (fun b ↦ decide (P b)) l).toFinset = (List.filter (fun b ↦ decide (P b)) l).length

Tactic:
exact toFinset_card_of_nodup (h.filter P)

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ (if n ≤ ↑a + ↑b % n then ↑a + ↑b % n - n else ↑a + ↑b % n) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

Tactic:
Nat.mod_eq_of_lt (show ↑b < n from b.2)

Goal state after:
n : ℕ
a b : Fin n
⊢ (if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
· obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi < j ↔ i < j.castSucc

Tactic:
by
  rw [← castSucc_lt_castSucc_iff, castSucc_castPred]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j < i.castPred hi ↔ j.castSucc < i

Tactic:
by
  rw [← castSucc_lt_castSucc_iff, castSucc_castPred]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (fun i hi ↦ f ⟨i, hi⟩) (range n) ⋯

Tactic:
ext
  grind

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

Goal state before:
pp: case grind
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h✝¹ : #s + 1 = #t
a : α
ha : t \ s = {a}
h✝ : ∀ (a : α), insert a s = t → a ∈ s
this : a ∈ t \ s
h : insert a s ⊆ t
this✝ : #t ≤ #(insert a s) → insert a s = t
⊢ False

Tactic:
instantiate

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i : Fin (n✝ + 1)
⊢ i.predAbove 0 = 0

Tactic:
predAbove_of_le_castSucc _ _ (zero_le _),

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i : Fin (n✝ + 1)
⊢ castPred 0 ⋯ = 0
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
append_right,

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = (v ∘ Fin.cast ⋯) (natAdd m r)