mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
⊢ ∀ (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)

Tactic:
n

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Finset β
a : α
⊢ {a} ×ˢ t = map { toFun := Prod.mk a, inj' := ⋯ } t

Tactic:
by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
b : β
⊢ s ×ˢ {b} = map { toFun := fun i ↦ (i, b), inj' := ⋯ } s

Tactic:
by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ a = b

Tactic:
SemiconjBy,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : ↑c * a = b * ↑c
⊢ a = b
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (f ↑c) (f a) (f b)

Tactic:
SemiconjBy,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ f ↑c * f a = f b * f ↑c
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : SemiconjBy (↑c) 1 a
⊢ a = 1

Tactic:
SemiconjBy,

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : ↑c * 1 = a * ↑c
⊢ a = 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
by
  inhabit ι
  refine Subset.antisymm (image_iInter_subset s f) fun y hy => ?_
  simp only [mem_iInter, mem_image] at hy
  choose x hx hy using hy
  refine ⟨x default, mem_iInter.2 fun i => ?_, hy _⟩
  suffices x default = x i by
    rw [this]
    apply hx
  replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
  apply h (hx _) (hx _)
  simp only [hy]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x✝ : Subtype p
x : α
h : p x
⊢ ⟨x, h⟩ ∈ univ ↔ ⟨x, h⟩ ∈ ⋃ x, ⋃ (h : p x), {⟨x, h⟩}

Tactic:
by simp [h]

Goal state after:
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)⁻¹
| (fun x ↦ x⁻¹) '' g '' s

Tactic:
image_image,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
| (fun x ↦ (g x)⁻¹) '' s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x⁻¹) '' (fun x ↦ a⁻¹ * x) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ x * a) '' (fun x ↦ x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty

Tactic:
image_image,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ (a⁻¹ * x)⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔ ((fun x ↦ x⁻¹ * a) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x⁻¹) '' (fun x ↦ x * a⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ a * x) '' (fun x ↦ x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty

Tactic:
image_image,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ (x * a⁻¹)⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔ ((fun x ↦ a * x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set β
n : ℕ
⊢ (⇑f ⁻¹' s) ^ (n + 1) ⊆ ⇑f ⁻¹' s ^ (n + 1)

Tactic:
simpa [pow_succ] using Subset.trans (mul_subset_mul_right
    (preimage_pow_subset f s n)) (preimage_mul_preimage_subset f)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑(map K.subtype (H.subgroupOf K)) = ↑(H ⊓ K)

Tactic:
refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm

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

Goal state before:
pp: n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + (s + s)

Tactic:
rw [← Nat.add_assoc]; apply sqrt_le_add

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

Goal state before:
pp: m n : ℕ
⊢ m + n ≤ pair m n

Tactic:
simp only [pair, Nat.add_assoc]
  split_ifs
  · have := le_mul_self n
    lia
  · exact Nat.le_add_left _ _

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:
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 : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
⊢ ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H

Tactic:
n

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
n : N
⊢ f n ∈ H ↔ f (x * n * x⁻¹) ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

Tactic:
by
  rw [conjugatesOfSet, Set.mem_iUnion₂]
  simp only [conjugatesOf, isConj_iff, Set.mem_ofPred_eq, exists_prop]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ (f.prodMap g).ker = f.ker.prod g.ker

Tactic:
by
  rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]

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

Goal state before:
pp: case cons_cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ a * l₁✝.prod ≤ a * l₂✝.prod

Tactic:
grw [ih' h₁.2]

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

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid

Tactic:
change x * y * x⁻¹ * y⁻¹ ∈ H₂
    apply H₂.mul_mem _ (H₂.inv_mem hy)
    apply hH₂.conj_mem _ hy

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

Goal state before:
pp: case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)

Goal state after:
case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
⊢ f (a * l.prod) ≤ f a * (map f l).prod
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b

Tactic:
by
  obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
  · exact Lex.left _ _ (hr _ _ hij)
  · exact Lex.right _ (hs _ _ _ hab)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : S = ⊥
⊢ card ↥S ≤ 1

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (map inl s + map inr t).card = s.card + t.card

Tactic:
card_add,

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (map inl s).card + (map inr t).card = s.card + t.card
Module: Mathlib.Data.Multiset.Lattice

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

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
Module: Mathlib.Data.Multiset.Lattice

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

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

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ ∀ (x_1 : Subtype (Membership.mem s)),
    x_1 ∈ (Multiset.pmap (fun y hy ↦ ⟨y, hy⟩) (Multiset.filter (fun x ↦ x ∈ s) (Multiset.range (↑x).succ)) ⋯).toFinset

Tactic:
simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ]

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

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

Tactic:
simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u = s.disjSum t
⊢ u.toLeft = s ∧ u.toRight = t

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n) ∧ m ∈ s

Tactic:
simp only [h.2, and_true]

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n)
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
⊢ ∀ (a : ℕ), a < ↑(succ (ofNat s n)) ∧ a ∈ s ↔ a = ↑(ofNat s n) ∨ a < ↑(ofNat s n) ∧ a ∈ s

Tactic:
exact fun m =>
        ⟨fun h => by
          simp only [h.2, and_true]
          exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),
         fun h =>
          h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h =>
            ⟨h.1.trans (lt_succ_self _), h.2⟩⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑(insert a s)) (max a (s.max' H))

Tactic:
coe_insert

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (insert a ↑s) (max a (s.max' H))
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑(insert a s)) (min a (s.min' H))

Tactic:
coe_insert

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (insert a ↑s) (min a (s.min' H))
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_7
R : Type u_8
inst✝ : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
y : α
hys : y ∈ s.toFinset
hy : ∀ x' ∈ s.toFinset, f x' ≤ f y
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
exact ⟨y, mem_toFinset.mp hys, fun _ hz ↦ hy _ (mem_toFinset.mpr hz)⟩

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

Goal state before:
pp: case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : (⋃ n, f n).Pairwise r
⊢ ∀ (n : κ), (f n).Pairwise r

Tactic:
n

Goal state after:
case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : (⋃ n, f n).Pairwise r
n : κ
⊢ (f n).Pairwise r
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length) ++ []) ~ tl.sublists'

Tactic:
append_nil,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length) ~ tl.sublists'
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
⊢ card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))

Tactic:
simp only [card_fin, card_option, card_ulift]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
⊢ (s.sup fun b ↦ {f b}) = image f s

Tactic:
ext a

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ s.sup fun b ↦ {f b}) ↔ a ∈ image f s
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
he i hi,

Goal state after:
case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ ∅
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ (fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩) ((fun a ↦ untopD ⊤ (map Subtype.val a)) ↑⟨a, h⟩) = ↑⟨a, h⟩

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a b✝ : WithTop { a // a ≠ ⊤ }
b : α
h : b ≠ ⊤
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        ⊤ ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ↑⟨b, h⟩ ↔
    ⊤ ≤ ↑⟨b, h⟩

Tactic:
by simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
rw [ciSup_of_not_bddAbove hg, ciSup_of_not_bddAbove <| mt bbdAbove_range_right_of_sup hg]

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ sSup ∅ ≤ max (⨆ x, f x) (sSup ∅)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : β
ha : f a < c
hb : c < f b
⊢ False

Tactic:
obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α
f : α ↪o β
hab : a ⩿ b
h : (range ⇑f).OrdConnected
c : α
ha : f a < f c
hb : f c < f b
⊢ False
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Finset α
f : α → Set β
x : α
h : x ∈ s
⊢ f x ⊆ ⋃ (_ : x ∈ s), f x

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b

Tactic:
by
  rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
· refine Or.inl (subset_antisymm ?_ hst)
    rwa [← sdiff_singleton_eq_self h, sdiff_singleton_subset_iff]

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h
    · exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩
    · exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩
  · rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_wcovBy_mk_iff_left.2 h
    · exact mk_wcovBy_mk_iff_right.2 h

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
hf : Bijective f
⊢ image f s = t ↔ s = t.preimage f ⋯

Tactic:
by
  rw [← image_inj hf.injective, t.image_preimage_of_bijective hf]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: 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 : α
hyt : f y ∈ t
⊢ y ≤ x → x ≤ y

Tactic:
exact h.le_of_le hyt

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' a (b + 1 - a)), nodup := ⋯ } ↔ a ≤ x ∧ x ≤ b

Tactic:
by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; lia

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' a (b - a)), nodup := ⋯ } ↔ a ≤ x ∧ x < b

Tactic:
by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; lia

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' (a + 1) (b - a)), nodup := ⋯ } ↔ a < x ∧ x ≤ b

Tactic:
by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; lia

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

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ x ∈ { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := ⋯ } ↔ a < x ∧ x < b

Tactic:
by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; lia

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

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

Tactic:
rw [add_mod_right] at hkl

Goal state after:
case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n + a = l
Module: Mathlib.Order.Interval.Finset.Nat

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

Tactic:
rw [add_mod_right] at hkl

Goal state after:
case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n + a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (↑(Icc a b)).Nonempty ↔ a ≤ b

Tactic:
coe_Icc,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Set.Icc a b).Nonempty ↔ a ≤ b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ↑(Icc a b) = ∅ ↔ ¬a ≤ b

Tactic:
coe_Icc,

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Icc a b = ∅ ↔ ¬a ≤ b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ ↑(Icc a b₁) ⊆ ↑(Ico a b₂)

Tactic:
coe_Icc,

Goal state after:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ ↑(Ico a b₂)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b ⊆ Set.Icc a b

Tactic:
exact Set.Ico_subset_Icc_self

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ ↑(Icc a₁ b₁) ⊆ ↑(Icc a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
coe_Icc,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ ↑(Icc a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ ↑(Icc a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
coe_Icc,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ ↑(Icc a₁ b₁) ⊆ ↑(Ioo a₂ b₂) ↔ a₂ < a₁ ∧ b₁ < b₂

Tactic:
coe_Icc,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ ↑(Ioo a₂ b₂) ↔ a₂ < a₁ ∧ b₁ < b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ ↑(Icc a₁ b₁) ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ < b₂

Tactic:
coe_Icc,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ ↑(Ico a₂ b₂) ↔ a₂ ≤ a₁ ∧ b₁ < b₂