mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
⊢ Injective (Sum.elim Subtype.val Subtype.val)

Tactic:
rintro (⟨a, ha⟩ | ⟨a, ha⟩) (⟨b, hb⟩ | ⟨b, hb⟩)

Goal state after:
case inl.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inl ⟨b, hb⟩) →
    Sum.inl ⟨a, ha⟩ = Sum.inl ⟨b, hb⟩

case inl.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inl ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩

case inr.inl
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inl ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inl ⟨b, hb⟩

case inr.inr
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, ha⟩) = Sum.elim Subtype.val Subtype.val (Sum.inr ⟨b, hb⟩) →
    Sum.inr ⟨a, ha⟩ = Sum.inr ⟨b, hb⟩
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ * 1 ∈ {1, a✝}

Tactic:
rw [mul_one]; exact .inr rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
⊢ ∀ (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l✝ ++ [a]) → m ∈ a_2 :: (l✝ ++ [a])

Tactic:
_

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝ : α
⊢ (∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝) →
    ∀ (a m : α), m ∈ foldl (argAux r) (some a) (l✝ ++ [a✝]) → m ∈ a :: (l✝ ++ [a✝])
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝ : α
⊢ (∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝) →
    ∀ (a m : α), m ∈ foldl (argAux r) (some a) (l✝ ++ [a✝]) → m ∈ a :: (l✝ ++ [a✝])

Tactic:
_

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝¹ : α
a✝ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) (l✝ ++ [a✝¹]) → m ∈ a :: (l✝ ++ [a✝¹])
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝¹ : α
a✝ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) (l✝ ++ [a✝¹]) → m ∈ a :: (l✝ ++ [a✝¹])

Tactic:
_

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
⊢ ∀ (m : α), m ∈ foldl (argAux r) (some a✝) (l✝ ++ [a✝²]) → m ∈ a✝ :: (l✝ ++ [a✝²])
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l l' : List α
h : l ~ l'
⊢ l.maximum = l'.maximum

Tactic:
by
  induction h with grind [maximum_cons]

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

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (max a b) = f a ⊔ f b

Tactic:
sup_eq_right.2 h,

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f b = f a ⊔ f b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ f x < f y

Tactic:
calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ map (fun x ↦ x ++ []) l.sublists ++ (map (fun x ↦ x ++ [a]) l.sublists ++ []) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
map_id'' append_nil,

Goal state after:
α : Type u
l : List α
a : α
⊢ l.sublists ++ (map (fun x ↦ x ++ [a]) l.sublists ++ []) = l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]

Goal state after:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ List.map (fun x ↦ (x, ↑l₂ - x)) (powersetAux l₁) ~ List.map (fun x ↦ (x, ↑l₂ - x)) (powersetAux l₂)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ powersetCard 0 ⟦l⟧ = {0}

Tactic:
by simp [powersetCard_coe']

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
s : Multiset α
l : List α
⊢ powersetCard (n + 1) (a ::ₘ ⟦l⟧) = powersetCard (n + 1) ⟦l⟧ + map (cons a) (powersetCard n ⟦l⟧)

Tactic:
by simp [powersetCard_coe']

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

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
l : List α
⊢ s ∈ powersetCard n ⟦l⟧ ↔ s ≤ ⟦l⟧ ∧ s.card = n

Tactic:
by simp [powersetCard_coe']

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

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Finset α
⊢ s ∈ powersetCard n t ↔ s ⊆ t ∧ #s = n

Tactic:
by
  cases s; simp [powersetCard, val_le_iff.symm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ {x ∈ s.powerset | #x = n.succ} ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
← powersetCard_eq_filter

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ s ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
⊢ i ∉ s →
    (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
      count b ((insert i s).sup f) = (insert i s).sup fun a ↦ count b (f a)

Tactic:
_

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : i ∉ s
⊢ (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
    count b ((insert i s).sup f) = (insert i s).sup fun a ↦ count b (f a)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : IsEmpty ι
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅

Tactic:
have (i : ι) : IsEmpty (p i) := ⟨hp i⟩
    simp only [iSup_of_empty', ciSup_const]

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

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

Tactic:
refine le_antisymm (by simpa using fun _ ↦ biInf_le _) <|
    (le_iInf_iff.mpr fun i ↦ ?_).trans_eq (WithBot.coe_iInf _ (OrderBot.bddBelow _)).symm
  by_cases h : i ∈ s
  · simpa only [iInf_pos h] using by apply biInf_le _ h
  · simp [iInf_neg h]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : IsEmpty ι
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x
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:
_

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.Data.Set.Finite.Lattice

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

Tactic:
_

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

Goal state before:
pp: case inl
α : Type u_5
inst✝ : CompleteLinearOrder α
a : α
hne : a ≠ ⊥
hfin : ∅.Finite
hmem : a ∉ ∅
⊢ sSup ∅ ≠ a

pp: case inr
α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
hnonempty : s.Nonempty
⊢ sSup s ≠ a

Tactic:
· simp [eq_comm, hne]

Goal state after:
case inr
α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
hnonempty : s.Nonempty
⊢ sSup s ≠ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case neg.inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : IsEmpty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

case neg.inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : Nonempty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b

Tactic:
by
  simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk i '' g i ⁻¹' s = Sigma.map f g ⁻¹' Sigma.mk (f i) '' s

Tactic:
by
  refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_
  rintro ⟨j, x⟩ ⟨y, hys, hxy⟩
  simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)

Tactic:
rw [gc.l_csSup hne hbdd, sSup_image']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : IsEmpty ι
⊢ e (⨆ i, f i) = ⨆ i, e (f i)

case inr
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h✝ : Nonempty ι
⊢ e (⨆ i, f i) = ⨆ i, e (f i)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂

Tactic:
simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
by
  rw [wcovBy_iff_covBy_or_le_and_le] at h
  obtain h | h := h
  · exact exists_forall_antisymmRel_of_covBy h
  · inhabit ι
    exact ⟨default, fun j hj ↦ ⟨h.left j, h.right j⟩⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
h : a ⋖ b
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ i, ∀ (j : ι), j ≠ i → a j = b j

Tactic:
exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⩿ b
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ i, ∀ (j : ι), j ≠ i → a j = b j

Tactic:
exact ⟨i, fun j hj ↦ AntisymmRel.eq (hi _ hj)⟩

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 : ι
⊢ i ∈ ↑s → ∀ ⦃y : ι⦄, y ∈ ↑s → i ≠ y → (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i y

Tactic:
_

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝ : i ∈ ↑s
⊢ ∀ ⦃y : ι⦄, y ∈ ↑s → i ≠ y → (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i y
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 : ι
⊢ j ∈ ↑s → i ≠ j → (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i j

Tactic:
_

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
⊢ i ≠ j → (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i j
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c

Tactic:
by
  rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
hIoo : h₀_finset_Ioo = h₁_finset_Ioo
⊢ { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := ⋯, finset_mem_Ico := ⋯, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }

Tactic:
hIoc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
hIoo : h₀_finset_Ioo = h₁_finset_Ioo
⊢ { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := ⋯, finset_mem_Ico := ⋯, finset_mem_Ioc := ⋯, finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
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) ↑((Ico n (n + a + 1)).erase n)

Tactic:
Ico_succ_right_eq_insert_Ico (by lia)

Goal state after:
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)
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
by_cases he : hbad.toFinset.Nonempty

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad

case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : ¬hbad.toFinset.Nonempty
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → n ∉ bad
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case e'_2
n a : ℕ
⊢ Multiset.map (fun x ↦ x % a) (Multiset.Ico n (n + a)) = (image (fun x ↦ x % a) (Finset.Ico n (n + a))).val

Tactic:
refine ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm

Goal state after:
case e'_2
n a : ℕ
⊢ ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
⊢ P x✝ → x✝ < k * x✝

Tactic:
_

Goal state after:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ < k * x✝
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite

Tactic:
refine ⟨fun h ↦ ⟨h.to_wellFoundedLT, fun s ↦ h.finite_of_isAntichain⟩,
    fun ⟨hwf, hc⟩ ↦ ⟨fun f ↦ ?_⟩⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
obtain ⟨z, hxz, hz⟩ :=
      (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 <| hxy.lt_of_not_ge hxy'
    have z_card := calc
      #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right hz.1.2
      _          < #(Icc x y) := this
    have h₁ := transGen_wcovBy_of_le hz.1.1
    have h₂ : z ⩿ y :=
      ⟨hz.1.2.le, fun c hzc hcy ↦ hzc.not_ge <| hz.2 ⟨hz.1.1.trans hzc.le, hcy⟩ hzc.le⟩
    exact .tail h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
a : M
inst✝ : Mul M
h : IsMulCentral a
b c : M
⊢ a * (b * c) = b * (a * c)

Tactic:
by
  simp only [(h.comm _).eq, h.right_assoc]

Goal state after: