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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

pp: case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Tactic:
· rintro ⟨a, b, c, t, hsub, hab, hac, hbc, rfl⟩
      exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩

Goal state after:
case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
ext i
  refine Fin.addCases ?_ ?_ i <;> clear i
  · intro i
    rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
    exact Fin.cons_zero _ _
  · intro i
    rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
    exact Fin.cons_succ _ _ _

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

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

Tactic:
ext i
  cases i using Fin.cases with
  | zero => simp
  | succ j =>
    cases j using Fin.lastCases with
    | last => simp
    | cast j =>
      rw [cons_succ]
      simp [← castSucc_succ]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
by
    by_cases h : a ≼ b
    · simp [h]
    · simpa [h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ h.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
by
  rw [Finset.Nontrivial, h.coe_toFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
g : γ ↪ α
s : Finset γ
⊢ fold op b f (map g s) = fold op b (f ∘ ⇑g) s

Tactic:
simp only [fold, map, Multiset.map_map]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ ∀ (a a' : Fin n), a = a' → i.removeNth (j.removeNth m) a ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m) a'

Tactic:
rintro k _ rfl

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ i.removeNth (j.removeNth m) k ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m) k
Module: Mathlib.Data.List.Range

Goal state before:
pp: a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u : List ℕ
⊢ ∀ {b : List ℕ}, u.Disjoint b → (map (fun x ↦ a + x) u).Disjoint (map (fun x ↦ a + x) b)

Tactic:
v

Goal state after:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ u.Disjoint v → (map (fun x ↦ a + x) u).Disjoint (map (fun x ↦ a + x) v)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬[] ∈ l₁ :: l₂ :: L
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
rw [mem_cons, not_or, ← Ne] at hL
    rw [flatten_cons, isChain_append, isChain_flatten hL.2, forall_mem_cons, isChain_cons_cons]
    rw [mem_cons, not_or, ← Ne] at hL
    simp only [forall_mem_cons, and_assoc, flatten_cons, head?_append_of_ne_nil _ hL.2.1.symm]
    exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
ha : IsChain (fun x1 x2 ↦ x1 > x2) [a]
hmas : b :: bs ≤ []
⊢ a > b

Tactic:
simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas

Goal state after:
case cons.nil
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
ha : IsChain (fun x1 x2 ↦ x1 > x2) [a]
hmas : b :: bs < []
⊢ a > b
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: 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

Tactic:
split_ifs with hp

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (n • {a}) = n • {a}

case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ (n • m + m).prod = m.prod ^ n * m.prod

Tactic:
prod_add,

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ (n • m).prod * m.prod = m.prod ^ n * m.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mp
α : Type u
l l' : List α
h : l.reverse ~r l'
⊢ l ~r l'.reverse

Tactic:
simpa using h.reverse

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

Goal state before:
pp: case mpr
α : Type u
l l' : List α
h : l ~r l'.reverse
⊢ l.reverse ~r l'

Tactic:
simpa using h.reverse

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

Goal state before:
pp: α : Type u
l' l : List α
h : l' ∈ l.cyclicPermutations
⊢ l'.length = l.length

Tactic:
obtain ⟨k, hk, rfl⟩ := get_of_mem h

Goal state after:
α : Type u
l : List α
k : Fin l.cyclicPermutations.length
h : l.cyclicPermutations.get k ∈ l.cyclicPermutations
⊢ (l.cyclicPermutations.get k).length = l.length
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ f ⁻¹' range f = univ

Tactic:
preimage_range

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ univ = univ
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
⊢ f '' s⁻¹ = (g '' s)⁻¹

Tactic:
by
  conv_rhs => rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)

Tactic:
exact fun x hx y hy i => mem_image2_of_mem hx (hy _)

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Tactic:
· rintro ⟨a, rfl, ha⟩
    exact ha.set

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s : Set α
⊢ IsUnit s ↔ ∃ a, s = {a}

Tactic:
by
  simp only [isUnit_iff, Group.isUnit, and_true]

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : MulOneClass M
s : Set M
motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
⊢ motive x 1 hx ⋯

Tactic:
exact one_right x hx

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S

Tactic:
rw [hb, ha]
    simp only [mul_assoc, mul_inv_rev]

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

Goal state before:
pp: case one
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
⊢ p x 1 hx ⋯

Tactic:
exact one_right x hx

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
f : G →* N
hf : Injective ⇑f
⊢ Surjective ⇑(f.codRestrict f.range ⋯)

Tactic:
by
      rintro ⟨x, y, rfl⟩
      exact ⟨y, rfl⟩

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 G
x y : G
hy : y ∈ H
hy' : f y = f x
⊢ y * (y⁻¹ * x) ∈ H ⊔ f.ker

Tactic:
exact mul_mem_sup hy (by simp [mem_ker, hy'])

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g = ⊥ ↔ g = 1

Tactic:
eq_bot_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g ≤ ⊥ ↔ g = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ normalClosure s = ⊥ ↔ s ⊆ {1}

Tactic:
eq_bot_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ normalClosure s ≤ ⊥ ↔ s ⊆ {1}
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure s ≤ normalClosure s

Tactic:
by
  simp only [subset_normalClosure, closure_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ (map f) ((map g) x) = (map (f ∘ g)) x

Tactic:
unfold map
  simp only [MonoidHom.coe_mk, OneHom.coe_mk, toList_ofList, List.map_map]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : (B'.subgroupOf B).Normal
⊢ ((A ⊓ B').subgroupOf (A ⊓ B)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf A.le_normalizer hN) inf_normalizer_le_normalizer_inf

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

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ max (map f l).prod (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
by
  rw [max_le_iff]
  constructor <;> apply List.prod_le_prod' <;> intros
  · apply le_max_left
  · apply le_max_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b : β
⊢ ∃ b_1, toLex (a, b) < b_1

Tactic:
obtain ⟨c, h⟩ := exists_gt b

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b c : β
h : b < c
⊢ ∃ b_1, toLex (a, b) < b_1
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Tactic:
by
  simp_rw [disjSum, mem_add, mem_map]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝² : Denumerable α✝
inst✝¹ : Denumerable β✝
α : Type ?u.10
β : Type ?u.15
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
by
      simp [decode_ofEquiv, encode_ofEquiv]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α),
    (s.sup ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a) → ((a_1 ::ₘ s).sup ≤ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ≤ a)

Tactic:
simp +contextual [or_imp, forall_and]

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:
let := Subtype.semilatticeSup Psup

Goal state after:
α : 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 }
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x

Tactic:
obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys

Goal state after:
case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ x ∈ s, (insert a r).sup id ≤ x
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯

Tactic:
refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Goal state after:
case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯

case refine_2
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯
⊢ a ∈ s.powerset
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨆ j, f i j
i : ι
hx : (fun i ↦ ⨆ j, f i j) i = x
⊢ (fun i ↦ ⨆ j, f i j) i ≤ a ⊔ sSup ∅

Tactic:
cases isEmpty_or_nonempty <| κ i

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨆ j, f i j
i : ι
hx : (fun i ↦ ⨆ j, f i j) i = x
h✝ : IsEmpty (κ i)
⊢ (fun i ↦ ⨆ j, f i j) i ≤ a ⊔ sSup ∅

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨆ j, f i j
i : ι
hx : (fun i ↦ ⨆ j, f i j) i = x
h✝ : Nonempty (κ i)
⊢ (fun i ↦ ⨆ j, f i j) i ≤ a ⊔ sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i

Tactic:
cases isEmpty_or_nonempty <| κ i

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : IsEmpty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : Nonempty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ some ⁻¹' range some = univ

Tactic:
preimage_range

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ univ = univ
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b ⊆ sigmaLift g a b

Tactic:
rintro x hx

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
π : β → Type u_1
s : Finset β
e : α ≃ β
x : (a : α) → π (e a)
b : ↥s
⊢ (s.restrict ∘ ⇑(Equiv.piCongrLeft π e)) x b =
    (⇑(Equiv.piCongrLeft (fun b ↦ π ↑b) (e.restrictPreimageFinset s)) ∘ (s.preimage ⇑e ⋯).restrict) x b

Tactic:
simp only [comp_apply, restrict, Equiv.piCongrLeft_apply_eq_cast,
    Equiv.restrictPreimageFinset_symm_apply_coe]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
P : α → Prop
a : α
ha : P a
⊢ ∃ b, b ≤ a ∧ Minimal P b

Tactic:
obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ :=
    exists_minimal_of_wellFoundedLT (fun b ↦ b ≤ a ∧ P b) ⟨a, le_rfl, ha⟩
  exact ⟨b, hba, hb, fun c hc hcb ↦ hbmin ⟨hcb.trans hba, hc⟩ hcb⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hca : c ≤ a
⊢ {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico a b).val

Tactic:
Finset.Ico_filter_le_of_le_left hca

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hca : c ≤ a
⊢ (Finset.Ico a b).val = (Finset.Ico a b).val
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
⊢ filter (fun x ↦ x ≤ a) (Ico a b) = {a}

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
  rfl

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ m ∉ s

Tactic:
classical
  cases eq_empty_or_nonempty s with
  | inl h => subst h; apply notMem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Iic n

Tactic:
rw [range_succ_eq_Icc_zero]

Goal state after:
n : ℕ
⊢ Icc 0 n = Iic n
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n a : ℕ
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = range a

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · rw [range_zero, add_zero, Ico_self, image_empty]
  ext i
  simp only [mem_image, mem_range, mem_Ico]
  constructor
  · rintro ⟨i, _, rfl⟩
    exact mod_lt i ha.bot_lt
  intro hia
  have hn := Nat.mod_add_div n a
  obtain hi | hi := lt_or_ge i (n % a)
  · refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
    · rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]
      refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)
      simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le
    · refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_
      rw [Nat.mul_add, mul_one, ← add_assoc, hn]
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
  · refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · lia
    · lia
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r r' : α → α → Prop
s t : Set α
h : t.WellFoundedOn r'
hle : r ≤ r'
hst : s ⊆ t
⊢ s.WellFoundedOn r

Tactic:
by
  rw [wellFoundedOn_iff] at *
  exact Subrelation.wf (fun xy => ⟨hle _ _ xy.1, hst xy.2.1, hst xy.2.2⟩) h

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ico a b) = Ico ↑a ↑b

Tactic:
by
  rw [subtype_Ico_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ico] at hx
  exact hp hx.1 hx.2.le a.prop b.prop

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
a : α
⊢ a ∈ Ici ⊥ ↔ a ∈ univ

Tactic:
simp only [mem_Ici, bot_le, mem_univ]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
⊢ m = n

pp: case refine_2
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ IsAntichain r (range f)

Tactic:
· obtain h | h | h := lt_trichotomy m n
    · refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _
    · exact h
    · refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _

Goal state after:
case refine_2
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ IsAntichain r (range f)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ ∃ x ∈ U, f x = f a

Tactic:
refine ⟨g⁻¹ • a, ?_, by simp +instances [f, orbitRel, Quotient.eq']⟩

Goal state after:
case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ g⁻¹ • a ∈ U
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : IsConj x y
⊢ x = y

Tactic:
exact H.eq_of_left_mem_center hx

Goal state after: