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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
contrapose! +distrib
  rw [Set.infinite_image2 hfs hft]
  grind only [Set.Infinite.nonempty]

Goal state after:
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
⊢ MulAction.IsPretransitive (Perm α) α

Tactic:
MulAction.isPretransitive_iff

Goal state after:
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
⊢ ∀ (x y : α), ∃ g, g • x = y
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
⊢ Pairwise fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)

Tactic:
intro i

Goal state after:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i : I
⊢ ∀ ⦃j : I⦄, i ≠ j → (fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)) i j
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

pp: case refine_2
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v

Tactic:
· have hk := congr_fun h k
    have hl := congr_fun h l
    have hm := congr_fun h m
    have hn := congr_fun h n
    grind [mul_one, one_mul, mul_apply]

Goal state after:
case refine_2
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n →
    mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hS : S.Nonempty
hT : T.Nonempty
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
by
  obtain ⟨s₁, h₁⟩ := hS
  obtain ⟨s₂, h₂⟩ := hT
  refine Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_
  rw [mem_iInter₂] at hx
  exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s * t ⊆ range ⇑m

Tactic:
by
  rintro _ ⟨a, ha, b, hb, rfl⟩
  obtain ⟨a, rfl⟩ := hs ha
  obtain ⟨b, rfl⟩ := ht hb
  exact ⟨a * b, map_mul ..⟩

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

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

Tactic:
← MulEquiv.coe_monoidHom_trans,

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

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

Tactic:
← MulEquiv.coe_monoidHom_trans,

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
by
  rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]

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
y : G
⊢ ∃ a, (f.codRestrict f.range ⋯) a = ⟨f y, ⋯⟩

Tactic:
exact ⟨y, rfl⟩

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

Goal state before:
pp: case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ K i.down

Tactic:
intro i

Goal state after:
case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
i : PLift ι
⊢ ∀ (y : PLift ι),
    ∃ z,
      (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ K i.down) i) ((fun i ↦ K i.down) z) ∧
        (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ K i.down) y) ((fun i ↦ K i.down) z)
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
⊢ map f f.ker = ⊥

Tactic:
by
  rw [map_eq_bot_iff]

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

Goal state before:
pp: b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n + 1 - (k + 1)) = shiftLeft' b m (n + 1) >>> (k + 1)

Tactic:
succ_sub_succ_eq_sub,

Goal state after:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = shiftLeft' b m (n + 1) >>> (k + 1)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b

Tactic:
simp [pair, h]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ (g⁻¹ * h * g ∈ s ↔ h ∈ s)

Tactic:
iff_comm

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ a • s ∩ b • t ⊆ 1 • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
by simp [hAB]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
⊢ ∀ (i : ι), h * g * h⁻¹ ∈ a i

Tactic:
intro i

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
i : ι
⊢ h * g * h⁻¹ ∈ a i
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case pos
α : 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:
simp [hl_empty]

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b

Tactic:
obtain ⟨i, a⟩ := a

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
i : ι
a : α i
⊢ (r ⟨i, a⟩.fst b.fst ∨ ∃ h, s b.fst (h ▸ ⟨i, a⟩.snd) b.snd) → Lex r s ⟨i, a⟩ b
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b

Tactic:
obtain ⟨i, a⟩ := a

Goal state after:
case mpr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
⊢ (r ⟨i, a⟩.fst b.fst ∨ ∃ h, s b.fst (h ▸ ⟨i, a⟩.snd) b.snd) → Lex r s ⟨i, a⟩ b
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]

Goal state after:
case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ ∈ {1, a✝}
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (↑m.succ % ↑n).toNat) = x ^ (k * (↑m % ↑n).toNat) * x ^ k

Tactic:
norm_cast

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (↑(m.succ % n)).toNat) = x ^ (k * (↑(m % n)).toNat) * x ^ k
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (↑(m + 1) * ↑(n - 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
norm_cast

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (↑((m + 1) * (n - 1) % n)).toNat) = x ^ (k * ((↑(m.succ % n)).toNat * (n - 1)))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ ∀ x ∈ s,
    ∀ (y : M),
      (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z

Tactic:
clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hs x hx, hx']

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by
      simp [List.mem_filter, Subtype.ext_iff, ht]

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
⊢ ∃ a, ofNat s a = ⟨x, hx⟩
Module: Mathlib.Data.List.Sublists

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

Tactic:
rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]
      simp [sublistsAux]

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

Goal state before:
pp: α : Type u_1
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ (↑l₁, ↑l₂).1 + (↑l₁, ↑l₂).2 = ↑l

Tactic:
exact Quot.sound (revzip_sublists _ _ _ h)

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : List α → β
r : List β
⊢ sublistsLenAux 0 l f r = f [] :: r

Tactic:
cases l <;> rfl

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) (a :: l₂✝)

Tactic:
refine IH.trans ?_

Goal state after:
case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) l₂✝ <+ sublistsLen (n + 1) (a :: l₂✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case inl
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1

pp: case inr
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1

Tactic:
· exact length_of_sublistsLen h

Goal state after:
case inr
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (Multiset.map id l.toFinset.val).sup

Tactic:
← List.toFinset_coe,

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (Multiset.map id (↑l).toFinset.val).sup
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∈ s.ssubsets ↔ t ⊂ s

Tactic:
by
  rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ s.sup f ⊓ a = s.sup fun i ↦ f i ⊓ a

Tactic:
_root_.inf_comm,

Goal state after:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a ⊓ s.sup f = s.sup fun i ↦ f i ⊓ a
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 α
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a ↦ count b (f a)

Tactic:
intro i

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 α),
    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.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ (a : ι), ∃ a_1 ∈ s, (if a ∈ s then f a else sSup ∅) ≤ f a_1

Tactic:
intro i

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
⊢ ∃ a ∈ s, (if i ∈ s then f i else sSup ∅) ≤ f a
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ a ∈ s, ∃ a_2, f a ≤ if a_2 ∈ s then f a_2 else sSup ∅

Tactic:
intro i

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
⊢ i ∈ s → ∃ a, f i ≤ if a ∈ s then f a else sSup ∅
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite

Tactic:
rw [finite_iUnion_iff (by aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise]))]
  simp

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f

Tactic:
refine ciSup_le fun i ↦ ?_

Goal state after:
case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
⊢ ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ (∀ {z : α}, z < y ↔ z ≤ x) ↔ ∀ {z : α}, z ≤ x ↔ z < y

Tactic:
iff_comm

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, ∀ (j : ι), j ≠ i → a j = b j

Tactic:
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_covBy h
  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)
⊢ (↑s).PairwiseDisjoint fun i ↦ map (Embedding.sigmaMk i) (t i)

Tactic:
intro i

Goal state after:
ι : 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
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Tactic:
· rw [sigmaLift, dif_neg h]
    refine iff_of_false (notMem_empty _) ?_
    rintro ⟨⟨⟩, ⟨⟩, _⟩
    exact h rfl

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

Goal state before:
pp: case inr.mp
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → i < a

pp: case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i

Tactic:
· rintro ⟨i, _, rfl⟩
    exact mod_lt i ha.bot_lt

Goal state after:
case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ i ∈ Finset.cons a s h, r i ((f ∘ ⇑g) a_2 i) ((f ∘ ⇑g) b i)

Tactic:
intro i

Goal state after:
case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
⊢ ∀ (s : Finset ι) (h : i ∉ s),
    (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s h, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
rw [← coe_subset, coe_Ico, coe_Icc]
  exact Set.Ico_subset_Icc_self

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (a : ι) (s_1 : Finset ι) (h : a ∉ s_1),
    (∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s_1, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
          ∃ g, ∀ ⦃a_3 b : ℕ⦄, a_3 ≤ b → ∀ i ∈ Finset.cons a s_1 h, r i ((f ∘ ⇑g) a_3 i) ((f ∘ ⇑g) b i)

Tactic:
intro i

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
⊢ ∀ (s_1 : Finset ι) (h : i ∉ s_1),
    (∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s_1, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
          ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s_1 h, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Tactic:
by
  rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (↑l) comm b = List.foldr f b l

Tactic:
by
  simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, List.attachWith, Function.comp_def]
  rw [← List.foldr_map]
  simp [List.map_pmap]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ (↑{a}).Pairwise (Commute on f)

Tactic:
norm_cast

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ {a}.Pairwise (Commute on f)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ ↑l, Disjoint b a

Tactic:
exact disjoint_list_sum_left

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

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ).Pairwise (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i))

Tactic:
intro i

Goal state after:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
⊢ i ∈ ↑univ → ∀ ⦃y : ι⦄, y ∈ ↑univ → i ≠ y → (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i)) i y
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
⊢ piSetoid (fun i ↦ (Quotient.mk'' (a✝ i)).out) a✝

Tactic:
intro i

Goal state after:
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
i : ι
⊢ (fun i ↦ (Quotient.mk'' (a✝ i)).out) i ≈ a✝ i
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ ⇑(sInf s) = sInf (@r α '' s)

Tactic:
ext
  simp only [sInf_image, iInf_apply, iInf_Prop_eq]
  rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Finset M
⊢ (∃ f, Function.support f ⊆ ↑s ∧ ∏ a ∈ s, a ^ f a = x) → x ∈ closure ↑s

Tactic:
rintro ⟨n, -, rfl⟩; exact prod_mem _ fun x hx ↦ pow_mem (subset_closure hx) _

Goal state after: