mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f b * f a ≤ f (c * a)

Tactic:
mul

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f b * f a ≤ f c * f a
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f a * f c ≤ f (b * c)

Tactic:
mul

Goal state after:
α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f a * f c ≤ f b * f c
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ f a * f b < f (a * c)

Tactic:
mul

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ f a * f b < f a * f c
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ f b * f a < f (c * a)

Tactic:
mul

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ f b * f a < f c * f a
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
⊢ mulSupport (mulSingle i a) = if a = 1 then ∅ else {i}

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: i n✝ n : ℕ
h✝ : n.succ.succ < 2
⊢ n.succ.succ + (n✝ + 1)! ≤ (n.succ.succ + (n✝ + 1))!

Tactic:
contradiction

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

Goal state before:
pp: n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < (n + 1).ascFactorial 1

Tactic:
contradiction

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

Goal state before:
pp: n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1).ascFactorial 1 < (n + 1) ^ 1

Tactic:
contradiction

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ

Tactic:
rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]

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

Goal state before:
pp: n : ℕ
a✝ : 2 ≤ 1
⊢ 1 ≤ n → (n + 1 - 1) ^ 1 < n.descFactorial 1

Tactic:
contradiction

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a✝ : 2 ≤ 1
⊢ n.descFactorial 1 < n ^ 1

Tactic:
contradiction

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

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

Tactic:
Nat.mul_comm n

Goal state after:
n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
rcases n with n | n

Goal state after:
case ofNat
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.ofNat n))⁻¹ = (↑(Int.ofNat n))⁻¹

case negSucc
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹
Module: Mathlib.Algebra.Order.Round

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

Tactic:
rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]

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

Goal state before:
pp: case succ.zero
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
IH : (h : 0 < 0) → p ⟨0, h⟩
h : 0 < 0 + 1
⊢ p ⟨0 + 1, h⟩

pp: case succ.succ
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n + 1) → p ⟨n + 1, h⟩
h : 0 < n + 1 + 1
⊢ p ⟨n + 1 + 1, h⟩

Tactic:
· exact one

Goal state after:
case succ.succ
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n + 1) → p ⟨n + 1, h⟩
h : 0 < n + 1 + 1
⊢ p ⟨n + 1 + 1, h⟩
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
⊢ ↑k ∣ ↑m ↔ m.mod k = k

Tactic:
rw [Nat.dvd_iff_mod_eq_zero]

Goal state after:
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ m.mod k = k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
k m : ℕ+
h : m.mod k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0

Tactic:
exact h'

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(↑⌊x⌋ - ↑z + fract x)

Tactic:
neg_add,

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(↑⌊x⌋ - ↑z) + -fract x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m n : ℕ+
⊢ m ∣ n → m ≤ n

Tactic:
dvd_iff'

Goal state after:
m n : ℕ+
⊢ n.mod m = m → m ≤ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ a < ↑⌊a⌋ + 1

Tactic:
simpa only [Int.succ, Int.cast_add, Int.cast_one] using lt_succ_floor a

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
m : ℤ
⊢ m ≤ ⌊a * ↑n⌋ / n ↔ m ≤ ⌊a⌋

Tactic:
rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr hn)]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 ≤ a
⊢ Monotone fun n ↦ a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_
  rw [zpow_add_one]
  exact le_mul_of_one_le_right' ha

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

Goal state before:
pp: case inl
α : 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
⊢ False

Tactic:
rcases exists_between hlt with ⟨b, hab, hb⟩

Goal state after:
case inl
α : 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
b : α
hab : a < b
hb : b < 1
⊢ False
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 b : R
⊢ a + b - ↑⌊a + b⌋ ≤ a - ↑⌊a⌋ + (b - ↑⌊b⌋)

Tactic:
sub_add_sub_comm,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + b - ↑⌊a + b⌋ ≤ a + b - (↑⌊a⌋ + ↑⌊b⌋)
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 b : R
⊢ a - ↑⌊a⌋ + (b - ↑⌊b⌋) ≤ a + b - ↑⌊a + b⌋ + 1

Tactic:
sub_add_sub_comm,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a + b - (↑⌊a⌋ + ↑⌊b⌋) ≤ a + b - ↑⌊a + b⌋ + 1
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -(1 + 1) ≤ a - 1

Tactic:
neg_add,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -1 + -1 ≤ a - 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
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) + 1)

Tactic:
neg_add,

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 + 1)
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:
pointReflection_symm

Goal state after:
G : Type u_3
P : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ (pointReflection x) y = (pointReflection x) y
Module: Mathlib.Data.Set.List

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
a : α
hl : f a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ f a :: map f l ∈ range (map f)

Tactic:
exact ⟨a :: l, map_cons⟩

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

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ x ∈ l → count x l = 1

Tactic:
← count_pos_iff

Goal state after:
α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ 0 < count x l → count x l = 1
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
by rw [insert_of_not_mem h', nodup_cons]; constructor <;> assumption

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t

Tactic:
exact Multiset.add_le_add_right le_union_left

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.dedup.toFinset = m.toFinset

Tactic:
by
  simp_rw [toFinset, dedup_idem]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∩ t) = min (count a s) (count a t)

Tactic:
by
  apply @Nat.add_left_cancel (count a (s - t))
  rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : x ∈ s
hkx : f k = f x
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case mp
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] → head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

pp: case mpr
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x] → head✝¹ :: head✝ :: tail✝ <:+: [x]

Tactic:
· rintro ⟨_ | _, _, h⟩ <;> simp at h

Goal state after:
case mpr
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x] → head✝¹ :: head✝ :: tail✝ <:+: [x]
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) (range b))

Tactic:
apply range_disjoint_map_add

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t u : Finset α
x : α
hx : x ∈ u
hi hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) (f x)
h : f x ≠ f x
⊢ x ∈ ⊥

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ {a} ∩ s = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ s ∩ {a} = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

Tactic:
simp_rw [erase_eq, disjoint_sdiff_comm]

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

Goal state before:
pp: case h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Tactic:
| _ i h
   => 

Goal state after:
case h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

Tactic:
rw [Fin.add_def]

Goal state after:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s

Tactic:
← card_union_of_disjoint (disjoint_filter_filter_not _ _ _),

Goal state after:
α : Type u_1
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ #(filter p s ∪ {a ∈ s | ¬p a}) = #s
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ Function.Injective (Fin.cons x₀ xs)

Tactic:
rw [Fin.cons_injective_iff]

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove i.succ = i

Tactic:
by
  rw [predAbove_of_succ_le _ _ (succ_le_succ_iff.mpr h), pred_succ]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst✝¹ : Decidable p
α : p → Type u_4
inst✝ : (hp : p) → Fintype (α hp)
hp : ¬p
h : (hp : p) → α hp
x : p
⊢ h x = ⋯.elim

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : 1 < #s
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
have : Nonempty α := ⟨a⟩

Goal state after:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this : Nonempty α
⊢ ∃ b ∈ s, b ≠ a
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys) ↔ Injective xs ∧ Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j

Tactic:
← Sum.elim_injective,

Goal state after:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys) ↔ Injective (Sum.elim xs ys)
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case neg.cons_cons
α : Type u_1
l✝ : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
a✝ : [x] <+ l
⊢ [x, x] <+ l

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (∃ x, x ∈+ l) ↔ ¬l.Nodup

Tactic:
simp [nodup_iff_forall_not_duplicate]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
nd : l.Nodup
h : ∀ (x : α), x ∈ l
i : Fin l.length
⊢ (fun a ↦ ⟨idxOf a l, ⋯⟩) ((fun i ↦ l.get i) i) = i

Tactic:
by simp [nd]

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

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
this : i < n + m
⊢ as ⟨i, ⋯⟩ = b

Tactic:
contradiction

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

Goal state before:
pp: case pos
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : ¬i - n < m
lt_add : i < n + m
this : i - n < m
⊢ b = bs ⟨i - n, ⋯⟩

Tactic:
contradiction

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
⊢ t.Finite

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
this : Finite ↑s
⊢ t.Finite
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).Finite

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
this : Finite ↑s
⊢ (f '' s).Finite
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ SurjOn f s s ↔ BijOn f s s

Tactic:
refine ⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩

Goal state after:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
⊢ InjOn f s
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.nil
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
hb : Pairwise r []
hs : a :: as <+ []
⊢ orderedInsert r x (a :: as) <+ orderedInsert r x []

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α),
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (a ::ₘ s))

Tactic:
simp +contextual [hm]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
split_ifs
  · grind [find_eq_zero]
  · grind [find_of_not_zero]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha
  exact ha.elim h₁.rel_dropLast_getLast (· ▸ hlast)

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
h : Pairwise R []
ha : a ∈ []
⊢ R [].head! a

Tactic:
contradiction

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

Goal state before:
pp: case refine_2.rel
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂

Tactic:
exact Or.inl h

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

Goal state before:
pp: case nil.nil
α : Type u
inst✝ : DecidableEq α
H : [].length ≤ [].length
h : [] ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] []

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b

Tactic:
refine ⟨fun h _ _ _ _ eq => (isChain_append_cons_cons.mp (eq ▸ h)).2.1, ?_⟩

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
inst✝ : Trans R R R
hl : IsChain R (a :: l)
hb : b ∈ l
⊢ R a b

Tactic:
rw [isChain_iff_pairwise] at hl
  exact rel_of_pairwise_cons hl hb

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

Goal state before:
pp: case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (a ++ [L]).getLast hL :: (a ++ [L]).dropLast ~r a ++ [L]

Tactic:
| append_singleton a L _ =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ x, ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Tactic:
rw [exists_comm]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ b a, b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ ((a ::ₘ s).sigma fun a ↦ t a + u a) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u

Tactic:
rw [cons_sigma, IH]

Goal state after:
α : Type u_1
σ : α → Type u_4
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (s.sigma fun a ↦ t a + u a) = s.sigma t + s.sigma u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + (s.sigma t + s.sigma u) = (a ::ₘ s).sigma t + (a ::ₘ s).sigma u
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : ¬List.count a l ≤ 1
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
Nat.not_le

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1