mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp [division_def, mul_nonneg_iff]

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

Goal state before:
pp: case mp.cons_right
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a✝¹ : β
l₁✝ : List α
l₂✝ : List β
a✝ : SublistForall₂ R l₁✝ l₂✝
ih : ∃ l, Forall₂ R l₁✝ l ∧ l <+ l₂✝
⊢ ∃ l, Forall₂ R l₁✝ l ∧ l <+ a✝¹ :: l₂✝

Tactic:
obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩

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

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

Tactic:
exact SublistForall₂.cons_right (ih _ _ atb tbc)

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ l.prod * l'.prod = (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod

Tactic:
by
  apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans
  rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → β
b : β
x : α
xs : List α
⊢ foldr f b (xs ++ [x]) = foldr f (f x b) xs

Tactic:
simp only [List.foldr_append, List.foldr]

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

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d

Tactic:
have d₁0 := Int.ofNat_ne_zero.2 h₁

Goal state after:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
d₁0 : ↑d₁ ≠ 0
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
ι : Type u_1
inst✝¹ : BEq ι
inst✝ : LawfulBEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i < (a :: l).length
⊢ (a :: l).erase (a :: l)[i] ~ (a :: l).eraseIdx i

Tactic:
cases i with

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

Goal state before:
pp: p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C q

Tactic:
rw [← q.num_divNat_den]

Goal state after:
p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C (divNat q.num q.den)
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| y * e * 1

Tactic:
hdx

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * d * e * 1
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑(mkRat a b) = ↑a / ↑b

Tactic:
Rat.mkRat_eq_divInt,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑(a /. ↑b) = ↑a / ↑b
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b c : R
k : ℕ
x✝¹ : a ^ k = b
x✝ : b * b = c
⊢ a ^ Nat.mul 2 k = c

Tactic:
by
  subst_vars; simp [Nat.succ_mul, pow_add]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b c : R
k : ℕ
d : R
x✝² : a ^ k = b
x✝¹ : b * b = c
x✝ : c * a = d
⊢ a ^ (Nat.mul 2 k).add 1 = d

Tactic:
by
  subst_vars; simp [Nat.succ_mul, pow_add]

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

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

Tactic:
rw [iUnion_nonempty_index, biUnion_self]

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'

Tactic:
obtain ⟨i₀, hi₀⟩ := htriv

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : f i₀ ≠ ⊥
⊢ ∃ i', ⊥ ≤ f ↑i'
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f g : ι → α
⊢ (⨆ i, f i) ∆ ⨆ i, g i ≤ ⨆ i, f i ∆ g i

Tactic:
by
  simp_rw [symmDiff_le_iff, ← iSup_sup_eq]
  exact ⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
    iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩

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

Goal state before:
pp: case pos.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

Tactic:
exact ⟨b, hb⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Symm r
a b : α
⊢ Pairwise (r on fun c ↦ bif c then a else b) ↔ r a b

Tactic:
simpa [Pairwise, Function.onFun] using symm

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : (fun b ↦ [[b, a]]) b = (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
rw [Set.ext_iff] at h

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ [[b, a]]) b ↔ x ∈ (fun b ↦ [[b, a]]) c
⊢ b = c
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

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : (fun b ↦ Ι b a) b = (fun b ↦ Ι b a) c
⊢ b = c

Tactic:
rw [Set.ext_iff] at h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
⊢ b = c
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : s.OrdConnected
a b : ↑s
⊢ Subtype.val '' uIoo a b = uIoo ↑a ↑b

Tactic:
simp [uIoo, (Subtype.mono_coe (· ∈ s)).map_inf, (Subtype.mono_coe (· ∈ s)).map_sup]

Goal state after:
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:
by split_ifs with h <;> simp [h]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
⊢ (mulSupport (mulSingle i a)).Subsingleton

Tactic:
by
  classical
  rw [mulSupport_mulSingle]
  split_ifs with h <;> simp

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

Goal state before:
pp: case step
m n m✝ : ℕ
a✝ : m.le m✝
ih : m ! ∣ m✝!
⊢ m ! ∣ m✝.succ !

Tactic:
| step _ ih =>

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

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

Tactic:
descFactorial_zero

Goal state after:
n : ℕ
⊢ (n + 1) * 1 = (n + 1) * 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
descFactorial_zero

Goal state after:
n : ℕ
⊢ 1 = 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
descFactorial_zero

Goal state after:
n : ℕ
⊢ 1 = 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
exact pow_sub_lt_descFactorial' h

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

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑⌊x⌋| = fract x

Tactic:
self_sub_floor,

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |fract x| = fract x
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊x + 1 / 2⌋

Tactic:
rw [← cast_mul_floor_div_cancel_of_pos two_pos, round_eq_div]
  simp [mul_add]

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
a b : R
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Tactic:
rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]

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

Tactic:
← one_add_mul,

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a < (1 + ↑⌊a / b⌋) * 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 : R
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
rcases eq_or_ne (fract a) 0 with ha | ha
  · exact Or.inl ha
  right
  suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
    rw [this, ← self_sub_fract]
    abel
  rw [← Int.cast_one, ← Int.cast_add]
  refine congrArg Int.cast (ceil_eq_iff.mpr ⟨?_, _root_.le_of_lt <| by simp⟩)
  rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
  exact ha.symm.lt_of_le (fract_nonneg a)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
by
  by_cases h : a ∈ s
  · rwa [card_erase_of_mem h, if_pos]
  · rwa [erase_of_notMem h, if_neg]

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

Goal state before:
pp: case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : (a :: l).Nodup
i : ℕ
h : i < (a :: l).length
⊢ (a :: l).erase (a :: l)[i] = (a :: l).eraseIdx i

Tactic:
cases i with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ l.dedup.tail = l'

Tactic:
rw [h, tail_cons]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∪ t \ s = t ∪ s \ t

Tactic:
simp [union_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), x ∉ {a} ∩ s

Tactic:
simp only [mem_inter, mem_singleton]; rintro x ⟨rfl, h⟩; exact H h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ++ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl hl => simp [hl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
x✝ : β
⊢ x✝ ∈ map f s.toFinset ↔ x✝ ∈ (Multiset.map (⇑f) s).toFinset

Tactic:
by simp only [mem_map, Multiset.mem_map, Multiset.mem_toFinset]

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

Goal state before:
pp: n : ℕ
⊢ range (n + 1) \ {0} = image Nat.succ (range n)

Tactic:
by
  induction n with
  | zero => simp
  | succ k hk =>
    conv_rhs => rw [range_add_one]
    rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]
    simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #(insert a s) = #s + 1

Tactic:
by
  grind [=_ cons_eq_insert]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
⊢ #s = #t

Tactic:
refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
let f' : s → β := fun a ↦ f a a.2
  have hinj' : Set.InjOn f' s.attach := fun x hx y hy hxy ↦ Subtype.ext (hinj _ _ x.2 y.2 hxy)
  have hmapsto' : Set.MapsTo f' s.attach t := fun x hx ↦ hf _ _
  intro b hb
  obtain ⟨a, ha, rfl⟩ := surjOn_of_injOn_of_card_le _ hmapsto' hinj' (by rwa [card_attach]) hb
  exact ⟨a, a.2, rfl⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ s.Nontrivial

Tactic:
rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ {x ∈ s | x i = ai} ⊂ s

Tactic:
filter_ssubset

Goal state after:
ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ ∃ x ∈ s, ¬x i = ai
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
| f n

Tactic:
rw [hf]

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
| seqOfForallFinsetExistsAux P r h' n
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: m n : ℕ
h : m ≤ n
| m

Tactic:
← Fintype.card_fin m

Goal state after:
m n : ℕ
h : m ≤ n
| card (Fin m)
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: n m : ℕ
h : Fin n = Fin m
⊢ cast h = Fin.cast ⋯

Tactic:
by
  cases fin_injective h
  rfl

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

Goal state before:
pp: m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : Fin (n + (m + 1))
⊢ append as (snoc bs b) i = snoc (append as bs) b i

Tactic:
rcases i with ⟨i, isLt⟩

Goal state after:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
⊢ append as (snoc bs b) ⟨i, isLt⟩ = snoc (append as bs) b ⟨i, isLt⟩
Module: Mathlib.Data.List.ProdSigma

Goal state before:
pp: α : Type u_1
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ ⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

Tactic:
by
  simp [List.sigma, mem_flatMap, mem_map, exists_and_left, and_left_comm,
    exists_eq_left, exists_eq_right]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
rw [flatten_cons, isChain_append, isChain_flatten hL.2, forall_mem_cons, isChain_cons_cons]

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧
            ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
            IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

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

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
hle : l.length = l'.length
⊢ l = l'

Tactic:
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h

Goal state after:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ l = l'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
x✝ : l ~r []
n : ℕ
hn : l.rotate n = []
⊢ l = []

Tactic:
by simpa using hn

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

Goal state before:
pp: α : Type u
l : List α
x : α
x✝ : l ~r [x]
n : ℕ
hn : l.rotate n = [x]
⊢ l = [x]

Tactic:
by simpa using hn

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

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations → l ~r l'

pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations

Tactic:
· simp_rw [mem_iff_get, get_cyclicPermutations]
    rintro ⟨k, rfl⟩
    exact .forall _ _

Goal state after:
case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
hs : ¬a ∈ s ∧ s.Nodup
⊢ ¬a ∈ s

Tactic:
exact hs.1

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

Goal state before:
pp: n k : ℕ
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
rcases lt_trichotomy k n with hk | rfl | hk

Goal state after:
case inl
n k : ℕ
hk : k < n
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

case inr.inl
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k

case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ

Tactic:
simp [multichoose_eq n (k + 1), multichoose_eq (n + 1) k]

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

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ (Pi.cons m a (f a ⋯) fun a_1 ha ↦ f a_1 ⋯) = f

Tactic:
rw [Pi.cons_eta]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_4
inst✝ : MulOneClass M
S : Submonoid M
a : M
ha : a ∈ S
⊢ ⟨a, ha⟩ = 1 ↔ a = 1

Tactic:
simp [← SetLike.coe_eq_coe]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : {a} * {b} = 1
⊢ {a⁻¹} = {b}

Tactic:
inv_eq_of_mul_eq_one_right hab

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : {a} * {b} = 1
⊢ {b} = {b}