mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
⊢ ∃ x, s ⊆ {x}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
    · exact ⟨Classical.arbitrary α, empty_subset _⟩
    · exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩

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

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h,
      castSucc_pred_eq_pred_castSucc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ ⇑{ toFun := f, inj' := h } '' Set.univ

Tactic:
Set.image_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ Set.range ⇑{ toFun := f, inj' := h }
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ s ⊂ Set.univ

Tactic:
Set.ssubset_univ_iff

Goal state after:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → ↑s
hf : Injective f
h : Fintype α
⊢ s ≠ Set.univ
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
⊢ Injective (natEmbeddingAux α)

Tactic:
rintro m n h
  let := Classical.decEq α
  wlog hmlen : m ≤ n generalizing m n
  · exact (this h.symm <| le_of_not_ge hmlen).symm
  by_contra hmn
  have hmn : m < n := lt_of_le_of_ne hmlen hmn
  refine (Classical.choose_spec (exists_notMem_finset
    ((Multiset.range n).pmap (fun m (_ : m < n) ↦ natEmbeddingAux α m)
      (fun _ ↦ Multiset.mem_range.1)).toFinset)) ?_
  refine Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, ?_⟩)
  rw [h, natEmbeddingAux]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
⊢ orderedInsert r a l = takeWhile (fun b ↦ decide ¬r a b) l ++ a :: dropWhile (fun b ↦ decide ¬r a b) l

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ orderedInsert r a [] = takeWhile (fun b ↦ decide ¬r a b) [] ++ a :: dropWhile (fun b ↦ decide ¬r a b) []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a head✝ : α
tail✝ : List α
tail_ih✝ :
  orderedInsert r a tail✝ = takeWhile (fun b ↦ decide ¬r a b) tail✝ ++ a :: dropWhile (fun b ↦ decide ¬r a b) tail✝
⊢ orderedInsert r a (head✝ :: tail✝) =
    takeWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝) ++ a :: dropWhile (fun b ↦ decide ¬r a b) (head✝ :: tail✝)
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

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
⊢ a ∈ orderedInsert r b [] ↔ a = b ∨ a ∈ []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b head✝ : α
tail✝ : List α
tail_ih✝ : a ∈ orderedInsert r b tail✝ ↔ a = b ∨ a ∈ tail✝
⊢ a ∈ orderedInsert r b (head✝ :: tail✝) ↔ a = b ∨ a ∈ head✝ :: tail✝
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

Goal state after:
case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
hl₁ : ∀ (a : α), a ∈ [] → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ [] → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x []) = orderedInsert s (f x) (map f [])

case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x head✝ : α
tail✝ : List α
tail_ih✝ :
  (∀ (a : α), a ∈ tail✝ → (r a x ↔ s (f a) (f x))) →
    (∀ (a : α), a ∈ tail✝ → (r x a ↔ s (f x) (f a))) →
      map f (orderedInsert r x tail✝) = orderedInsert s (f x) (map f tail✝)
hl₁ : ∀ (a : α), a ∈ head✝ :: tail✝ → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ head✝ :: tail✝ → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x (head✝ :: tail✝)) = orderedInsert s (f x) (map f (head✝ :: tail✝))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ insertionSort r l ~ l

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
⊢ insertionSort r [] ~ []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
tail_ih✝ : insertionSort r tail✝ ~ tail✝
⊢ insertionSort r (head✝ :: tail✝) ~ head✝ :: tail✝
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ Pairwise r l → insertionSort r l = l

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
⊢ Pairwise r [] → insertionSort r [] = []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise r tail✝ → insertionSort r tail✝ = tail✝
⊢ Pairwise r (head✝ :: tail✝) → insertionSort r (head✝ :: tail✝) = head✝ :: tail✝
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

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
hl : c <+ []
⊢ a :: c <+ orderedInsert r a []

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
c : List α
a : α
ha : ∀ (a' : α), a' ∈ c → r a a'
head✝ : α
tail✝ : List α
tail_ih✝ : c <+ tail✝ → a :: c <+ orderedInsert r a tail✝
hl : c <+ head✝ :: tail✝
⊢ a :: c <+ orderedInsert r a (head✝ :: tail✝)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Infinite
ht : (s \ t).Finite
⊢ (s ∩ t).Infinite

Tactic:
simpa using hs.sdiff ht

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False
⊢ ∀ ⦃x y z : ↑s⦄, x < y → y < z → False

Tactic:
by simpa only [SetCoe.forall'] using! h

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

Goal state before:
pp: m n : ℕ
p q : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
i j : Fin n
h : ∃ i, p i
⊢ decide (p h.choose) = true

Tactic:
simp only [h.choose_spec, decide_true]

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

Goal state before:
pp: case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j

Tactic:
· rwa [Fin.lt_def]

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

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False

Tactic:
mem_range

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u < a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False
Module: Mathlib.Data.List.Range

Goal state before:
pp: l : List ℕ
⊢ Pairwise Disjoint l.ranges

Tactic:
induction l with
  | nil => exact Pairwise.nil
  | cons a l hl =>
    simp only [ranges, pairwise_cons]
    constructor
    · intro s hs
      obtain ⟨s', _, rfl⟩ := mem_map.mp hs
      intro u hu
      rw [mem_map]
      rw [mem_range] at hu
      lia
    · rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map op (map unop l)).reverse.reverse.prod

Tactic:
map_map,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map (op ∘ unop) l).reverse.reverse.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr.inl
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 = n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
simp [← hn]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ l = [x]

Tactic:
by
  rw [rotate_eq_iff, rotate_singleton]

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []

Tactic:
by
  rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]

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

Goal state before:
pp: case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ (hd :: tl).length * n

Tactic:
exact Nat.le_mul_of_pos_left _ (by simp)

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

Goal state before:
pp: ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
⊢ (map (fun i ↦ (f i)⁻¹) m).prod = (map Inv.inv (map f m)).prod

Tactic:
map_map,

Goal state after:
ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
⊢ (map (fun i ↦ (f i)⁻¹) m).prod = (map (Inv.inv ∘ f) m).prod
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
a : α
l : List α
| map (fun x ↦ (x, a)) (map Prod.fst l.zipIdx)

Tactic:
map_map,

Goal state after:
α : Type u_1
a : α
l : List α
| map ((fun x ↦ (x, a)) ∘ Prod.fst) l.zipIdx
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul,
        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc,
        ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
⊢ Infinite ((i : ι) → π i)

Tactic:
by
  classical
  choose m n hm using fun i => exists_pair_ne (π i)
  refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
  simp_rw [update_eq_iff, update_of_ne hne] at h
  exact (hm x h.1.symm).elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(image2 f s t)

Tactic:
by
  rw [← image_prod]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ x = y

Tactic:
have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
this : ∀ (a : M), a ∈ ⊥
⊢ x = y
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
by
  rw [← closure_singleton_le_iff_mem, le_iSup_iff]
  simp only [closure_singleton_le_iff_mem]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
by
  rw [← closure_singleton_le_iff_mem, le_iSup_iff]
  simp only [closure_singleton_le_iff_mem]

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H

Tactic:
exact mul_mem hx (inv_mem hy)

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ ¬H ≤ K → H ≤ L

Tactic:
SetLike.not_le_iff_exists,

Goal state after:
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ (∃ x, x ∈ H ∧ ¬x ∈ K) → H ≤ L
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑e.symm) H) = H

Tactic:
map_map,

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map ((↑e).comp ↑e.symm) H = H
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K

Tactic:
map_map,

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map ((↑e.symm).comp ↑e) K = K
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable α
f : β → α
finv : α → Option β
linv : ∀ (b : β), finv (f b) = some b
b : β
⊢ (decode (encode (f b))).bind finv = some b

Tactic:
simp [Encodable.encodek, linv]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
P : α → Prop
encA : Encodable α
decP : DecidablePred P
x✝ : { a // P a }
v : α
h : P v
⊢ decodeSubtype (encodeSubtype ⟨v, h⟩) = some ⟨v, h⟩

Tactic:
by simp [encodeSubtype, decodeSubtype, encodek, h]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : map (↑(MulAut.conj y)) H = H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ map (↑(MulAut.conj (f y))) (map f H) = map f H

Tactic:
map_map,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : map (↑(MulAut.conj y)) H = H
hx : f y ∈ map f (normalizer ↑H)
this : (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)
⊢ map ((↑(MulAut.conj (f y))).comp f) H = map f H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * ({a} ∪ {b}) = s <• a ∪ s <• b

Tactic:
mul_union,

Goal state after:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * {a} ∪ s * {b} = s <• a ∪ s <• b
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Irrefl r
inst✝ : ∀ (i : ι), Std.Irrefl (s i)
i✝ : ι
a : α i✝
hi : r i✝ i✝
⊢ False

pp: case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Irrefl r
inst✝ : ∀ (i : ι), Std.Irrefl (s i)
i✝ : ι
a : α i✝
ha : s i✝ a a
⊢ False

Tactic:
· exact irrefl _ hi

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Irrefl r
inst✝ : ∀ (i : ι), Std.Irrefl (s i)
i✝ : ι
a : α i✝
ha : s i✝ a a
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ ∀ (x : M), x ∈ l → x ≤ l.prod

Tactic:
induction l

Goal state after:
case nil
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ ∀ (x : M), x ∈ [] → x ≤ [].prod

case cons
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ (head✝ :: tail✝).prod
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
obtain ⟨v, hv⟩ := exists_gt x.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ inr b ∈ s.disjSum t ↔ b ∈ t

Tactic:
rw [mem_disjSum, or_iff_right]
  · simp only [inr.injEq, exists_eq_right]
  rintro ⟨a, _, ha⟩
  exact inl_ne_inr ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (map inl s) + map f (map inr t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t

Tactic:
map_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map (f ∘ inl) s + map (f ∘ inr) t = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
by
  rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]; simp

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
by
  rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]; simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
hn : n ∈ range ↑⊥ ∧ n ∈ s
⊢ False

Tactic:
mem_range

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b

Tactic:
induction l

Goal state after:
case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ [].maximum ↔ ∃ b, b ∈ [] ∧ a ≤ b

case cons
α : Type u_1
inst✝ : LinearOrder α
l : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ↑a ≤ tail✝.maximum ↔ ∃ b, b ∈ tail✝ ∧ a ≤ b
⊢ ↑a ≤ (head✝ :: tail✝).maximum ↔ ∃ b, b ∈ head✝ :: tail✝ ∧ a ≤ b
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : powersetAux' l₁✝ ~ powersetAux' l₂✝
⊢ powersetAux' (x✝ :: l₁✝) ~ powersetAux' (x✝ :: l₂✝)

Tactic:
simp only [powersetAux'_cons]
    exact IH.append (IH.map _)

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
H : ∃ a ∈ s, f a = (image f s).max' hne
⊢ motive s

Tactic:
rcases H with ⟨a, has, hfa⟩

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 s
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
⊢ powersetCard n (map f s) = map (map f) (powersetCard n s)

Tactic:
by
  induction s using Multiset.induction generalizing n with
  | empty => cases n <;> simp [powersetCard_zero_left]
  | cons t s ih => cases n <;> simp [ih]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)

Tactic:
by
  let := Subtype.semilatticeSup Psup
  let := Subtype.orderBot Pbot
  apply apply_sup_eq_sup_comp Subtype.val <;> intros <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite

Tactic:
by
  have := hs.to_subtype
  simpa [range] using finite_range fun x : s => F x x.2

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃! i, i ∈ s ∧ y ∈ f i

Tactic:
refine existsUnique_of_exists_of_unique ?ex ?unique
  · simpa only [mem_iUnion, exists_prop] using hy
  · rintro i j ⟨his, hi⟩ ⟨hjs, hj⟩
    exact h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
h : s.Nonempty
f : β → α
⊢ ↑(s.sup f) = s.sup (WithBot.some ∘ f)

Tactic:
by simp only [← sup'_eq_sup h, coe_sup' h]

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

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ ↑(f i) ≤ ⨆ i ∈ s, ↑(f i)

Tactic:
apply le_biSup _ h

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

Goal state before:
pp: case pos
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
⊢ ⨅ i ∈ s, ↑(f i) ≤ ↑(⨅ (_ : i ∈ s), f i)

Tactic:
simpa only [iInf_pos h] using by apply biInf_le _ h

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

Goal state before:
pp: α : Type u
ι : Sort v
κ : ι → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
intro ι κ _ f

Goal state after:
α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝² : Order.Frame α
inst✝¹ : Finite ι✝
f✝ : (a : ι✝) → κ✝ a → α
ι : Type v
κ : ι → Type w
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
f : ι → α
⊢ univ.sup' ⋯ f = ⨆ i, f i

Tactic:
simp [sup'_eq_csSup_image, iSup]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ ⨆ i, ↑i = sSup s

Tactic:
rw [← sSup_range, Subtype.range_coe]

Goal state after: