mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a * u ∣ b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩
  apply Units.mul_right_dvd

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

Goal state before:
pp: case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = if 0 = 0 then ↑k else 0

Tactic:
rw [if_pos rfl]

Goal state after:
case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = ↑k
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case zero
m k : ℕ+
⊢ ↑(k.modDivAux 0 (↑m / ↑k)).fst = if 0 = 0 then ↑k else 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = if 0 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
rw [if_pos rfl]

Goal state after:
case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = ↑m / ↑k - 1
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: case zero
m k : ℕ+
⊢ (k.modDivAux 0 (↑m / ↑k)).snd = if 0 = 0 then ↑m / ↑k - 1 else ↑m / ↑k

Tactic:
| zero =>

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

Goal state before:
pp: case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑(nr * nr) / ↑(dr * dr)

Tactic:
← hnr,

Goal state after:
case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑q.num / ↑(dr * dr)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p / q) = ↑p / ↑q

Tactic:
rw [div_def', cast_divInt_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
    (Int.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)

case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b c k : ℕ
d e : R
x✝² : b = c * k
x✝¹ : a ^ c = d
x✝ : d ^ k = e
⊢ a ^ b = e

Tactic:
by
  subst_vars; simp [pow_mul]

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

Goal state before:
pp: case e'_4.zero
α : Type u_2
x : α
f : ℕ → α → α
⊢ rec (f 0 x) (f ∘ succ) 0 = f 0 (rec x f 0)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), gi.choice (u a ⊓ u b) ⋯ ≤ b

Tactic:
simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_right

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
by_cases BddAbove (s ∪ t) <;>
    grind [csSup_union, bddAbove_union, csSup_of_not_bddAbove]

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

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

Tactic:
by
  contrapose! h
  exact csSup_le' h

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

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

Tactic:
intro a

Goal state after:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
⊢ a ∈ (fun a ↦ ↑a) ⁻¹' s → a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
intro a

Goal state after:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
⊢ a ∈ (fun a ↦ ↑a) ⁻¹' s → a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s

Tactic:
intro a

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
⊢ a ∈ s → ⊤ ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ a ∈ t, sInf (f '' s) ≤ f a

Tactic:
intro a

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
⊢ a ∈ t → sInf (f '' s) ≤ f a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : ¬S ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ a

Tactic:
· cases a
        · exact le_top
        · apply WithTop.coe_le_coe.2
          refine csInf_le ?_ haS
          use ⊥
          intro b _
          exact bot_le

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
b' : β
⊢ b' ∈ ⇑φ '' s → b ≠ b' → r'ᶜ b b'

Tactic:
hb'

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
b' : β
hb' : b' ∈ ⇑φ '' s
⊢ b ≠ b' → r'ᶜ b b'
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
⊢ a * b < a * c

Tactic:
by
    rw [← lt, mul, mul]; refine mul_lt_mul_of_pos_left (lt.2 hbc) ?_; rwa [← zero, lt]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩ = 1

Tactic:
by ext; simp [r.2.ne']

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩ = 1

Tactic:
by ext; simp [r.2.ne']

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

Goal state before:
pp: a : ℤ
b : ℕ
h : IsInt a (Int.negOfNat b)
⊢ -a = ↑b

Tactic:
by simp [h.out]

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

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

Tactic:
refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_) <;> lia

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

Goal state before:
pp: case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!

Tactic:
apply Nat.le_of_lt

Goal state after:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n m : ℕ
h : n ≤ m
⊢ n.ascFactorial 0 ≤ m.ascFactorial 0

Tactic:
| zero =>

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

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

Tactic:
by_cases hmn : m ≤ n

Goal state after:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case zero
k m : ℕ
h : k ≤ m
⊢ k.descFactorial 0 ≤ m.descFactorial 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ min (fract x) (1 - fract x) ≤ |x - ↑z|

Tactic:
min_le_iff

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|
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
h : fract a = b
⊢ 0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z

Tactic:
by
    rw [← h]
    exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩

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
h : fract a = fract b
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)

Tactic:
unfold fract at h

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

Tactic:
← one_add_one_eq_two,

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.Floor.Ring

Goal state before:
pp: case zero
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
⊢ ∃ z, fract a * ↑0 - fract (a * ↑0) = ↑z

Tactic:
| zero =>

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b / a ^ (Equiv.neg ℤ) x ∈ Ioc c (c * a)

Tactic:
by
    simpa only [Equiv.neg_apply, zpow_neg, div_inv_eq_mul] using
      existsUnique_add_zpow_mem_Ioc ha b c

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✝⁶ : 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
⊢ l + a + n • a = l + (n + 1) • a

Tactic:
by rw [add_comm n, add_smul, one_smul, add_assoc]

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

Goal state before:
pp: case refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n

Tactic:
· rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn

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

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n * 1 ≤ ↑(n * 1) * m

Tactic:
Nat.cast_id,

Goal state after:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n * 1 ≤ n * 1 * m
Module: Mathlib.Algebra.Order.Archimedean.Basic

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

Tactic:
cases y with

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

Goal state before:
pp: case zero
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
x : WithZero M
hxy : 1 < 0
⊢ ∃ n, x ≤ 0 ^ n

Tactic:
| zero =>

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

Goal state before:
pp: case coe.zero
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
⊢ ∃ n, 0 ≤ ↑y ^ n

Tactic:
| zero =>

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

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

Tactic:
cases y with

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Tactic:
intro a

Goal state after:
case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
a : α
⊢ ∀ (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x

Tactic:
rintro ⟨x', hx'⟩
    have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
    rwa [this, replicate_succ, cons_le_cons_iff] at hx'

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

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0

Tactic:
| zero =>

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

Goal state before:
pp: case mp.zero
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s + t = a ::ₘ (s + t)

Tactic:
rw [← singleton_add, ← singleton_add, Multiset.add_assoc]

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

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ ∀ {a : α}, a ∈ 0 → ∃ b, b ∈ 0 ∧ r a b

Tactic:
| zero =>

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
⊢ ∀ {a : α}, a ∈ x ::ₘ s → ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
intro a

Goal state after:
case cons
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
⊢ a ∈ x ::ₘ s → ∃ b, b ∈ y ::ₘ t ∧ r a b
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)

Tactic:
| zero =>

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

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

Tactic:
intro a

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l : List α
d : (map f l).Nodup
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y

Tactic:
induction l with
  | nil => simp
  | cons hd tl ih =>
    simp only [map, nodup_cons, mem_map, not_exists, not_and, ← Ne.eq_def] at d
    simp only [mem_cons]
    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
    · rfl
    · apply (d.1 _ h₂ h₃.symm).elim
    · apply (d.1 _ h₁ h₃).elim
    · apply ih d.2 h₁ h₂ h₃

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

Goal state before:
pp: case cons.zero
α : 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
h : 0 < (a :: l).length
⊢ (a :: l).erase (a :: l)[0] = (a :: l).eraseIdx 0

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
k : ℕ
a : α
⊢ map f (replicate k a) = replicate k (f a)

Tactic:
simp only [← coe_replicate, map_coe, List.map_replicate]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ (map f s).card

Tactic:
← t.card_map f

Goal state after:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ (map f t).card ≤ (map f s).card
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
| cons a l hl =>

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
      rw [mem_union_iff, not_or]
      exact ⟨hx, h.1⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs.Disjoint ys.dedup

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
⊢ a ∈ xs → a ∈ ys.dedup → False
Module: Mathlib.Data.List.Perm.Lattice

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

Tactic:
by
  induction l with
  | nil => simp
  | cons x xs l_ih =>
    by_cases h₁ : x ∈ t₁
    · have h₂ : x ∉ t₂ := h h₁
      simp [*]
    by_cases h₂ : x ∈ t₂
    · simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
      exact perm_cons_append_cons _ l_ih
    · simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
⊢ ∀ (a b : List α) (p_1 : a ≈ b),
    Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ =
      fun ex_unique ↦ List.chooseX p b ⋯

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a : List α
⊢ ∀ (b : List α) (p_1 : a ≈ b),
    Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ =
      fun ex_unique ↦ List.chooseX p b ⋯
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.take n xs ~ List.filter (fun a ↦ elem a (List.take n xs)) xs

Tactic:
by
    conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]

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

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

Tactic:
rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ count a (filter p (Quot.mk (⇑(isSetoid α)) _l)) = count a (Quot.mk (⇑(isSetoid α)) _l)

Tactic:
by
    simp only [quot_mk_to_coe'', filter_coe, coe_count]
    apply count_filter
    simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.Perm s

Tactic:
apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs
  rw [toList_toFinset]

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

Goal state before:
pp: case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ u ≤ ⊥

Tactic:
rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_notMem]
    exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

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

Goal state before:
pp: α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ s✝ <+: a :: t

Tactic:
← hs,

Goal state after:
α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case cons.zero
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
h : 0 < (a :: l).tails.length
⊢ (a :: l).tails[0] = drop 0 (a :: l)

Tactic:
| zero =>

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

Goal state before:
pp: case cons.zero
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.inits.length), l.inits[n] = take n l
h : 0 < (a :: l).inits.length
⊢ (a :: l).inits[0] = take 0 (a :: l)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
⊢ ∀ (a b : Finset α), P a b

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a : Finset α
⊢ ∀ (b : Finset α), P a b