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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∩ t + u = (s + u) ∩ (t + u)

Tactic:
by
  by_contra! h
  obtain ⟨a, ha⟩ := lt_iff_cons_le.1 <| h.lt_of_le <| le_inter
    (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right)
  rw [← cons_add] at ha
  exact (lt_cons_self (s ∩ t) a).not_ge <| le_inter
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l ~ l'

Tactic:
← Multiset.coe_eq_coe

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ ↑l = ↑l'
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = b :: s

Tactic:
eq_of_heq ba

Goal state after:
α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = a :: s
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) (↑s)ᶜ

Tactic:
exact s.insert_inj_on

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
a : α
⊢ ↑(map f {a}) = ↑{f a}

Tactic:
simp only [coe_map, coe_singleton, Set.image_singleton]

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
by
  simp [Finset.subset_iff, Set.subset_def]

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

Goal state before:
pp: ⊢ univ.val = {True, False}.val

Tactic:
by simp; rfl

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
a : α
ha : p a
⊢ ⟨a, ha⟩ ∈ Finset.subtype p s ↔ ↑⟨a, ha⟩ ∈ s

Tactic:
by simp [Finset.subtype, ha]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hab : b ≤ a
⊢ a - b < last n

Tactic:
lt_def

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hab : b ≤ a
⊢ ↑(a - b) < ↑(last n)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: m n : ℕ
h : n = m
⊢ (castOrderIso h).toEquiv = Equiv.cast ⋯

Tactic:
by
  subst h; rfl

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]
    simp only [succ_eq_add_one, Fin.castSucc_succ]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a.succ.castPred ha ≤ b ↔ a < b

Tactic:
by
  rw [castPred_le_iff, succ_le_castSucc_iff]

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

Goal state before:
pp: α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

Tactic:
simp only [pairwise_iff_getElem, length_ofFn, List.getElem_ofFn,
    Fin.forall_iff,
    Fin.mk_lt_mk, forall_comm (α := (_ : Prop)) (β := ℕ)]

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : i.castSucc < p
⊢ 0 < p.succAbove i

Tactic:
simpa [succAbove_of_castSucc_lt _ _ H] using castSucc_pos' h

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

Goal state before:
pp: n : ℕ
j : Fin n
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
have := succ_succAbove_succ 0 j

Goal state after:
n : ℕ
j : Fin n
this : (succ 0).succAbove j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (i.pred ⋯) = i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast
n : ℕ
P : Fin (n + 1) → Prop
i✝ : Fin n
hi : P i✝.castSucc
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
exact .inr ⟨_, hi⟩

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

Goal state before:
pp: case p
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j✝ : Fin n
hi : P (p.succAbove j✝)
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
exact .inr ⟨_, hi⟩

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

Goal state before:
pp: case inr.inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)

pp: case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
· exact (aux _ l₂ _ h).imp cons cons

Goal state after:
case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
simp [replicate, List.prod_replicate]

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

Goal state before:
pp: case pos
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)

pp: case neg
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ p (a * s.prod)

Tactic:
· simp [hs_empty, p_s a]

Goal state after:
case neg
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
⊢ p (a * s.prod)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬[] ∈ l₁ :: l₂ :: L
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
mem_cons,

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬([] = l₁ ∨ [] ∈ l₂ :: L)
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
mem_cons,

Goal state after:
α : Type u_1
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬([] = l₂ ∨ [] ∈ L)
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case empty
n : ℕ
⊢ sum 0 % n = (map (fun x ↦ x % n) 0).sum % n

Tactic:
simp [Nat.add_mod, *]

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

Goal state before:
pp: case cons
n a✝¹ : ℕ
s✝ : Multiset ℕ
a✝ : s✝.sum % n = (map (fun x ↦ x % n) s✝).sum % n
⊢ (a✝¹ ::ₘ s✝).sum % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).sum % n

Tactic:
simp [Nat.add_mod, *]

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 β
⊢ ⋂₀ S ×ˢ ⋂₀ {t} = ⋂ s ∈ S, s ×ˢ ⋂₀ {t}

Tactic:
sInter_prod_sInter hS (singleton_nonempty t),

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ ⋂₀ {t}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
· contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.zpow
    · simp

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
· rintro ⟨rfl, hn⟩
    exact empty_zpow hn

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a * x) '' t = (fun x ↦ a⁻¹ * x) ⁻¹' t

Tactic:
by
  rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x * b) '' t = (fun x ↦ x * b⁻¹) ⁻¹' t

Tactic:
by
  rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a / x) '' t = (fun x ↦ x⁻¹ * a) ⁻¹' t

Tactic:
by
  rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x / b) '' t = (fun x ↦ x * b) ⁻¹' t

Tactic:
by
  rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

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✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' s⁻¹ = (⇑f '' s)⁻¹

Tactic:
rw [← image_inv_eq_inv, ← image_inv_eq_inv]; exact image_comm (map_inv _)

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

Goal state before:
pp: case mp
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x⁻¹
⊢ ∃ x, x ∈ H ∧ P x

Tactic:
exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ ∃ x, x ∈ H ∧ P x⁻¹

Tactic:
exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

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
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : x ∈ f.ker
y : G
⊢ y * x * y⁻¹ ∈ f.ker

Tactic:
by
    rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]

Goal state after:
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
hf : Surjective ⇑f
H : Subgroup N
⊢ Disjoint H ⊤ ↔ H = ⊥

Tactic:
disjoint_top

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ H = ⊥ ↔ H = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ A ⊔ A' = B ⊓ A ⊔ A'

Tactic:
inf_of_le_right hA

Goal state after:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ A ⊔ A' = A ⊔ A'
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp.right
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
· rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ x • a = b

Tactic:
by simp [← this]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp.of_mul
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : (map f) (of head * a✝¹) = of d
⊢ ∃ a, f a = d

Tactic:
simp only [map_mul, map_of] at hb

Goal state after:
case mp.of_mul
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
⊢ ∃ a, f a = d
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
hH : H.Normal
f : G →* N
x✝ : G
⊢ x✝ ∈ Subgroup.comap f H → ∀ (g : G), g * x✝ * g⁻¹ ∈ Subgroup.comap f H

Tactic:
simp +contextual [Subgroup.mem_comap, hH.conj_mem]

Goal state after:
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:
normal_subgroupOf_iff_le_normalizer_inf

Goal state after:
G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ B' ⊓ (A ⊓ B))
Module: Mathlib.Algebra.Group.Subgroup.Basic

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

Tactic:
normal_subgroupOf_iff_le_normalizer_inf

Goal state after:
G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : A ≤ normalizer ↑(A' ⊓ A)
⊢ A ⊓ B ≤ normalizer ↑(A' ⊓ B ⊓ (A ⊓ B))
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:
normal_subgroupOf_iff_le_normalizer_inf

Goal state after:
G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ≤ normalizer ↑(N ⊓ H)
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩

Tactic:
exact Or.inr (Lex.left _ _ hji)

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

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

Tactic:
exact mul_left x hx y ih

Goal state after:
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 n✝ n : M
i : ℕ
⊢ (fun x ↦ n✝ ^ x) i = n ↔ ((powersHom M) n✝) i = n

Tactic:
by simp; rfl

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

Goal state before:
pp: case append_singleton
α : 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]
⊢ m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r b m

Tactic:
ho

Goal state after:
case append_singleton
α : 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]
ho : m ∈ foldl (argAux r) o (tl ++ [a])
⊢ ¬r b m
Module: Mathlib.Data.List.MinMax

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

Tactic:
WithBot.coe_max

Goal state after:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ a✝ ∈ s.sup t ↔ a✝ ∈ s.biUnion t

Tactic:
rw [mem_sup, mem_biUnion]

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

Goal state before:
pp: case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails → init ++ tail = hd :: tl

Tactic:
mem_cons,

Goal state after:
case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) = ([], hd :: tl) ∨ (init, tail) ∈ (map (fun t ↦ hd :: t) tl.inits).zip tl.tails → init ++ tail = hd :: tl
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl → (init, tail) ∈ ([], hd :: tl) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails

Tactic:
mem_cons,

Goal state after:
case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl → (init, tail) = ([], hd :: tl) ∨ (init, tail) ∈ (map (fun t ↦ hd :: t) tl.inits).zip tl.tails
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)
⊢ foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      (a :: l₁) =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] (a :: l₁))

Tactic:
foldr_cons,

Goal state after:
case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)
⊢ flatMap (fun x ↦ [x, a :: x])
      (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc)
        (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂) l₁) =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] (a :: l₁))
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Tactic:
rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ powersetCard n ⟦l⟧ ≤ powerset ⟦l⟧

Tactic:
simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]

Goal state after:
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
· refine (hs hi.1 hj.1 hij).mono ?_ ?_
    · convert! le_iSup₂ (α := α) i' hi.2; rfl
    · convert! le_iSup₂ (α := α) j' hj.2; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
rcases isEmpty_or_nonempty β
  · simp [iSup_of_empty']
  rcases isEmpty_or_nonempty γ
  · simp [iSup_of_empty']
  have h₁ : BddAbove (Set.range fun b ↦ ⨆ c, f (b, c)) := by
    rw [bddAbove_def] at hf ⊢
    obtain ⟨B, hB⟩ := hf
    refine ⟨B, fun y hy ↦ ?_⟩
    obtain ⟨z, rfl⟩ := Set.mem_range.mp hy
    exact ciSup_le fun c ↦ by grind
  have h₂ b : BddAbove (Set.range fun c ↦ f (b, c)) := by
    rw [bddAbove_def] at hf ⊢
    obtain ⟨B, hB⟩ := hf
    exact ⟨B, by grind⟩
  refine eq_of_forall_ge_iff fun c ↦ ?_
  rw [ciSup_le_iff (bddAbove_iff_subset_Iic.mpr hf), ciSup_le_iff h₁]
  conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)]
  simp [Prod.forall]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b

Tactic:
simp [← Ici_inter_Iic]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
⊢ BddAbove (range fun i ↦ g ↑i)

Tactic:
simpa [bddAbove_def] using hf

Goal state after: