mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ.last
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
⊢ cons a (snoc q b) (last n).succ = snoc (cons a q) b (last n).succ

Tactic:
| last =>

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
⊢ append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
rw [Fin.append_left]

Goal state after:
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)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ (last n)
⊢ i.castSucc = last n

Tactic:
| last =>

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

Goal state before:
pp: case last.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
h : snoc x x₀ (last n) = snoc x x₀ (last n)
⊢ last n = last n

Tactic:
| last =>

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

Goal state before:
pp: case last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
h : snoc x x₀ (last n) = snoc x x₀ j
⊢ last n = j

Tactic:
| last =>

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

Goal state before:
pp: case last
n : ℕ
P : Fin (n + 1) → Prop
hi : P (last n)
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
| last =>

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

Goal state before:
pp: case i
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ Fin (n + 1)

Tactic:
exact rev i

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ op (op (fold op b₁ s₁) a) (fold op b₂ b) = op (fold op b₁ s₁) (op a (fold op b₂ b))

Tactic:
ha.assoc

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ op (fold op b₁ s₁) (op a (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))

Tactic:
ha.assoc

Goal state after:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a))) =
    op (f a) (op (fold op u₁ (map f b)) (op (fold op u₂ (map g b)) (g a)))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ j.contractNth op g k = g k.succ

Tactic:
rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]

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

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
· exact .rel ab

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h✝ : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
x✝¹ : α
h : x✝¹ ≠ a
x✝ : x✝¹ ∈ filter p (a :: as).dedup
⊢ (if a = x✝¹ then 1 else 0) = 0

Tactic:
simp [h.symm]

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

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

Tactic:
by
  rcases l.length.zero_le.eq_or_lt with hl | hl
  · simp [eq_nil_of_length_eq_zero hl.symm]
  rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
⊢ List.Pairwise rᶜ l.reverse

Tactic:
refine List.pairwise_iff_forall_infix.mpr fun l' hne hsub ↦ ?_

Goal state after:
α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
l' : List α
hne : 1 < l'.length
hsub : l' <:+: l.reverse
⊢ rᶜ (l'.head ⋯) (l'.getLast ⋯)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ≤ s.card • t ↔ s ⊆ t

Tactic:
by
  classical
  refine ⟨fun hle ↦ Subset.trans (subset_of_le hle) (t.smul_subset_self s.card), ?_⟩
  refine fun hsub ↦ le_iff_count.mpr fun a ↦ ?_
  by_cases! has : a ∉ s
  · simp [count_eq_zero_of_notMem has]
  grw [count_le_card, count_nsmul, ← one_le_count_iff_mem.mpr <| mem_of_subset hsub has, mul_one]

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

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ take (n % l'.length) l' ++ drop (n % l'.length) l' = l'

Tactic:
take_append_drop

Goal state after:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l' = l'
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s t : Multiset M
l₁ l₂ : List M
⊢ (⟦l₁⟧ + ⟦l₂⟧).prod = prod ⟦l₁⟧ * prod ⟦l₂⟧

Tactic:
by simp [List.prod_append]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ prod 0 = m.prod ^ 0

Tactic:
pow_zero

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ prod 0 = 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
apply zero_lt_succ

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
⊢ l.offDiag.Nodup

Tactic:
let := Classical.decEq α
  rw [nodup_iff_count_le_one]
  rintro ⟨x, y⟩
  rw [count_offDiag_eq_mul_sub_ite l x y]
  grind

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

Goal state before:
pp: case neg.hf.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ∀ (a_1 : (a : α) → a ∈ m → β a),
    a_1 ∈ n → Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' a_1) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b a_1)

Tactic:
intro f

Goal state after:
case neg.hf.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
f : (a : α) → a ∈ m → β a
⊢ f ∈ n → Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!

Tactic:
choose_mul_factorial_mul_factorial h,

Goal state after:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = n !
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n r : ℕ
hr : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
induction hr using decreasingInduction with
  | self => rfl
  | of_succ k hk ih => exact (choose_le_succ_of_lt_half_left hk).trans ih

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
refine fun _ ↦ Nat.stabilises_of_monotone mono (fun n ↦ set_fintype_card_le_univ (S ^ n))
    fun n h ↦ le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) ?_)

Goal state after:
case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ x ^ 0 ∈ S

Tactic:
pow_zero

Goal state after:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
⊢ 1 ∈ S
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j

Tactic:
by simp_rw [preimage_iUnion]

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

Goal state before:
pp: case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ↑(closure (s \ t))

Tactic:
rw [SetLike.mem_coe, Submonoid.mem_closure]

Goal state after:
case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ ∀ (S : Submonoid M), s \ t ⊆ ↑S → x ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

Tactic:
rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
  simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s \ {1} ∪ {1}) = closure s

Tactic:
sdiff_union_self,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s ∪ {1}) = closure s
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ x ∈ s ⊔ t → ∃ y ∈ s, ∃ z ∈ t, y * z = x

pp: case mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t

Tactic:
· intro hx; rw [sup_eq_closure] at hx
    refine closure_induction ?_ ?_ ?_ ?_ hx
    · rintro x (hx | hx)
      · exact ⟨x, hx, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, x, hx, by simp⟩
    · exact ⟨1, s.one_mem, 1, t.one_mem, by simp⟩
    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨y₁ * y₂, s.mul_mem hy₁ hy₂,
            (y₂⁻¹ * z₁ * y₂) * z₂, t.mul_mem (ht.conj_mem' z₁ hz₁ y₂) hz₂, by simp [mul_assoc]⟩
    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨y⁻¹, s.inv_mem hy,
            y * z⁻¹ * y⁻¹, ht.conj_mem z⁻¹ (t.inv_mem hz) y, by simp [mul_assoc]⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Tactic:
refine
    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_

Goal state after:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun x2 ↦ 1 • x2) '' s = s

Tactic:
by simp_rw [one_smul, image_id']

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

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
obtain hab | hba := total_of (s i) a b

Goal state after:
case inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
cases x with | h x
    cases y with | h y
    simp only [Prod.Lex.toLex_lt_toLex] at h
    rcases h with (h | h)
    · obtain ⟨v, hv⟩ := exists_lt y.2
      use toLex (y.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]
    · obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

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

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
⊢ ∀ {o : Option α}, b ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r b m

Tactic:
o

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
⊢ b ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r b m
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ 0 ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
exact Nat.zero_le _

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

Goal state before:
pp: case none
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) none = max none ↑a

Tactic:
exact (max_eq_right bot_le).symm

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
have wf : ↑m < x := by simpa using! hmt.mp (List.maximum_mem hmax)

Goal state after:
case coe
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
m : ↑s
hmax : t.maximum = ↑m
wf : ↑m < x
⊢ ∃ a, ofNat s a = ⟨x, hx⟩
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

Tactic:
simp only [foldr]
      exact le_max_of_le_left h

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

Goal state before:
pp: α : Type u_1
t : Finset α
inst✝ : DecidableEq α
s : Finset (Finset α)
⊢ s.biUnion id ⊆ t ↔ s ⊆ t.powerset

Tactic:
by
  aesop (add simp subset_iff)

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

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
h : none ∈ s
⊢ #(eraseNone s) = #s - 1

Tactic:
classical rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
by
  induction hs using Nonempty.cons_induction <;> simp [*]

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i

Tactic:
by
  induction hs using Nonempty.cons_induction <;> simp [*]

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

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
max_eq_left le

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⩿ x ∧ b = Function.update a i x) → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
rintro ⟨i, x, h, rfl⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⩿ x
⊢ ∃ i_1, a i_1 ⩿ Function.update a i x i_1 ∧ ∀ (j : ι), j ≠ i_1 → a j = Function.update a i x j
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i x, a i ⋖ x ∧ b = Function.update a i x) → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
rintro ⟨i, x, h, rfl⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⋖ x
⊢ ∃ i_1, a i_1 ⋖ Function.update a i x i_1 ∧ ∀ (j : ι), j ≠ i_1 → a j = Function.update a i x j
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ (∃ i x, x ⩿ b i ∧ a = Function.update b i x) → ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
rintro ⟨i, x, h, rfl⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⩿ b i
⊢ ∃ i_1, Function.update b i x i_1 ⩿ b i_1 ∧ ∀ (j : ι), j ≠ i_1 → Function.update b i x j = b j
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
⊢ (∃ i x, x ⋖ b i ∧ a = Function.update b i x) → ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j

Tactic:
rintro ⟨i, x, h, rfl⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⋖ b i
⊢ ∃ i_1, Function.update b i x i_1 ⋖ b i_1 ∧ ∀ (j : ι), j ≠ i_1 → Function.update b i x j = b j
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
j : ι
hj : MaximalFor (fun x ↦ x ∈ s) f j
hji : f j ≤ f i
⊢ ∃ i_1, MaximalFor (fun x ↦ x ∈ cons i s hi) f i_1

Tactic:
refine ⟨i, mem_cons_self .., ?_⟩
      simp only [mem_cons, forall_eq_or_imp, imp_self, true_and]
      exact fun k hk hik ↦ _root_.trans (hj.2 hk <| _root_.trans hji hik) hji

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ {x ∈ Finset.Ico a b | x ≤ a}.val = {a}

Tactic:
Finset.Ico_filter_le_left hab

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ {a}.val = {a}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case zero
a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(range a)

Tactic:
rintro k hk l hl (hkl : k % a = l % a)

Goal state after:
case zero
a k : ℕ
hk : k ∈ ↑(range a)
l : ℕ
hl : l ∈ ↑(range a)
hkl : k % a = l % a
⊢ k = l
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
⊢ Set.InjOn (fun x ↦ x % a) ↑((insert (n + a) (Ico n (n + a))).erase n)

Tactic:
rintro k hk l hl (hkl : k % a = l % a)

Goal state after:
case succ
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
⊢ k = l
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = (n + a) % a
hln : n + a ≠ n
⊢ k = n + a

Tactic:
rw [add_mod_right] at hkl
      suffices k = n by contradiction
      refine ih hk ?_ hkl
      simpa using Nat.lt_add_of_pos_right (n := n) ha

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : Std.Refl r
⊢ WellQuasiOrdered r

Tactic:
intro f

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : Std.Refl r
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)