mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1.refine_3
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
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ (x y : G),
    x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) →
      y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → (∃ i, p i ∧ x ∈ K i) → (∃ i, p i ∧ y ∈ K i) → ∃ i, p i ∧ x * y ∈ K i

Tactic:
rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩

Goal state after:
case refine_1.refine_3
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
hx : x✝ ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
hy✝ : y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
⊢ ∃ i, p i ∧ x * y ∈ K i
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ map f (H ⊔ K) = ⊤

Tactic:
codisjoint_iff.mp h,

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ map f ⊤ = ⊤
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

Tactic:
SetLike.ext'_iff

Goal state after:
ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ ↑(pi Set.univ S) = ↑⊥ ↔ ∀ (i : ι), ↑(S i) = ↑⊥
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]

Goal state after:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + s + s
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: ⊢ unpair 0 = 0

Tactic:
by
  rw [unpair]
  simp

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

Tactic:
SetLike.ext'_iff

Goal state after:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ ↑(pi univ H) = ↑⊥ ↔ ∀ (i : η), ↑(H i) = ↑⊥
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ g ∈ normalizer s → g ∈ normalizer ↑(closure s)

Tactic:
hg

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ normalizer s
⊢ g ∈ normalizer ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ closure (⇑(MulAut.conj g) '' s) = closure s

Tactic:
hg

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ closure s = closure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ (N.subgroupOf H).Normal

Tactic:
by
  rw [normal_subgroupOf_iff_le_normalizer_inf]
  exact (le_inf hLE H.le_normalizer).trans inf_normalizer_le_normalizer_inf

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ Subtype.val '' Sum.inl ⁻¹' ⇑(sumSet h) ⁻¹' r = r ∩ s

Tactic:
simp [Set.ext_iff]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ Subtype.val '' Sum.inr ⁻¹' ⇑(sumSet h) ⁻¹' r = r ∩ t

Tactic:
simp [Set.ext_iff]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ range ⇑(sumSet h) = s ∪ t

Tactic:
simp [Set.ext_iff]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
r : Set α
⊢ Subtype.val '' Sigma.mk i ⁻¹' ⇑(sigmaSet h) ⁻¹' r = r ∩ s i

Tactic:
simp [Set.ext_iff]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ range ⇑(sigmaSet h) = ⋃ i, s i

Tactic:
simp [Set.ext_iff]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ motive x

Tactic:
by
  have : x ∈ closure s := by simp [hs]
  induction this using closure_induction_right with
  | one => exact one
  | mul_right x _ y hy ih => exact mul_right x y hy ih

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k ≤ 0
⊢ False

Tactic:
le_zero_eq

Goal state after:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k = 0
⊢ False
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #(insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s}))

Tactic:
← h₂

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #({x ∈ range ↑(succ (ofNat s n)) | x ∈ s})
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f : TopHom β γ
g : TopHom α β
⊢ (⇑f ∘ ⇑g) ⊤ = ⊤

Tactic:
comp_apply,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f : TopHom β γ
g : TopHom α β
⊢ f (g ⊤) = ⊤
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⊔ b) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b

Tactic:
comp_apply,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f : SupHom β γ
g : SupHom α β
a b : α
⊢ f (g (a ⊔ b)) = (⇑f ∘ ⇑g) a ⊔ (⇑f ∘ ⇑g) b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).max

Tactic:
rw [max_eq_sup_withBot, sup_image]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = s.sup (WithBot.some ∘ ⇑ofDual)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).max

Tactic:
rw [max_eq_sup_withBot, sup_image]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = s.sup (WithBot.some ∘ ⇑toDual)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ s

Tactic:
rw [← mem_coe]
  exact ((isGLB_iff_isLeast i s hs).mp his).1

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ (∅.sup fun x ↦ ⊥) = ⊥

pp: case inr
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ (s.sup fun x ↦ ⊥) = ⊥

Tactic:
· exact sup_empty

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ (s.sup fun x ↦ ⊥) = ⊥
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
o : Option α
⊢ o.toFinset.card = o.elim 0 1

Tactic:
by cases o <;> rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
⊢ ∀ i_1 ∈ t, Disjoint (f (i, i')) (f (j, i_1))

Tactic:
j'

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
⊢ j' ∈ t → Disjoint (f (i, i')) (f (j, j'))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
⊢ ∀ i_1 ∈ s, Disjoint (f (i', i)) (f (i_1, j))

Tactic:
j'

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
⊢ j' ∈ s → Disjoint (f (i', i)) (f (j', j))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

Tactic:
rcases le_total (f a) (s.sup f) with (ha | ha)

Goal state after:
case insert.inr.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : f a ≤ s.sup f
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
⊢ ↑((s.sup (WithBot.some ∘ f)).unbot ⋯) = s.sup (WithBot.some ∘ f)

Tactic:
WithBot.coe_unbot

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
⊢ s.sup (WithBot.some ∘ f) = s.sup (WithBot.some ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

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

Tactic:
by
  rw [inf_comm, sup'_inf_distrib_left]; simp_rw [inf_comm]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
cases le_total (f b) (f c) with
    | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
    | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Tactic:
· assumption

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

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x < a

Tactic:
refine h.trans_le' (le_csSup ?_ ?_)

Goal state after:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i ↦ ⨆ (_ : i ∈ s), f i)

case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
s : Set α
⊢ (s \ ⋃ x, Ioo ↑x.1 ↑x.2).Finite

Tactic:
by
  simpa only [iUnion, iSup_prod, iSup_subtype] using s.finite_sdiff_iUnion_Ioo

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down

Tactic:
rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]

Goal state after:
α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ x, s (Equiv.plift x) = ⨆ i, s i.down
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi a = {b}
⊢ IsTop b ∧ a ⋖ b

Tactic:
simp_rw [Set.ext_iff, mem_Ioi, mem_singleton_iff] at h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ∀ (x : α), a < x ↔ x = b
⊢ IsTop b ∧ a ⋖ b
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x ↦ x ∈ f '' s) (f a)
y : α
hys : (fun x ↦ x ∈ s) y
⊢ y ≤ a → a ≤ y

Tactic:
← hf ha hys,

Goal state after:
α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x ↦ x ∈ f '' s) (f a)
y : α
hys : (fun x ↦ x ∈ s) y
⊢ y ≤ a → f a ≤ f y
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ (Finset.Icc a b).val = 0 ↔ ¬a ≤ b

Tactic:
Finset.val_eq_zero,

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc a b = 0 ↔ ¬a ≤ b

Tactic:
by
  rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ (Finset.Ico a b).val = 0 ↔ ¬a < b

Tactic:
Finset.val_eq_zero,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Finset.Ico a b = ∅ ↔ ¬a < b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ (Finset.Ioc a b).val = 0 ↔ ¬a < b

Tactic:
Finset.val_eq_zero,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Finset.Ioc a b = ∅ ↔ ¬a < b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ (Finset.Ioo a b).val = 0 ↔ ¬a < b

Tactic:
Finset.val_eq_zero,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ Finset.Ioo a b = ∅ ↔ ¬a < b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1

Tactic:
· assumption

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

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = Nat.find hp

Tactic:
rw [Nat.sInf_def hp] at hn

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
hn : n ≤ Nat.find hp
⊢ Nat.find ⋯ + n = Nat.find hp
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Icc (f a) (f b)).preimage ⇑f ⋯ ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ.add x)))

Tactic:
exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

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

Goal state before:
pp: case mpr
a b x : ℕ
h : a ≤ x ∧ x < a + b
⊢ ∃ a_1 < b, a + a_1 = x

Tactic:
exact ⟨x - a, by lia⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
y : α
inst✝ : LocallyFiniteOrderBot α
⊢ Finite { x // x < y }

Tactic:
simpa only [coe_Iio] using! (Finset.Iio y).finite_toSet

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : TransGen CovBy a b ≤ (TransGen LT.lt on f) a b
⊢ f a < f b

Tactic:
← lt_iff_transGen_covBy,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : (a < b) ≤ (TransGen LT.lt on f) a b
⊢ f a < f b
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e✝ x ∈ Set.center N

Tactic:
change e x ∈ Set.center N

Goal state after:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e x ∈ Set.center N
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), Commute (op x) (op a)) ∧
      (∀ (a a_1 : M), op x * (op a * op a_1) = op x * op a * op a_1) ∧
        ∀ (a a_1 : M), op a * op a_1 * op x = op a * (op a_1 * op x)) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)

Tactic:
← op_mul,

Goal state after:
M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), Commute (op x) (op a)) ∧
      (∀ (a a_1 : M), op (a_1 * a * x) = op (a_1 * (a * x))) ∧ ∀ (a a_1 : M), op (x * (a_1 * a)) = op (x * a_1 * a)) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case f
G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
s : G
hs : s ∈ S
x : G
⊢ s⁻¹ * x ∈ ↑N ↔ x * s⁻¹ ∈ ↑N

Tactic:
exact (mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm

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

Goal state before:
pp: case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x x'✝ x' : G
hx✝ : x'✝ ∈ closure (↑H * ↑N)
hy✝ : x' ∈ closure (↑H * ↑N)
hx : x'✝ ∈ ↑H * ↑N
hx' : x' ∈ ↑H * ↑N
⊢ x'✝ * x' ∈ ↑H * ↑N

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := hx
    obtain ⟨x', hx', y', hy', rfl⟩ := hx'
    refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
    · exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy
    · simp only [mul_assoc, mul_inv_cancel_left]

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

Goal state before:
pp: case mk
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
a✝ : List α
comm : {x | x ∈ Quot.mk (⇑(List.isSetoid α)) a✝ + t}.Pairwise Commute
⊢ (Quot.mk (⇑(List.isSetoid α)) a✝ + t).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝) ⋯ * t.noncommProd ⋯

Tactic:
rcases t with ⟨⟩

Goal state after:
case mk.mk
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
a✝¹ a✝ : List α
comm : {x | x ∈ Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝}.Pairwise Commute
⊢ (Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝¹) ⋯ * noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝) ⋯
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
⊢ g ∈ normalizer ↑H ⊓ normalizer ↑K → g ∈ normalizer ↑(H ⊔ K)

Tactic:
hg

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : g ∈ normalizer ↑H ⊓ normalizer ↑K
⊢ g ∈ normalizer ↑(H ⊔ K)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
⊢ g ∈ ⨅ i, normalizer ↑(H i) → g ∈ normalizer ↑(⨆ i, H i)

Tactic:
hg

Goal state after:
G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : g ∈ ⨅ i, normalizer ↑(H i)
⊢ g ∈ normalizer ↑(⨆ i, H i)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : ∀ (i : ι), map (↑(MulAut.conj g)) (H i) = H i
⊢ ⨆ i, map (↑(MulAut.conj g)) (H i) = ⨆ i, H i

Tactic:
hg

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ (List.map f s.toList).prod = s.prod f

Tactic:
rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)

Tactic:
simpa only [disjoint_comm] using disjoint_finsetSum_left

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x✝ : M
s : Set M
x : M
hx : x ∈ s
⊢ ↑{x} ⊆ s ∧ Function.support (Pi.single x 1) ⊆ ↑{x} ∧ ∏ a ∈ {x}, a ^ Pi.single x 1 a = x

Tactic:
simp [hx, Pi.single_apply]

Goal state after: