mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ⌊↑0⌋ = 0

Tactic:
floor_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ 0 = 0
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
⊢ ⌊↑1⌋ = 1

Tactic:
floor_intCast

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

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

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
z : ℤ
⊢ ↑z - ↑⌊↑z⌋ = 0

Tactic:
floor_intCast

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
⊢ ↑z - ↑z = 0
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b + ((↑n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) =
    (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
        abel

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

Tactic:
rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]

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
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
refine ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one ?_⟩

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
n : ℤ
hn : (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n
⊢ m < n + 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
this : 0 < 1 - fract q
⊢ 0 < ↑q.den

Tactic:
exact mod_cast q.pos

Goal state after:
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
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈(b - 1)⁻¹⌉ < b * a

Tactic:
rwa [← div_lt_iff₀']

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
⊢ (p₁ /ₛ p₂)⁻¹ = p₂ /ₛ p₁

Tactic:
refine inv_eq_of_mul_eq_one_right (smul_right_cancel p₁ ?_)

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
⊢ ((p₁ /ₛ p₂) * (p₂ /ₛ p₁)) • p₁ = 1 • p₁
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ Int.cast ⁻¹' Iic a = Iic ⌊a⌋

Tactic:
ext
  simp [le_floor]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p /ₛ p₁ = p /ₛ p₂
⊢ p₁ = p₂

Tactic:
by
  refine smul_left_cancel (p /ₛ p₂) ?_
  rw [sdiv_smul, ← h, sdiv_smul]

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

Goal state before:
pp: α : Type u_1
a b : α
m : Multiset α
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0

Tactic:
rw [← cons_zero, cons_eq_cons]

Goal state after:
α : Type u_1
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s

Tactic:
obtain rfl := mem_singleton.1 (hs.1 hb)
    rwa [singleton_subset]

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

Goal state before:
pp: case mp.cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
· rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

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

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

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
a : α
⊢ count a (s + t - u) = count a (s + (t - u))
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ count a (s + t - t) = count a s
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons.inl.inr
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f x✝) ∧ (map f tl).Nodup
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
apply (d.1 _ h₂ h₃.symm).elim

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

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

Tactic:
rw [eq_comm, map_eq_zero]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: List.filter (fun a ↦ elem a (take n l)) l =
    List.filter (fun a ↦ elem a (b :: List.filter (fun a ↦ elem a (take n l)) l)) (b :: l)

Tactic:
filter_cons_of_pos (by simp)

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: List.filter (fun a ↦ elem a (take n l)) l =
    b :: List.filter (fun a ↦ elem a (b :: List.filter (fun a ↦ elem a (take n l)) l)) l
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)
⊢ t = map (fun x ↦ i ↑x ⋯) s.attach

Tactic:
rw [ht.ext]

Goal state after:
α : 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)
⊢ ∀ (a : β), a ∈ t ↔ a ∈ map (fun x ↦ i ↑x ⋯) s.attach

α : 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 (fun x ↦ i ↑x ⋯) s.attach).Nodup
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    ((if p (f a) then {a} else 0) + filter (fun a ↦ p (f a)) t).card

Tactic:
card_add,

Goal state after:
case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then {a} else 0).card + (filter (fun a ↦ p (f a)) t).card
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s - filter p s = filter (fun a ↦ ¬p a) s

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (ndinsert a s).card = s.card

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (ndinsert a s).card = s.card + 1

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
⊢ ¬∅.Nontrivial

Tactic:
by simp [Finset.Nontrivial]

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ¬{a}.Nontrivial

Tactic:
by simp [Finset.Nontrivial]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ a ∉ s \ t

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False

Tactic:
simpa [hp, hq] using h a

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ univ ∩ s = s

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ univ ∩ s ↔ a ∈ s
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ s.toFinset = t.toFinset

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image f (image g s) = image g' (image f' s)

Tactic:
image_image,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image (f ∘ g) s = image (g' ∘ f') s
Module: Mathlib.Data.Finset.Image

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

Tactic:
ext a

Goal state after:
α : 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
Module: Mathlib.Data.Finset.Image

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

Tactic:
ext a

Goal state after:
α : 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
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ s = image (fun i ↦ f ↑i ⋯) (range n).attach

Tactic:
ext a

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ a ∈ s ↔ a ∈ image (fun i ↦ f ↑i ⋯) (range n).attach
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : 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
⊢ #s = #t

Tactic:
classical
  calc
    #s = #s.attach := card_attach.symm
    _ = #(s.attach.image fun a ↦ i a.1 a.2) := Eq.symm ?_
    _ = #t := ?_
  · apply card_image_of_injective
    intro ⟨_, _⟩ ⟨_, _⟩ h
    simpa using i_inj _ _ _ _ h
  · congr 1
    ext b
    constructor <;> intro h
    · obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi
    · obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

Goal state after:
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
  by_contra! hz
  refine hc.not_ge (card_le_card_of_injOn f hf ?_)
  intro x hx y hy
  contrapose
  exact hz x hx y hy

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ (n - ↑b + ↑a) % n = (m - ↑b + ↑a) % m + n - m

Tactic:
Nat.mod_eq_of_lt (by omega)

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = (m - ↑b + ↑a) % m + n - m
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = (m - ↑b + ↑a) % m + n - m

Tactic:
Nat.mod_eq_of_lt (by omega)

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m

Tactic:
Nat.mod_eq_of_lt (by omega)

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
c : α
⊢ [] = replicate 0 c

Tactic:
replicate_zero

Goal state after:
α : Type u
c : α
⊢ [] = []
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rcases i.le_or_gt (castSucc j) with (h | h)
  · rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]
  · rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : p < i
⊢ p.predAbove i.castSucc = i.castSucc.pred ⋯

Tactic:
by
  rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_castSucc_iff.2 h)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
inst✝ : Decidable p
x✝ : PLift p
h : p
⊢ { down := h } ∈ if h : p then {{ down := h }} else ∅

Tactic:
by simp [h]

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

Goal state before:
pp: case refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
l : Fin n
⊢ «repeat» m.succ a (Fin.cast ⋯ (castAdd (m * n) l)) =
    (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m * n) l))

pp: case refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
r : Fin (m * n)
⊢ «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))

Tactic:
· simp [modNat, Nat.mod_eq_of_lt l.is_lt]

Goal state after:
case refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
r : Fin (m * n)
⊢ «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l

Tactic:
induction l <;> grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
l : List α
x : α
hl₁ : ∀ (a : α), a ∈ l → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ l → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x l) = orderedInsert s (f x) (map f l)

Tactic:
induction l <;> grind

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
⊢ a ∉ s.toFinset.val

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∈ s
⊢ ∀ (x : α), x ∈ s.toFinset ↔ x ∈ insert a s

Tactic:
by simp [h]

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

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ StrictMono fun i ↦ if ↑i = 0 then n else m

Tactic:
rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩

Goal state after:
case mpr.refine_1.zero.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi hj : 0 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

case mpr.refine_1.zero.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l c : List α
a : α
hl : c <+ l
ha : ∀ (a' : α), a' ∈ c → r a a'
⊢ a :: c <+ orderedInsert r a l

Tactic:
induction l <;> grind

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
this : ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
by
        simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]

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

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

Tactic:
find_eq_iff,

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧ ∀ (j : Fin (n + 1)), j < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
⊢ p (natAdd m (subNat m (Fin.cast ⋯ (Fin.find p hᵢ)) hm))

Tactic:
by simp [Fin.find_spec]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > min y z ↔ x > y ∨ x > z

Tactic:
change _ < _ ↔ _

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z < x ↔ x > y ∨ x > z
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x > max y z ↔ x > y ∧ x > z

Tactic:
change _ < _ ↔ _

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ max y z < x ↔ x > y ∧ x > z
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' ≤ l
⊢ a :: l' ≤ a :: l

Tactic:
rw [le_iff_lt_or_eq] at h ⊢

Goal state after:
α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ ((a :: l).rotate n).prod = 1

Tactic:
have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
    rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
⊢ (n • s).dedup = s.dedup

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
⊢ count a (n • s).dedup = count a s.dedup
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
⊢ image Prod.fst (s ×ˢ t) = s

Tactic:
ext i
  simp [mem_image, ht.exists_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
⊢ image Prod.snd (s ×ˢ t) = t

Tactic:
ext i
  simp [mem_image, ht.exists_mem]

Goal state after: