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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s

Tactic:
by
  simp +contextual [mem_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) → i ∈ t

Tactic:
by
  simp +contextual [mem_image]

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
s : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
t : (i : ↥s) → Set (π ↑i)
⊢ s.restrict ⁻¹' Set.univ.pi t = (↑s).pi fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ

Tactic:
ext
  simp_all

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
⊢ image (fun f ↦ f a) (piFinset t) = t a

Tactic:
refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
x : δ a
h : x ∈ t a
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅

Tactic:
have : Nonempty α := ⟨a⟩

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
this : Nonempty α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n r : ℕ
hr : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
by
  induction hr using decreasingInduction with
  | self => rfl
  | of_succ k hk ih => exact (choose_le_succ_of_lt_half_left hk).trans ih

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ (s ×ˢ t).Finite

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (s ×ˢ t).Finite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
⊢ (image2 f s t).Finite

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (image2 f s t).Finite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
ht : t.Infinite
a : α
ha : a ∈ s
⊢ (image2 f s t).Infinite

Tactic:
· exact ht.image2_right ha (hft _ ha)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ y ∈ S, ⋂ x, ⋂ (_ : (y, t) = x), x.1 ×ˢ x.2 = ⋂ s ∈ S, s ×ˢ t

Tactic:
iInter_iInter_eq_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ y ∈ T, ⋂ x, ⋂ (_ : (s, y) = x), x.1 ×ˢ x.2 = ⋂ t ∈ T, s ×ˢ t

Tactic:
iInter_iInter_eq_right

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
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, image2 f (s i j) t

Tactic:
image2_iUnion_left

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N✝ : Type u_5
inst✝² : Group N✝
P : Type u_6
inst✝¹ : Group P
N : Type u_7
inst✝ : Group N
f : G →* N
H : Subgroup N
a : G
ha : a ∈ ⇑f ⁻¹' ↑H
⊢ f a⁻¹ ∈ H

Tactic:
rw [f.map_inv]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N✝ : Type u_5
inst✝² : Group N✝
P : Type u_6
inst✝¹ : Group P
N : Type u_7
inst✝ : Group N
f : G →* N
H : Subgroup N
a : G
ha : a ∈ ⇑f ⁻¹' ↑H
⊢ (f a)⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i

Tactic:
by
  -- Could use the `Submonoid` version, but we limit the imports here
  refine ⟨?_, fun ⟨i, hi', hi⟩ ↦ ?_⟩
  · suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
      simpa only [closure_iUnion, closure_eq (K _)] using this
    refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
    · simp
    · exact ⟨i, hp, (K i).one_mem⟩
    · rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩
      rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
      exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩
    · rintro _ _ ⟨i, hi', hi⟩
      exact ⟨i, hi', inv_mem hi⟩
  · apply le_iSup (fun i ↦ ⨆ (_ : p i), K i) i
    simp [hi, hi']

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : f x = f y
⊢ x = y

Tactic:
by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
simp only [bodd_eq_one_and_ne_zero] at this

Goal state after:
m : ℕ
b : Bool
n : ℕ
this : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)
⊢ (bit b n).testBit m.succ = n.testBit m
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ bit a m < 2 * n

Tactic:
cases a <;> dsimp [bit]

Goal state after:
case false
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m < 2 * n

case true
m n : ℕ
b : Bool
h : m < n
⊢ 2 * m + 1 < 2 * n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = (⋃ n, s n) ×ˢ ⋃ n, t n

Tactic:
by
  rw [← Set.iUnion_prod]
  exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (f x)

Tactic:
Subgroup.zpowers_eq_closure,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.closure {x}) = Subgroup.zpowers (f x)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.closure {x}) = Subgroup.zpowers (f x)

Tactic:
Subgroup.zpowers_eq_closure,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.closure {x}) = Subgroup.closure {f x}
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ a ∈ N

Tactic:
refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N

case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a ^ (n.succ + 1) = a

Tactic:
by rw [pow_succ, ih, h.eq]

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

Goal state before:
pp: case inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
⊢ motive x

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ motive x
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
h : argmax f tl = none
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
rw [h] at hm

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) none = some m
h : argmax f tl = none
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
val✝ : α
h : argmax f tl = some val✝
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
rw [h] at hm

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (some val✝) = some m
h : argmax f tl = some val✝
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit false n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit false n.div2

Tactic:
simp [bit_val, encodeSum]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case true
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit true n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit true n.div2

Tactic:
simp [bit_val, encodeSum]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : l.maximum = ↑y
⊢ l.max?.getD d = WithBot.unbotD d ↑y

Tactic:
rw [List.maximum_eq_coe_iff] at hy

Goal state after:
case coe
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = WithBot.unbotD d ↑y
Module: Mathlib.Data.List.MinMax

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

Tactic:
contradiction

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

Goal state before:
pp: case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ max x (foldr max ⊥ l)

Tactic:
exact le_max_of_le_left h

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ x :: l
⊢ a ≤ max x (foldr max b l)

Tactic:
exact le_max_of_le_left h

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a x b : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max b l

Tactic:
induction l with
  | nil => exact absurd hx List.not_mem_nil
  | cons y l IH =>
    simp only [List.foldr]
    obtain rfl | hl := mem_cons.mp hx
    · exact le_max_of_le_left h
    · exact le_max_of_le_right (IH hl)

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.reverse = l.reverse.revzip

Tactic:
by
  rw [← zip_unzip (revzip l).reverse]
  simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]

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

Goal state before:
pp: case H
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
⊢ motive s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Goal state after:
case H.inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
ih : ∀ s ∈ ∅, motive (∅.erase s)
⊢ motive ∅

case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
⊢ motive s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr.cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

Tactic:
exact Or.inl h

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

Goal state before:
pp: α : Type u
a : α
r : List (List α)
⊢ sublistsAux a [] = flatMap (fun l ↦ [l, a :: l]) []

Tactic:
by simp [sublistsAux]

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:
have := hs.to_subtype

Goal state after:
α : Type u
β : Type v
s : Set α
hs : s.Finite
F : (i : α) → i ∈ s → β
this : Finite ↑s
⊢ {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ (range fun h ↦ f h) = ∅

Tactic:
rwa [range_eq_empty_iff, isEmpty_Prop]

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite
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 : False
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
contradiction

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:
simpa using fun _ ↦ biInf_le _

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i
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
inst✝ : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
have := hs.to_subtype

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 → α
this : Finite ↑s
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
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:
simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ Ioi a = {⊤}

Tactic:
← Ioc_top,

Goal state after:
case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ Ioc a ⊤ = {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ a < ↑(f i)

Tactic:
simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
j : ι
hj : a j < b j
this : Nonempty ι
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
obtain rfl : i = j := by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj

Goal state after:
case mp
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⋖ b
this : Nonempty ι
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
hj : a i < b i
⊢ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (s.sigma t).sup f = s.sup fun i ↦ (t i).sup fun b ↦ f ⟨i, b⟩

Tactic:
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
  exact
    ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
      le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

Tactic:
split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_2
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y

Tactic:
obtain ⟨z, hzy, hz⟩ := h hy

Goal state after:
case refine_2
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
z : α
hzy : z ≤ y
hz : Q z
⊢ x ≤ y
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
hac : a ≤ c
⊢ filter (fun x ↦ c ≤ x) (Ico a b) = Ico c b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a✝ : α
hab : a ≤ a✝ ∧ a✝ < b
hbc : c ≤ a✝ ∧ a✝ < d
⊢ False

Tactic:
exact hab.2.not_ge (h.trans hbc.1)

Goal state after: