mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
⊢ Ioc a b = Ioc c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun h ↦ ?_, by grind⟩

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
⊢ a = c ∧ b = d
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

Tactic:
simp [*]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIcc (e x) (e y) = uIcc x y

Tactic:
simp [*]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : x ≤ y
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

Tactic:
simp [*]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
h✝ : y ≤ x
⊢ ⇑e ⁻¹' uIoc (e x) (e y) = uIoc x y

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : ¬t ⊆ ⊥
⊢ t.Nonempty

Tactic:
rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : a < b
⊢ b ≤ c

Tactic:
simpa [ha, ha.not_ge, mem_uIoc] using h b

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
x✝ : x ≤ y ∨ y ≤ x
⊢ y ≤ x

Tactic:
cases hs.total hx hy with

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
c : ↑(Icc a b)
hc : c ∈ S
⊢ a ≤ sSup (Subtype.val '' S)

Tactic:
exact c.2.1.trans (le_csSup ⟨b, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.2⟩ ⟨c, hc, rfl⟩)

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update f a y) ↔ a ∈ insert a (mulSupport f)

Tactic:
simp [*]

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)

Tactic:
simp [*]

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
a : ι
⊢ a ∈ mulSupport (update f a 1) ↔ a ∈ mulSupport f \ {a}

Tactic:
simp [*]

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}

Tactic:
simp [*]

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

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

Tactic:
have : 0 < n := by lia

Goal state after:
n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
⊢ round x = ⌈2 * x⌉ / 2

Tactic:
by
  rcases em (2 * x ∈ range Int.cast) with ⟨m, hm⟩ | hx'
  · rw [← hm, ceil_intCast]
    rcases m.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩
    · obtain rfl : m = x := mul_left_cancel₀ two_ne_zero <| by simp [← hm, ← two_mul]
      rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]
    · refine absurd ?_ hx
      exact (mul_fract_eq_one_iff_exists_int one_lt_two).mpr ⟨m, mod_cast hm.symm⟩
  · rw [round_eq_div, (ceil_eq_floor_add_one_iff_notMem _).mpr hx']

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

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

Tactic:
have hm : (m : ℕ) > 0 := m.pos

Goal state after:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m > 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k
Module: Mathlib.Data.PNat.Basic

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

Tactic:
· replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
      rw [mod_coe, if_neg h'] at h
      exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

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

Goal state before:
pp: q : ℚ
⊢ -⌊-q⌋ = -(-q.num / ↑q.den)

Tactic:
rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h✝ : p
⊢ 0 < if p then a else b

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h✝ : ¬p
⊢ 0 < if p then a else b

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : p
⊢ 0 ≤ if p then a else b

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : ¬p
⊢ 0 ≤ if p then a else b

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h✝ : p
⊢ (if p then a else b) ≠ 0

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ¬p
⊢ (if p then a else b) ≠ 0

Tactic:
simp [*]

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

Tactic:
conv_rhs => rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]

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

Goal state before:
pp: case inr
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)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
⊢ R (f (x - m • a)) (f (y - m • a))

Tactic:
exact this _ _ (by simpa) hm

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

Goal state before:
pp: case inr.inr.inl
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
refine ⟨0, ?_⟩

Goal state after:
case inr.inr.inl
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < c ^ 0 ∧ c ^ 0 < b
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ (∀ (x : K), ∃ n, x < ↑n) → Archimedean K

Tactic:
rw [archimedean_iff_nat_lt]
    intro h x
    obtain ⟨n, h⟩ := h x
    refine ⟨n.toNat, h.trans_le ?_⟩
    exact mod_cast Int.self_le_toNat _

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

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : A →* B
hf : Surjective ⇑f
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ ∀ (x y : B), c • (x * y) = c • x * c • y

Tactic:
simp only [hf.forall, smul_mul', ← smul, ← f.map_mul, implies_true]

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:
nsmul_eq_mul,

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.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
⊢ s = s' → (∀ (x : α), x ∈ s → p x = p' x) → countP p s = countP p' s'

Tactic:
exact Quot.induction_on₂ s s'
    (fun l l' hs hp => by
      simp only [quot_mk_to_coe'', coe_eq_coe] at hs
      apply hs.countP_congr
      simpa using hp)

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

Goal state before:
pp: α : Type u_1
l : List α
p : α → Bool
⊢ countP p l < l.length ↔ ∃ a, a ∈ l ∧ p a = false

Tactic:
simp [Nat.lt_iff_le_and_ne, countP_le_length]

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

Goal state before:
pp: case mpr.inl
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq₁ : a = b
eq₂ : as = bs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: 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✝

Tactic:
simp [*]

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 β
⊢ card 0 = card 0

Tactic:
simp [*]

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 β
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

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
H : hd = x
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
subst hd

Goal state after:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬x ∈ tl ∧ tl.Nodup
⊢ (update f x y x :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then (f x :: map f tl).set (idxOf x (x :: tl)) y else f x :: map f tl
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ :: tail✝.bagInter (l₂.erase head✝) <+ (head✝ :: tail✝) ∩ l₂

Tactic:
inter_cons_of_mem _ (by assumption),

Goal state after:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ :: tail✝.bagInter (l₂.erase head✝) <+ head✝ :: tail✝ ∩ l₂
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
simp [*]

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

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

Tactic:
inter_comm

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ s ∧ s = t → u + s = u ∪ t

Tactic:
rintro ⟨h0, rfl⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s u : Multiset α
h0 : u + s = u ∪ s
h : s ≤ s
⊢ u + s = u ∪ s
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).inits = map (map g) [].inits

Tactic:
simp [*]

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

Goal state before:
pp: case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).inits = map (map g) l✝.inits
⊢ (map g (l✝ ++ [a✝¹])).inits = map (map g) (l✝ ++ [a✝¹]).inits

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).inits = map (map g) l.inits

Tactic:
by
  induction l using reverseRecOn <;> simp [*]

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).tails = map (map g) [].tails

Tactic:
simp [*]

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

Goal state before:
pp: case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).tails = map (map g) l✝.tails
⊢ (map g (l✝ ++ [a✝¹])).tails = map (map g) (l✝ ++ [a✝¹]).tails

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).tails = map (map g) l.tails

Tactic:
by
  induction l using reverseRecOn <;> simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
h✝ : p
⊢ filter (fun _a ↦ p) s = s

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
h✝ : ¬p
⊢ filter (fun _a ↦ p) s = ∅

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ insert a (s₂ ∩ s₁) = insert a (s₁ ∩ s₂)

Tactic:
inter_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ insert a (s₁ ∩ s₂) = insert a (s₁ ∩ s₂)
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₂ ∩ s₁ = s₁ ∩ s₂

Tactic:
inter_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₁ ∩ s₂ = s₁ ∩ s₂
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∈ s₂
⊢ insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∉ s₂
⊢ insert a s₁ ∩ s₂ = s₁ ∩ s₂

Tactic:
simp [*]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) → s.Nontrivial

Tactic:
rintro ⟨b, hb, hba⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ s.Nontrivial
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ s.erase a ⊆ t ↔ s ⊆ t

Tactic:
← subset_insert_iff,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ s ⊆ insert a t ↔ s ⊆ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ image f s₁ ⊆ image f s₂

Tactic:
simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ ↑(castLE h ↑a) = ↑↑(a % m)

Tactic:
simp only [val_castLE, val_natCast]

Goal state after:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ a % m = a % m % n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f (if h : True then ⟨a₁, ⋯⟩ else ⟨a₀, ha₀⟩) = f (if h : True then ⟨a₂, ⋯⟩ else ⟨a₀, ha₀⟩)
⊢ a₁ = a₂

Tactic:
exact Subtype.ext_iff.mp (hf haa)

Goal state after:
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
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
⊢ a₁ = a₂

Tactic:
by
  let f' : s → β := fun a ↦ f a a.2
  have hsurj' : Set.SurjOn f' s.attach t := fun x hx ↦ by simpa [f'] using hsurj x hx
  have hinj' := injOn_of_surjOn_of_card_le f' (fun x hx ↦ hf _ _) hsurj' (by simpa)
  exact congrArg Subtype.val (@hinj' ⟨a₁, ha₁⟩ (by simp) ⟨a₂, ha₂⟩ (by simp) ha₁a₂)

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.succ
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
by
  obtain h | h := Fin.lt_or_lt_of_ne h
  · rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
      succAbove_castPred_of_lt _ _ h]
  · rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
      succAbove_pred_of_lt _ _ h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
hs : #s = Fintype.card α
⊢ #univ ≤ #s

Tactic:
rw [hs, Finset.card_univ]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ t = {x, y, z}) ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
← exists_and_left,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ t x x_1 x_2, t ⊆ s ∧ x ≠ x_1 ∧ x ≠ x_2 ∧ x_1 ≠ x_2 ∧ t = {x, x_1, x_2}) ↔
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ t = {x, y, z, w}) ↔
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
← exists_and_left,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ t x x_1 x_2 x_3,
      t ⊆ s ∧ x ≠ x_1 ∧ x ≠ x_2 ∧ x ≠ x_3 ∧ x_1 ≠ x_2 ∧ x_1 ≠ x_3 ∧ x_2 ≠ x_3 ∧ t = {x, x_1, x_2, x_3}) ↔
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ []
⊢ x ∈+ []

Tactic:
| slnil =>

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

Goal state before:
pp: case cast.inl
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
j : Fin n
y : α j.castSucc
⊢ snoc (update p j y) x j.castSucc = update (snoc p x) j.castSucc y j.castSucc

Tactic:
simp [*]

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

Goal state before:
pp: case cast.inr
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
hne : j ≠ i
⊢ snoc (update p i y) x j.castSucc = update (snoc p x) i.castSucc y j.castSucc

Tactic:
simp [*]

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

Goal state before:
pp: case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm

Goal state after: