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

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ Fin.cast ⋯

Tactic:
refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
  · rw [append_left, Function.comp_apply]
    refine congr_arg u (Fin.ext ?_)
    simp
  · exact (Fin.cast hv r).elim0

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

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

Tactic:
le_castSucc_iff,

Goal state after:
case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc < (i.pred ⋯).succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
⊢ append xs ys ∘ Sum.elim (castAdd n) (natAdd m) = Sum.elim xs ys

Tactic:
by
  ext (i | j) <;> simp

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

Goal state before:
pp: α : Type u_1
l : List α
x y : α
hne : x ≠ y
⊢ x ∈+ y :: l ↔ x ∈+ l

Tactic:
simp [duplicate_cons_iff, hne.symm]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast ⋯

Tactic:
generalize_proofs h
  apply funext
  rw [(Fin.rightInverse_cast h.symm).surjective.forall]
  refine Fin.addCases (fun l => ?_) fun r => ?_
  · simp [modNat, Nat.mod_eq_of_lt l.is_lt]
  · simp [modNat]

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

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = m

Tactic:
conv_rhs => rw [← Fintype.card_fin m]

Goal state after:
m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = card (Fin m)
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
by
  induction i using lastCases with
  | cast i =>
    induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)
  | last =>
    induction j using lastCases with
    | cast j =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [h] at hx₀
      apply hx₀.elim (Set.mem_range_self j)
    | last => simp

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

Goal state before:
pp: n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
⊢ Injective (snoc x x₀) ↔ Injective x ∧ ¬x₀ ∈ Set.range x

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩

Goal state after:
case refine_1
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ Injective x

case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ ¬x₀ ∈ Set.range x
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ List.Pairwise (fun x1 x2 ↦ x1 ≤ x2) (map (⇑e) l) ↔ List.Pairwise (fun x1 x2 ↦ x1 ≤ x2) l

Tactic:
e.pairwise_listMap

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

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ (if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none) =
    some (Fin.find (fun x ↦ p x = true) ⋯)

Tactic:
exists_eq_true_of_isSome_find? h,

Goal state after:
n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ (if h_1 : True then some (Fin.find (fun x ↦ p x = true) ⋯) else none) = some (Fin.find (fun x ↦ p x = true) ⋯)
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 : ↑k = ↑j
this : ¬↑k < ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Tactic:
rw [contractNth, if_neg this, if_pos h]

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:
| insert a s ha IH =>

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:
| insert a s ha IH =>

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

Goal state before:
pp: α : Type u_3
l : List α
R : α → α → Prop
⊢ Pairwise R l ↔ ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)

Tactic:
refine l.pairwise_iff_getElem.trans ⟨fun h l' hne ⟨l₁, l₂, hl⟩ ↦ ?_, fun h i j hi hj hij ↦ ?_⟩
  · grind [getElem_append_left', getElem_append_right']
  · grind [h _ _ <| List.drop_suffix i _ |>.isInfix.trans <| l.take_prefix (j + 1) |>.isInfix]

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

Goal state before:
pp: α : Type u
a : α
n k : ℕ
⊢ ((replicate n a).rotate k).length = n

Tactic:
rw [length_rotate, length_replicate]

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

Goal state before:
pp: case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0 • s
⊢ a ∈ s

Tactic:
zero_nsmul

Goal state after:
case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0
⊢ a ∈ s
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
⊢ a ∈ s

Tactic:
by
  induction n with
  | zero =>
    rw [zero_nsmul] at h
    exact absurd h (notMem_zero _)
  | succ n ih =>
    rw [succ_nsmul, mem_add] at h
    exact h.elim ih id

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ MulOpposite.unop (f l.prod) = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

Tactic:
map_list_prod f l,

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ MulOpposite.unop (map (⇑f) l).prod = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + k + n) % l.length

Tactic:
← add_mod_mod,

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + k + n % l.length) % l.length
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (bind 0 fun x ↦ {f x}) = map f 0

Tactic:
zero_bind,

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = map f 0
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) 0)

Tactic:
zero_bind,

Goal state after:
case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) 0 = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) 0)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
L : List α
hL : L ≠ []
⊢ L.getLast hL :: L.dropLast ~r L

Tactic:
induction L using List.reverseRecOn with
  | nil => simp at hL
  | append_singleton a L _ =>
    simp only [getLast_append, dropLast_concat]
    apply IsRotated.symm
    apply isRotated_concat

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
⊢ r (cons m a✝ b₁ f₁ a ha) (cons m a✝ b₂ f₂ a ha)

Tactic:
dsimp [cons]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
⊢ r (if h : a = a✝ then ⋯ ▸ b₁ else f₁ a ⋯) (if h : a = a✝ then ⋯ ▸ b₂ else f₂ a ⋯)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
h : n < k
⊢ 0 = k ! * 0

Tactic:
Nat.mul_zero

Goal state after:
case inl
n k : ℕ
h : n < k
⊢ 0 = 0
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
⊢ Finite (α ↪ β)

Tactic:
have : Finite α := Finite.of_injective _ f.injective

Goal state after:
case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
this : Finite α
⊢ Finite (α ↪ β)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (z, w) ∈ ⋃ x, s x ×ˢ t x ↔ (z, w) ∈ (⋃ x, s x) ×ˢ ⋃ x, t x

Tactic:
simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty

Tactic:
by rw [pow_succ]; exact hs.pow.mul hs

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

Goal state before:
pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : f x = 1
⊢ f x * f x⁻¹ = 1

Tactic:
rw [← map_mul, mul_inv_cancel, map_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ comap f H = f.ker ↔ Disjoint H f.range

Tactic:
← H.ker_le_comap f |>.ge_iff_eq',

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ comap f H ≤ f.ker ↔ Disjoint H f.range
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
show unpair (a * a + a + b) = (a, b)
    have ae : sqrt (a * a + (a + b)) = a := by
      rw [sqrt_add_eq]
      exact Nat.add_le_add_left (le_of_not_gt h) _
    simp [unpair, ae, Nat.add_assoc, Nat.add_sub_cancel_left]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (n + 1).boddDiv2 = ((n + 1).bodd, (n + 1).div2)

Tactic:
rw [boddDiv2, ih]

Goal state after:
case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (match (n.bodd, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
o : Option α
⊢ (Nat.casesOn (Option.casesOn o zero fun a ↦ (encode a).succ) (some none) fun m ↦ Option.map some (decode m)) = some o

Tactic:
cases o

Goal state after:
case none
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
⊢ (Nat.casesOn (Option.casesOn none zero fun a ↦ (encode a).succ) (some none) fun m ↦ Option.map some (decode m)) =
    some none

case some
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
val✝ : α
⊢ (Nat.casesOn (Option.casesOn (some val✝) zero fun a ↦ (encode a).succ) (some none) fun m ↦
      Option.map some (decode m)) =
    some (some val✝)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β))
      ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (decode (unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β)

Goal state after:
case none.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) none) =
    none.bind fun a ↦ Option.map (Prod.mk a) none

case none.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) (none.bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    none.bind fun a ↦ Option.map (Prod.mk a) (some val✝)

case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝ : α
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝).bind fun a ↦ Option.map (Sigma.mk a) none) =
    (some val✝).bind fun a ↦ Option.map (Prod.mk a) none

case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β)) ((some val✝¹).bind fun a ↦ Option.map (Sigma.mk a) (some val✝)) =
    (some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
A : Type u_4
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : H.Characteristic
inst✝ : K.Characteristic
⊢ (H ⊔ K).Characteristic

Tactic:
by
  simp_all [characteristic_iff_map_eq, map_sup]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer ↑H

Tactic:
← subgroupOf_eq_top,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ (normalizer ↑H).subgroupOf K = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ normalClosure (s ∪ t) = normalClosure s ⊔ normalClosure t

Tactic:
by
  simp_rw [normalClosure, Group.conjugatesOfSet_union, closure_union]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
α : Type u_6
β : Type u_7
e : α ≃ β
⊢ ∀ (x y : FreeMonoid α), (map ⇑e) (x * y) = (map ⇑e) x * (map ⇑e) y

Tactic:
simp [map_mul]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
α : Type u_6
β : Type u_7
e : α ≃ β
⊢ ∀ (x y : FreeMonoid α), (map ⇑e) (x * y) = (map ⇑e) x * (map ⇑e) y

Tactic:
by simp [map_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = (hd :: tl).maximum

Tactic:
rw [maximum_cons, foldr, WithBot.coe_max]
    by_cases h : tl = []
    · simp [h]
    · simp [IH h]

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

Goal state before:
pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive s

Tactic:
rw [← insert_erase has]

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive (Insert.insert a (s.erase a))
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s

Tactic:
unfold sublistsLenAux; simp

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

Goal state before:
pp: α : Type u
a : Set α
h : a.Finite
s : Set α
⊢ s ∈ {b | b ⊆ a} ↔ s ∈ ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)

Tactic:
simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset,
    ← and_assoc, Finset.coeEmb] using h.subset

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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ (Disjoint on fun i ↦ ⨆ i' ∈ t, f (i, i')) i j

Tactic:
Function.onFun,

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ Disjoint (⨆ i' ∈ t, f (i, i')) (⨆ i' ∈ t, f (j, i'))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ (Disjoint on fun i' ↦ ⨆ i ∈ s, f (i, i')) i j

Tactic:
Function.onFun,

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ Disjoint (⨆ i_1 ∈ s, f (i_1, i)) (⨆ i ∈ s, f (i, j))
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
a : α
o : Option α
⊢ a ∈ o.toFinset ↔ a ∈ o

Tactic:
cases o

Goal state after:
case none
α : Type u_1
a : α
⊢ a ∈ none.toFinset ↔ a ∈ none

case some
α : Type u_1
a val✝ : α
⊢ a ∈ (some val✝).toFinset ↔ a ∈ some val✝
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
o : Option α
⊢ o.toFinset.card = o.elim 0 1

Tactic:
cases o

Goal state after:
case none
α : Type u_1
⊢ none.toFinset.card = none.elim 0 1

case some
α : Type u_1
val✝ : α
⊢ (some val✝).toFinset.card = (some val✝).elim 0 1
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ image f s

Tactic:
by
  rw [ciSup_eq_max'_image _ h]
  exact max'_mem (image f s) _

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

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (hs.toFinset.sup g) = hs.toFinset.sup (⇑f ∘ g)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Tactic:
simp only [Finset.sup_eq_iSup, hs.mem_toFinset, comp_apply] at this

Goal state after:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
s : Set ι
hs : s.Finite
f : F
g : ι → α
this : f (⨆ a ∈ s, g a) = ⨆ a ∈ s, f (g a)
⊢ f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i

Tactic:
refine le_antisymm ?_ ?_
  · exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
  · exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i j

Tactic:
Function.onFun,

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ Disjoint (map (Embedding.sigmaMk i) (t i)) (map (Embedding.sigmaMk j) (t j))
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
by
  classical
  simp_rw [map_eq_image, subset_image_iff, eq_comm]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
⊢ Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, mem_range_self x⟩, ?_⟩⟩

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x)
y : α
hy : (fun x ↦ f x ∈ t) y
⊢ y ≤ x → x ≤ y

case refine_2
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
h : Minimal (fun x ↦ f x ∈ t) x
⊢ ∀ ⦃y : β⦄, (fun x ↦ x ∈ t ∩ range ⇑f) y → y ≤ f x → f x ≤ y
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬b ≤ x} ↔ a ≤ x ∧ x < b

Tactic:
Finset.mem_filter,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ finsetIcc a b ∧ ¬b ≤ x ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a} ↔ a < x ∧ x ≤ b

Tactic:
Finset.mem_filter,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ finsetIcc a b ∧ ¬x ≤ a ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x} ↔ a < x ∧ x < b

Tactic:
Finset.mem_filter,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ finsetIcc a b ∧ ¬x ≤ a ∧ ¬b ≤ x ↔ a < x ∧ x < b