mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s t : Flag α
a : α
carrier✝¹ : Set α
Chain'✝¹ : IsChain (fun x1 x2 ↦ x1 ≤ x2) carrier✝¹
max_chain'✝¹ : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 ↦ x1 ≤ x2) s → carrier✝¹ ⊆ s → carrier✝¹ = s
carrier✝ : Set α
Chain'✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) carrier✝
max_chain'✝ : ∀ ⦃s : Set α⦄, IsChain (fun x1 x2 ↦ x1 ≤ x2) s → carrier✝ ⊆ s → carrier✝ = s
h :
  { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ }.carrier =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }.carrier
⊢ { carrier := carrier✝¹, Chain' := Chain'✝¹, max_chain' := max_chain'✝¹ } =
    { carrier := carrier✝, Chain' := Chain'✝, max_chain' := max_chain'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ sSup ∅ = ⊥

Tactic:
rw [@subset_sSup_def α (Set.Ici a) _ _ ⟨⟨a, le_rfl⟩⟩]

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ (fun t ↦
        if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ Ici a then ⟨sSup (Subtype.val '' t), ⋯⟩
        else default)
      ∅ =
    ⊥
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ sSup (Subtype.val '' range fun i ↦ f i) = ⨆ i, ↑(f i)

Tactic:
congr

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' range fun i ↦ f i) = a ⊓ ⨅ i, ↑(f i)

Tactic:
congr

Goal state after:
case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ ¬mulSupport f = ∅ ↔ f ≠ 1

Tactic:
mulSupport_eq_empty_iff

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ ¬f = 1 ↔ f ≠ 1
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * db < num✝ * da) = true
h : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * db < num✝ * da) = true
h✝ : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ⅟↑db * (↑(num✝¹ * db) * ⅟↑da) < ⅟↑db * (↑(num✝ * da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * db < num✝ * da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
by
    have h := (Nat.cast_lt (α := α)).mpr <| of_decide_eq_true h
    have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da
    have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
    have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
    rw [← mul_assoc, Nat.commute_cast] at h
    simp? at h says simp only [Nat.cast_mul, mul_invOf_cancel_right'] at h
    rwa [Nat.commute_cast] at h

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ⅟↑db * ((fun x ↦ ↑x) (num✝¹ * ↑db) * ⅟↑da) < ⅟↑db * ((fun x ↦ ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ ^ n = (↑q)⁻¹ ^ n

Tactic:
congr

Goal state after:
case inr.e_a
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ = (↑q)⁻¹
Module: Mathlib.Algebra.Order.Round

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

Tactic:
simp [mul_add]

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 • b

Tactic:
← sub_add_cancel x (n • a),

Goal state after:
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 + n • a) - n • b
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
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x - ↑n) = f x - n • b

Tactic:
← map_sub_zsmul,

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x - ↑n) = f (x - n • 1)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q

Tactic:
lt_sub_iff_add_lt

Goal state after:
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 + fract q < 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mk.mk
R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
floor✝¹ ceil✝¹ : R → ℤ
gc_coe_floor✝¹ : GaloisConnection Int.cast floor✝¹
gc_ceil_coe✝¹ : GaloisConnection ceil✝¹ Int.cast
floor✝ ceil✝ : R → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝¹, ceil := ceil✝¹, gc_coe_floor := gc_coe_floor✝¹, gc_ceil_coe := gc_ceil_coe✝¹ } =
    { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ }

Tactic:
congr

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✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x : WithBot M
⊢ ∀ {y : WithBot M}, 0 < y → ∃ n, x ≤ n • y

Tactic:
y

Goal state after:
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
⊢ 0 < y → ∃ n, x ≤ n • y
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 : WithZero M
⊢ ∀ {y : WithZero M}, 1 < y → ∃ n, x ≤ y ^ n

Tactic:
y

Goal state after:
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
⊢ 1 < y → ∃ n, x ≤ y ^ n
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:
refine smul_left_cancel (p /ₛ p₂) ?_
  rw [sdiv_smul, ← h, sdiv_smul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if b = a then n else 0

Tactic:
by
  convert! List.count_replicate (a := a)
  · rw [← coe_count, coe_replicate]
  · simp

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ≤ t + s

Tactic:
by
  simpa using Multiset.add_le_add_right (zero_le t)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ s + {a} = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
rw [Multiset.add_comm, singleton_add]
  constructor
  · rintro rfl
    exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩
  · rintro ⟨h, rfl⟩
    exact cons_erase h

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x : α
⊢ ∀ {y z : α}, x ≠ z → x ≠ y ∨ y ≠ z

Tactic:
y

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x y : α
⊢ ∀ {z : α}, x ≠ z → x ≠ y ∨ y ≠ z
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ l₁ ∪ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
by
        simp only [e, cons_union, insert_of_mem h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
xs : List α
⊢ (map f xs).dedup = map f xs.dedup

Tactic:
induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [map_cons]
    by_cases h : x ∈ xs
    · rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]
    · rw [dedup_cons_of_notMem h, dedup_cons_of_notMem <| (mem_map_of_injective hf).not.mpr h, ih,
        map_cons]

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

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
⊢ m = ↑[a] ↔ m = {a}

Tactic:
coe_singleton

Goal state after:
α : Type u_1
a : α
m : Multiset α
⊢ m = {a} ↔ m = {a}
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✝ : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun a ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
⊢ ⟨x, px⟩ = ⟨y, py⟩

Tactic:
congr

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun a ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
⊢ x = y
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

Tactic:
by
  simpa using add_union_distrib (a ::ₘ 0) s t

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ map (fun x ↦ f x) (if p a then {a} else 0) + filterMap (fun a ↦ if p a then some (f a) else none) s =
    (if p a then some {f a} else none).getD 0 + filterMap (fun a ↦ if p a then some (f a) else none) s

Tactic:
congr

Goal state after:
case cons.e_a
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ map (fun x ↦ f x) (if p a then {a} else 0) = (if p a then some {f a} else none).getD 0
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
sub_add_inter,

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) - filter p t = (filter p s).erase a - filter p t

Tactic:
congr

Goal state after:
case pos.e_a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) = (filter p s).erase a
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ insert a ∅ = {a}

Tactic:
LawfulSingleton.insert_empty_eq

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a} = {a}
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
h inst✝ : DecidablePred p
⊢ filter p s = filter p s

Tactic:
congr

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x✝¹ x✝ : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ { elems := s₁, complete := h₁ } = { elems := s₂, complete := h₂ }

Tactic:
congr

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x✝¹ x✝ : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ s₁ = s₂
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ s ⊆ {a}ᶜ ↔ a ∉ s

Tactic:
by
  rw [subset_compl_comm, singleton_subset_iff, mem_compl]

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
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ ↑s → f x = f x₂ → x = x₂

Tactic:
y

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
x : α
hx : x ∈ ↑s
y : α
⊢ y ∈ ↑s → f x = f y → x = y
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero (OfNat.ofNat m)
⊢ NeZero (OfNat.ofNat m)

Tactic:
suffices m % (n + m) = m by simpa [neZero_iff, Fin.ext_iff, OfNat.ofNat, this] using! NeZero.ne m
  apply Nat.mod_eq_of_lt
  simpa using! zero_lt_of_ne_zero (NeZero.ne n)

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ f ⟨↑i, ⋯⟩ = f (Fin.cast ⋯ i)

Tactic:
congr

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ((a :: l).get 0 :: ofFn fun i ↦ (a :: l).get i.succ) = a :: l

Tactic:
congr

Goal state after:
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i ↦ (a :: l).get i.succ) = l
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < i.succ ↔ p ≤ i.castSucc

Tactic:
iff_true_left H,

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p ≤ i.castSucc
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)

Tactic:
grind =>
    have : #(X ∪ Y) = #X + #(Y \ X)
    finish

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃ a, s = {a}

Tactic:
by
  cases s
  simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ (p.pred ⋯).predAbove i = i.castPred ⋯

Tactic:
rw [predAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h)]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ predAbove 0 i = if hi : i = 0 then 0 else i.pred hi

Tactic:
split_ifs with hi

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 i = 0

case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ cons (Fin.cons x₀ x 0) (tail (Fin.cons x₀ x)) = cons x₀ x

Tactic:
congr

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi

Tactic:
split_ifs with hi

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ (last n).predAbove i = last n

case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ (last n).predAbove i = i.castPred hi
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (b.castPred ⋯).succ

Tactic:
predAbove_succ_of_lt _ _ h,

Goal state after:
case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ b.succ.castPred ⋯ = (b.castPred ⋯).succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ x₀ 0 = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n 0)

Tactic:
Function.comp_apply,

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ x₀ 0 = cons (x₀ 0) x (Fin.cast ⋯ (castAdd n 0))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ x i = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)

Tactic:
Function.comp_apply,

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ x i = cons (x₀ 0) x (Fin.cast ⋯ (natAdd 1 i))
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
by
  /- While it is possible to give a "morally correct" proof
  by saying that both functions are strictly monotone and have the same range `{i, i.succAbove j}ᶜ`,
  we give a direct proof by case analysis to avoid extra dependencies. -/
  ext
  simp only [succAbove, predAbove, lt_def, val_castSucc, apply_dite Fin.val, val_pred, coe_castPred,
    dite_eq_ite, apply_ite Fin.val, val_succ]
  split_ifs <;> lia

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

Goal state before:
pp: n : ℕ
α : Sort u_2
a : α
f : Fin n → α
i : Fin n
⊢ (snoc f a ∘ castSucc) i = f i

Tactic:
Function.comp_apply,

Goal state after:
n : ℕ
α : Sort u_2
a : α
f : Fin n → α
i : Fin n
⊢ snoc f a i.castSucc = f i
Module: Mathlib.Data.Fin.Tuple.Basic

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

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

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

Goal state before:
pp: case intro
α : Type u
s : Set α
h : s.Finite
val✝ : Fintype ↑s
⊢ ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s

Tactic:
exact ⟨s.toFinset, fun _ => mem_toFinset⟩

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t

Tactic:
by
  simp only [← Finset.coe_ssubset, Finite.coe_toFinset]

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
this : Finite ↑s
⊢ t.Finite

Tactic:
exact Finite.Set.subset _ ht

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

Goal state before:
pp: α : Type u_1
L : List α
i : Nat
h : i < L.length
⊢ drop i (take (i + 1) L) = [L[i]]

Tactic:
induction L generalizing i with

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:
y

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y : β
⊢ ∀ {z : β}, x ≥ min y z ↔ 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 > min y z ↔ x > y ∨ x > z

Tactic:
y

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y : β
⊢ ∀ {z : β}, x > min y z ↔ 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:
y

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y : β
⊢ ∀ {z : β}, x ≥ max y z ↔ 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:
y

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

Goal state before:
pp: case succ
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ (f ∘ f^[i]) l[0] = l[i + 1]

Tactic:
Function.comp_apply,

Goal state after:
case succ
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f (f^[i] l[0]) = l[i + 1]
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum

Tactic:
by
  rw [← mem_range, ← ranges_flatten, mem_flatten]

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

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + n • filter p ha = (n • if p a then {a} else 0) + n • filter p ha

Tactic:
congr

Goal state after:
case refine_2.e_a
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) = n • if p a then {a} else 0
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List.chains r
acc : ∀ (a : α), a ∈ (↑l).head? → Acc r a
⊢ Acc (List.lex_chains r) l

Tactic:
obtain ⟨_ | ⟨a, l⟩, hl⟩ := l
  · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
  specialize acc a _
  · rw [List.head?_cons, Option.mem_some_iff]
  /- For an r-decreasing chain of the form a :: l, apply induction on a -/
  induction acc generalizing l with
  | intro a _ ih =>
    /- Bundle l with a proof that it is r-decreasing to form l' -/
    have hl' := (List.isChain_cons.1 hl).2
    let l' : List.chains r := ⟨l, hl'⟩
    have : Acc (List.lex_chains r) l' := by
      rcases l with - | ⟨b, l⟩
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      /- l' is accessible by induction hypothesis -/
      · apply ih b (List.isChain_cons_cons.1 hl).1
    /- make l' a free variable and induct on l' -/
    revert hl
    rw [(by rfl : l = l'.1)]
    clear_value l'
    induction this with
    | intro l _ ihl =>
      intro hl
      apply Acc.intro
      rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ih b hr
      · apply ihl ⟨m, (List.isChain_cons.1 hm).2⟩ hr

Goal state after: