mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
h : cons x₀ x = cons y₀ y
i : Fin n
⊢ x i = y i

Tactic:
by simpa using congr_fun h (Fin.succ i)

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (last n).predAbove i.castSucc = i

Tactic:
predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)),

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ i.castSucc.castPred ⋯ = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ b = (b.pred ⋯).succ

Tactic:
succ_pred

Goal state after:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ b = b
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)

Tactic:
rw [seqOfForallFinsetExistsAux]

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (Classical.choose ⋯)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc < (i.pred ⋯).succ

Tactic:
succ_pred

Goal state after:
case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc < i
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Injective f ↔ Bijective f

Tactic:
simp [Bijective, injective_iff_surjective]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Injective f ↔ Bijective f

Tactic:
by
  simp [Bijective, injective_iff_surjective]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Surjective f ↔ Bijective f

Tactic:
simp [Bijective, injective_iff_surjective]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Surjective f ↔ Bijective f

Tactic:
by
  simp [Bijective, injective_iff_surjective]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
i : Fin (n + 1)
⊢ cons x xs i = (append (cons x elim0) xs ∘ Fin.cast ⋯) i

Tactic:
simp [append_left_eq_cons]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
⊢ g ∘ snoc q y = snoc (g ∘ q) (g y)

Tactic:
ext j
  by_cases h : j.val < n
  · simp [h, snoc, castSucc_castLT]
  · rw [eq_last_of_not_lt h]
    simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ Injective x

pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ ¬x₀ ∈ Set.range x

Tactic:
· simpa [Function.comp] using h.comp (Fin.castSucc_injective _)

Goal state after:
case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ ¬x₀ ∈ Set.range x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j ↦ q (i.succAbove j)

Tactic:
simp [Pi.le_def, forall_iff_succAbove i]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j ↦ q (i.succAbove j)) ≤ p

Tactic:
simp [Pi.le_def, forall_iff_succAbove i]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
⊢ ∃ u, ↑u ⊆ s ∧ InjOn f ↑u ∧ image f u = t

Tactic:
obtain ⟨u, hus, hf, himg⟩ := hfs.exists_subset_injOn_image_eq
  refine ⟨(Finite.of_finite_image (by simp [himg]) hf).toFinset, by simpa, by simpa, ?_⟩
  simpa [← Finset.coe_inj]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedLT ↔ l.SortedGT

Tactic:
grind [hf.lt_iff_gt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedGT ↔ l.SortedLT

Tactic:
grind [hf.lt_iff_gt]

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

Goal state before:
pp: case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m (m + 1)
⊢ IsChain r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m (m + 1)

Tactic:
rw [hn, forall_lt_succ_right]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩

Tactic:
by
  simpa using getElem_eq_getElem_rotate _ _ _ _

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
i j : ℕ
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
by
  rcases eq_or_ne l [] with rfl | hn
  · simp
  · simp only [hn, or_false]
    refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
    rw [← rotate_mod, h, rotate_mod]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
h : ∀ (x : M), x ∈ s → x = 1
⊢ s.prod = 1

Tactic:
by
  induction s using Quotient.inductionOn; simp [List.prod_eq_one h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : α
⊢ b ∈ t.disjiUnion (fun a ↦ {x ∈ s | f x = a}) ⋯ ↔ b ∈ {c ∈ s | f c ∈ t}

Tactic:
by simpa using and_comm

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.cyclicPermutations.length
⊢ l.cyclicPermutations[n] = l.rotate n

Tactic:
by
  cases l with
  | nil => simp
  | cons a l =>
    simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
      getElem_inits]
    rw [rotate_eq_drop_append_take (by simpa using h.le)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s✝ : Finset α
t : α → Finset β
f : β → γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : image f (s.biUnion t) = s.biUnion fun a ↦ image f (t a)
⊢ image f ((insert a s).biUnion t) = (insert a s).biUnion fun a ↦ image f (t a)

Tactic:
by simp only [biUnion_insert, image_union, ih]

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 2 * List.count a l ≤ List.count a l * List.count a l

Tactic:
exact Nat.mul_le_mul_right _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
refine
    ⟨fun H => ?_, fun H =>
      H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩

Goal state after:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j = (i + j)! / (i ! * j !)

Tactic:
rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
    Nat.mul_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:
rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ (⋃ i, f i) ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j

Tactic:
iUnion_inter,

Goal state after:
α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ ⋃ i, f i ∩ ⋃ j, g j = ⋃ i, ⋃ j, f i ∩ g j
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂

Tactic:
iUnion_inter,

Goal state after:
α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ ⋃ i, ⋃ i_1, f i i_1 ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) = {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
apply le_antisymm
  · intro x hx
    induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]
  · rintro x (hx | hx)
    · exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)
    · exact Subsemigroup.closure_le.mpr subset_closure hx

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

Goal state before:
pp: case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ↑(closure (s \ t))

Tactic:
SetLike.mem_coe,

Goal state after:
case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ closure (s \ t)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a

Tactic:
by
  change a ∈ Set.ofPred IsUnit ↔ IsUnit a
  rw [Set.mem_ofPred_eq]

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ -[n+1] ∈ K

Tactic:
rw [zpow_negSucc]

Goal state after:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
⊢ ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L

Tactic:
refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (mem_of_le_of_mem · xH) (mem_of_le_of_mem · xH)⟩

Goal state after:
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
h : ↑H ⊆ ↑K ∪ ↑L
⊢ H ≤ K ∨ H ≤ L
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
⊢ 1 ∈ s

Tactic:
let ⟨x, hx⟩ := hsn

Goal state after:
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
x : G
hx : x ∈ s
⊢ 1 ∈ s
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ ↑H ↔ x * n * x⁻¹ ∈ ↑H

Tactic:
SetLike.mem_coe,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ H ↔ x * n * x⁻¹ ∈ ↑H
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ H ↔ x * n * x⁻¹ ∈ ↑H

Tactic:
SetLike.mem_coe,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ H ↔ x * n * x⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s \ {1}) = closure s

Tactic:
← closure_union_one (s \ {1}),

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s \ {1} ∪ {1}) = closure s
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
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ x ∈ ↑(comap f (closure s))

Tactic:
SetLike.mem_coe,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ x ∈ comap f (closure s)
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : G), (∃ i, a ∈ ↑(S i)) → ∀ (b : G), (∃ i, b ∈ ↑(S i)) → a * b = b * a

Tactic:
SetLike.mem_coe,

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : G), (∃ i, a ∈ S i) → ∀ (b : G), (∃ i, b ∈ S i) → a * b = b * a
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 : M →* N
M' : Submonoid M
⊢ Surjective ⇑(f.submonoidMap M')

Tactic:
by
  rintro ⟨_, x, hx, rfl⟩
  exact ⟨⟨x, hx⟩, rfl⟩

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

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

Tactic:
conv_rhs => rw [← h.eq]

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : (B'.subgroupOf B).Normal
⊢ ((A ⊓ B').subgroupOf (A ⊓ B)).Normal

Tactic:
by
  rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf A.le_normalizer hN) inf_normalizer_le_normalizer_inf

Goal state after:
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:
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.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M), (∃ i, a ∈ ↑(S i)) → ∀ (b : M), (∃ i, b ∈ ↑(S i)) → a * b = b * a

Tactic:
SetLike.mem_coe,

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M), (∃ i, a ∈ S i) → ∀ (b : M), (∃ i, b ∈ S i) → a * b = b * a
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
by
  rw [← SetLike.le_def]
  exact le_iSup _ _

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ closure s = closure (Set.range Subtype.val)

Tactic:
Subtype.range_coe

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ closure s = closure s
Module: Mathlib.Logic.Embedding.Set

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

Tactic:
by
    rintro (⟨a, ha⟩ | ⟨a, ha⟩) (⟨b, hb⟩ | ⟨b, hb⟩)
    · simp
    · simpa using h.ne_of_mem ha hb
    · simpa using h.symm.ne_of_mem ha hb
    simp

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 : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
l : FreeMonoid { x // x ∈ s }
h : (FreeMonoid.lift Subtype.val) l ∈ closure s
⊢ motive ((FreeMonoid.lift Subtype.val) l) h

Tactic:
induction l using FreeMonoid.inductionOn' with

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

Goal state before:
pp: case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
ho : m ∈ Option.casesOn (some c) (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Tactic:
Option.mem_def

Goal state after:
case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
ho : (Option.casesOn (some c) (some a) fun c ↦ if r a c then some a else some c) = some m
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ none ∈ some none

Tactic:
Option.mem_def

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ some none = some none
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case succ.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ some (ofNat α n) ∈ some (some (ofNat α n))

Tactic:
Option.mem_def

Goal state after:
case succ.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ some (some (ofNat α n)) = some (some (ofNat α n))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
this : idxOf m l = idxOf n l
⊢ n ∈ some n

Tactic:
Option.mem_def

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
this : idxOf m l = idxOf n l
⊢ some n = some n
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Set.range Subtype.val = s

Tactic:
Subtype.range_coe

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = s
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ a ≤ maximum_of_length_pos w

Tactic:
by
  simp only [le_maximum_of_length_pos_iff]
  exact le_maximum_of_mem' h

Goal state after:
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✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedOrderHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

Goal state after:
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✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
inst✝ : Lattice δ
f g : LatticeHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLenAux (n + 1) (a :: l) id [] = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
sublistsLenAux,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLenAux (n + 1) l id (sublistsLenAux n l (id ∘ cons a) []) =
    sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
s : Finset β
f : β → α
inst✝¹ : One α
inst✝ : IsBotOneClass α
⊢ s.sup f = 1 ↔ ∀ i ∈ s, f i = 1

Tactic:
simp [← bot_eq_one]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
r : ℕ
hr : r.succ ≠ 0
hrs : r.succ ≤ #s
⊢ (powersetCard r.succ s).biUnion id = s

Tactic:
rw [← sup_eq_biUnion]

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
r : ℕ
hr : r.succ ≠ 0
hrs : r.succ ≤ #s
⊢ (powersetCard r.succ s).sup id = s
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
t : Finset β
f g : β → α
H : t.Nonempty
h₂ : ∀ x ∈ t, f x = g x
c : α
⊢ t.sup' H f ≤ c ↔ t.sup' ⋯ g ≤ c

Tactic:
simp +contextual only [sup'_le_iff, h₂]

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

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : IsEmpty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i

Tactic:
exact iInf_of_isEmpty (f i) ▸ inf_le_right

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ioi ↑a ↔ x ∈ some '' Ioi a ∪ {⊤}

Tactic:
induction x

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ioi ↑a ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}

case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ioi ↑a ↔ ↑a✝ ∈ some '' Ioi a ∪ {⊤}
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ici ↑a ↔ x ∈ some '' Ici a ∪ {⊤}

Tactic:
induction x

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊤ ∈ Ici ↑a ↔ ⊤ ∈ some '' Ici a ∪ {⊤}

case coe
α : Type u_1
inst✝ : Preorder α
a a✝ : α
⊢ ↑a✝ ∈ Ici ↑a ↔ ↑a✝ ∈ some '' Ici a ∪ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ sSup (range fun i ↦ ↑i) = sSup s

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ sSup s = sSup s