mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑(negOfNat n) / ↑d⌉ = negOfNat (n / d)

Tactic:
rw [@negOfNat_eq (n / d), ofNat_eq_natCast, ← ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    floor_natCast_div_natCast n d, ← neg_neg (n : ℤ), ← ofNat_eq_natCast, ← negOfNat_eq,
    ← ceil_intCast_div_natCast (.negOfNat n) d, ← ceil_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

Tactic:
apply exists_floor'
  · obtain ⟨n, hn⟩ := exists_int_lt x
    exact ⟨n, hn.le⟩
  · obtain ⟨n, hn⟩ := exists_int_gt x
    exact ⟨n, hn.le⟩

Goal state after:
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) → ∀ (x : K), ∃ n, x < ↑n

Tactic:
intro h

Goal state after:
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
h : ∀ (x : K), ∃ n, x < ↑n
⊢ ∀ (x : K), ∃ n, x < ↑n
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
Module: Mathlib.Data.Multiset.Replicate

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

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
s t : Multiset α
h : Rel (fun x1 x2 ↦ x1 = x2) s t
⊢ s = t
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x

Tactic:
exact ⟨x, cons_le_cons _ h⟩

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

Goal state before:
pp: case nil
α : Type u
⊢ (∀ (a : α), ¬[a, a] <+ []) → [].Nodup

Tactic:
intro h

Goal state after:
case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
⊢ (∀ (a : α), ¬[a, a] <+ head✝ :: tail✝) → (head✝ :: tail✝).Nodup

Tactic:
intro h

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
h : ∀ (a : α), ¬[a, a] <+ head✝ :: tail✝
⊢ (head✝ :: tail✝).Nodup
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') →
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
h : ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
⊢ ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
h : ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
⊢ ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a} ∧ f a = b
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t

Tactic:
← rel_eq,

Goal state after:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) (map f s) (map f t) ↔ s = t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) (map f s) (map f t) ↔ s = t

Tactic:
← rel_eq,

Goal state after:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) (map f s) (map f t) ↔ Rel (fun x1 x2 ↦ x1 = x2) s t
Module: Mathlib.Data.List.Dedup

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

Tactic:
refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self), fun ha => ?_, by rw [h, tail_cons]⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
⊢ False
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ map f s = map g t

Tactic:
by
  have : t = s.attach.map fun x => i x.1 x.2 := by
    rw [ht.ext]
    · aesop
    · exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy
  calc
    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u

Tactic:
simpa only [zero_inter] using h₁

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ≤ t
⊢ s ∪ t = t

Tactic:
union_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ≤ t
⊢ t ∪ s = t
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
rw [Multiset.add_comm, add_inter_distrib]
    refine le_inter (Multiset.add_le_add_right le_union_right) ?_
    rw [Multiset.add_comm]
    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:
simp_rw [toFinset, dedup_idem]

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

Goal state before:
pp: x✝ : ℕ
⊢ range x✝ ⊂ range (x✝ + 1)

Tactic:
simp [ssubset_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Bool
⊢ x ∈ { val := {true, false}, nodup := fintype._proof_1 }

Tactic:
cases x

Goal state after:
case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false ∈ { val := {true, false}, nodup := fintype._proof_1 }

case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true ∈ { val := {true, false}, nodup := fintype._proof_1 }
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Ordering
⊢ x ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

Tactic:
cases x

Goal state after:
case lt
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ lt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

case eq
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ eq ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

case gt
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ gt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t → map f.toEmbedding s ⊆ t

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
⊢ map f.toEmbedding s ⊆ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ map f.toEmbedding s ⊆ t → s ⊆ map f.symm.toEmbedding t

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
⊢ s ⊆ map f.symm.toEmbedding t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x ↦ x ∈ t) s
⊢ a ∈ t

Tactic:
convert! property_of_mem_map_subtype s ha

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
⊢ a ∈
      (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
        ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s) →
    a ∈ s

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h :
  a ∈
    (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
      ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s)
⊢ a ∈ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
⊢ a ∈ s →
    a ∈
      (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
        ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s)

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : a ∈ s
⊢ a ∈
    (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
      ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
⊢ a ∈
      ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
          ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s)) →
    a ∈ ↑s

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h :
  a ∈
    ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
        ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s))
⊢ a ∈ ↑s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
⊢ a ∈ ↑s →
    a ∈
      ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
          ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s))

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : a ∈ ↑s
⊢ a ∈
    ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
        ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s))
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
⊢ #(image f s) ≤ #s

Tactic:
simpa only [card_map] using! (s.1.map f).toFinset_card_le

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

Goal state before:
pp: n a : ℕ
ha : a < n + 2
⊢ 1 = ⟨a, ha⟩ ↔ a = 1

Tactic:
by
  simp [eq_comm]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < a ↔ a ≠ 0

Tactic:
by
  rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]

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

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

Tactic:
intro h

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

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

Tactic:
intro h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by_contra! hz

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ False
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ b ≤ a.castSucc.pred ⋯ ↔ b < a

Tactic:
le_pred_castSucc_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ b < a ↔ b < a
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
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)

Tactic:
intro h

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
⊢ Function.Injective (Fin.cons x₀ xs)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
card_eq_succ

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
card_eq_succ

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 4 → ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
card_eq_succ

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 3) → ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ

Tactic:
rwa [castSucc_castPred, ← le_castSucc_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Fintype ℕ), False

Tactic:
intro h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
h : Fintype ℕ
⊢ False
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
· simpa [h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset ⊆ t ↔ s ⊆ ↑t

Tactic:
by
  rw [← Finset.coe_subset, Finite.coe_toFinset]

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

Goal state before:
pp: α : Type u
t : Set α
ht : t.Finite
s : Finset α
⊢ s ⊆ ht.toFinset ↔ ↑s ⊆ t

Tactic:
by
  rw [← Finset.coe_subset, Finite.coe_toFinset]

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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : r x b
⊢ x :: a :: as <+ x :: b :: bs

Tactic:
exact .cons_cons _ <| .cons _ ‹a :: as <+ bs›

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
ih : x :: a :: as <+ orderedInsert r x bs
⊢ x :: a :: as <+ b :: orderedInsert r x bs

Tactic:
exact .trans ih <| .cons _ (.refl _)

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

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ {x | x ≠ a}.toFinset.card = Fintype.card α - 1

Tactic:
toFinset_ofPred,

Goal state after:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ {x | x ≠ a}.card = Fintype.card α - 1
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ j.succAbove (i.succAbove k) = (j.succAbove i).succAbove ((i.predAbove j).succAbove k)

Tactic:
succAbove_succAbove_succAbove_predAbove

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ j.succAbove (i.succAbove k) = j.succAbove (i.succAbove k)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
hi : Std.IdempotentOp op
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

Tactic:
induction s using Finset.cons_induction with
  | empty => rw [fold_empty, image_empty, fold_empty]
  | cons x xs hx ih =>
    have := Classical.decEq γ
    rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
    simp only [Function.comp_apply]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ (r c b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case cons.head
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
tail✝ : List α
h : Pairwise R (a :: tail✝)
⊢ R (a :: tail✝).head! a

Tactic:
exact refl_of ..

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

Goal state before:
pp: case cons.nil
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
H : (head✝ :: tail✝).length ≤ [].length
h : head✝ :: tail✝ ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) []

pp: case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)

Tactic:
· exact (not_lt_of_ge H).elim (succ_pos _)

Goal state after:
case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l

Tactic:
rotate_eq_rotate'

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l