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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
⊢ filter p (s - t) = filter p s - filter p t

Tactic:
revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
  rw [sub_cons, IH]
  by_cases h : p a
  · rw [filter_cons_of_pos _ h, sub_cons]
    congr
    by_cases m : a ∈ s
    · rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]
    · rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]
  · rw [filter_cons_of_neg _ h]
    by_cases m : a ∈ s
    · rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),
        cons_erase m]
    · rw [erase_of_notMem m]

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

Goal state before:
pp: case nil
α : Type u_1
l₁ : List α
h : l₁ <+: []
⊢ [] = l₁ ++ drop l₁.length []

Tactic:
simp [List.prefix_nil.mp h]

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ a ∉ (s.erase a).erase b

Tactic:
simp [insert_erase ha, *]

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ b ∉ (s.erase a).erase b

Tactic:
simp [insert_erase ha, *]

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

Goal state before:
pp: case refine_3
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ ¬a = b

Tactic:
simp [insert_erase ha, *]

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

Goal state before:
pp: case refine_4
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ cons a (cons b ((s.erase a).erase b) ⋯) ⋯ = s

Tactic:
simp [insert_erase ha, *]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ.Nonempty ↔ Nonempty α

Tactic:
exact univ_nonempty_iff

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map Subtype.val univ.val = (filter p univ).val

Tactic:
apply (map_val (Function.Embedding.subtype p) univ).symm.trans

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ (map (Embedding.subtype p) univ).val = (filter p univ).val
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : Fin n
⊢ motive i

Tactic:
obtain ⟨i, hi⟩ := i
  induction i using Nat.strong_induction_on with
  | h j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < b ↔ a ≤ b

Tactic:
rw [castSucc_pred_eq_pred_castSucc, pred_castSucc_lt_iff]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ i.castPred hi = j.castPred hj ↔ i = j

Tactic:
by
  simp_rw [Fin.ext_iff, le_antisymm_iff, ← le_def, castPred_le_castPred_iff]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ find? p (ofFn f) = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true

Tactic:
find?_eq_some_iff_getElem

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ (p b = true ∧ ∃ i h, (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true) ↔
    p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t

Tactic:
· rintro ⟨hst, h⟩
    obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} := card_eq_one.mp (by grind)
    grind =>
      have : a ∈ t \ s
      have h : insert a s ⊆ t
      have := eq_of_subset_of_card_le h
      instantiate

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

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : ¬i < n
sub_lt : i - n < m
nlt_add : ¬i < n + m
⊢ bs ⟨i - n, ⋯⟩ = b

Tactic:
obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt

Goal state after:
case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
isLt : n + m < n + (m + 1)
lt_n : ¬n + m < n
sub_lt : n + m - n < m
nlt_add : ¬n + m < n + m
⊢ bs ⟨n + m - n, ⋯⟩ = b
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : x i = x₀
⊢ False

Tactic:
rw [← @snoc_last n (fun i ↦ α) x₀ x, ← @snoc_castSucc n (fun i ↦ α) x₀ x i,
      h.eq_iff] at hi

Goal state after:
case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : i.castSucc = last n
⊢ False
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
e : α ↪ α
⊢ map e univ = univ

Tactic:
rw [← e.toEmbedding_equivOfFiniteSelfEmbedding, univ_map_equiv_to_embedding]

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

Goal state before:
pp: case mp.cons_cons.refine_2
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ),
    (a✝¹ :: l₁✝)[ix]? =
      (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) ix]?

Tactic:
rintro ⟨_ | i⟩
        · simp
        · simpa using hf _

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

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
⊢ InjOn f s

Tactic:
have : Finite s := finite_coe_iff.mpr hs

Goal state after:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
this : Finite ↑s
⊢ InjOn f s
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
⊢ SurjOn f s s

Tactic:
have : Finite s := finite_coe_iff.mpr hs

Goal state after:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
this : Finite ↑s
⊢ SurjOn f s s
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)

Tactic:
obtain ⟨hr, hp⟩ := pairwise_cons.mp hr

Goal state after:
case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
l₁✝ : List α
hr✝ : Pairwise r (head✝ :: l₁✝)
h : l₁✝ <+ tail✝
hr : ∀ (a' : α), a' ∈ l₁✝ → r head✝ a'
hp : Pairwise r l₁✝
⊢ head✝ :: l₁✝ <+ insertionSort r (head✝ :: tail✝)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Tactic:
← toFinset_card,

Goal state after:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ {x | x ≠ a}.toFinset.card = Fintype.card α - 1
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ⟨ai, a⟩.fst = ⟨bi, b⟩.fst
h : ⟨ai, a⟩.snd = ⟨bi, b⟩.snd ∘ Fin.cast hi
⊢ ⟨ai, a⟩ = ⟨bi, b⟩

Tactic:
dsimp only at hi

Goal state after:
α : Type u_1
ai : ℕ
a : Fin ai → α
bi : ℕ
b : Fin bi → α
hi : ai = bi
h : ⟨ai, a⟩.snd = ⟨bi, b⟩.snd ∘ Fin.cast hi
⊢ ⟨ai, a⟩ = ⟨bi, b⟩
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, l₁.length ≤ l₂.length → l₁ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
subst b
        exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
inst✝ : Trans R R R
hl : IsChain R (a :: l)
hb : b ∈ l
⊢ R a b

Tactic:
by
  rw [isChain_iff_pairwise] at hl
  exact rel_of_pairwise_cons hl hb

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

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod

Tactic:
← hl,

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ n • {a} = replicate n a

Tactic:
rw [← replicate_one, nsmul_replicate, mul_one]

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

Goal state before:
pp: case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate i = l.rotate j

Tactic:
rw [← rotate_mod, h, rotate_mod]

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
s : Multiset α
t : (a : α) → Multiset (σ a)
a : α
b : σ a
⊢ ⟨a, b⟩ ∈ s.sigma t ↔ ⟨a, b⟩.fst ∈ s ∧ ⟨a, b⟩.snd ∈ t ⟨a, b⟩.fst

Tactic:
simp [Multiset.sigma, and_left_comm]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _

Goal state after:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Goal state after:
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)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle i x) (mulSingle j y)

Tactic:
ext k

Goal state after:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
k : I
⊢ (mulSingle i x * mulSingle j y) k = (mulSingle j y * mulSingle i x) k
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

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

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

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

Goal state after:
case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
⊢ ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ ⋃ x ∈ t, g x

Tactic:
by
  ext ⟨_, _⟩
  simp only [mem_iUnion, mem_prod, exists_prop, Prod.exists]; tauto

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
S : ι → Subgroup G
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

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

Goal state before:
pp: G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
⊢ f.range.subgroupOf K = (f.codRestrict K ⋯).range

Tactic:
ext k

Goal state after:
G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ k ∈ f.range.subgroupOf K ↔ k ∈ (f.codRestrict K ⋯).range
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑(y.1⁻¹ * x.1) = 1 ∧ ↑(x.2 * y.2⁻¹) = 1
⊢ x = y

Tactic:
coe_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑y.1⁻¹ * ↑x.1 = 1 ∧ ↑(x.2 * y.2⁻¹) = 1
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑y.1⁻¹ * ↑x.1 = 1 ∧ ↑(x.2 * y.2⁻¹) = 1
⊢ x = y

Tactic:
coe_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : ↑y.1⁻¹ * ↑x.1 = 1 ∧ ↑x.2 * ↑y.2⁻¹ = 1
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.MulOpposite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ MulOpposite.unop x ∈ normalizer ↑H ↔ x ∈ normalizer ↑H.op

Tactic:
mem_normalizer_iff',

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ (∀ (n : G), n * MulOpposite.unop x ∈ H ↔ MulOpposite.unop x * n ∈ H) ↔ x ∈ normalizer ↑H.op
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ (bit b n + 1).div2 = bif (bit b n).bodd then (bit b n).div2.succ else (bit b n).div2

Tactic:
cases b <;>
    simp [bit_val, div2_val, Nat.succ_div, Nat.add_assoc, Nat.dvd_add_right (Nat.dvd_mul_right _ _)]

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

Goal state before:
pp: case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
by_cases h₂ : a₂ < b

Goal state after:
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
· simp [h₂, h]

Goal state after:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Tactic:
apply Nat.add_lt_add_of_le_of_lt

Goal state after:
case neg.hle
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b ≤ a₂ * a₂

case neg.hlt
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ a₁ < a₂ + b
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
· simp [h₂, h]

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : N
hx : x ∈ map f (normalizer ↑H)
⊢ x ∈ normalizer ↑(map f H)

Tactic:
obtain ⟨y, hy, rfl⟩ := Subgroup.mem_map.mp hx

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : y ∈ normalizer ↑H
hx : f y ∈ map f (normalizer ↑H)
⊢ f y ∈ normalizer ↑(map f H)
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a * b)

Tactic:
IsIdempotentElem,

Goal state after:
S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * b * (a * b) = a * b
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ IsIdempotentElem (f e)

Tactic:
IsIdempotentElem,

Goal state after:
M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ f e * f e = f e
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

Tactic:
dsimp [liftOfRightInverseAux]

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x)) = g x
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod ∧ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
constructor <;> apply List.prod_le_prod' <;> intros

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ≤ max (f i✝) (g i✝)

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod ∧ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod

Tactic:
constructor <;> apply List.prod_le_prod' <;> intros

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ f i✝

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ g i✝
Module: Mathlib.Algebra.Order.BigOperators.Group.List

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

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

Tactic:
· rw [prod_take_succ _ _ h]
    exact le_self_mul

Goal state after:
case inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case neg
α : 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 = []
hla_restrict : ∀ (x : α), x ∈ l → p x
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict

Goal state after:
case neg
α : 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 = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
⊢ f (a * l.prod) ≤ f a * (map f l).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
H : Subgroup G
⊢ Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H

Tactic:
by
  rw [← AddSubgroup.subgroupOf_inertia, Subgroup.subgroupOf_map_subtype]

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

Goal state before:
pp: case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
obtain ⟨v, hv⟩ := exists_lt y.2
      use toLex (y.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ ((∃ a_1, a_1 ∈ s ∧ inl a_1 = inl a) ∨ ∃ b, b ∈ t ∧ inr b = inl a) ↔ a ∈ s

Tactic:
or_iff_left

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ (∃ a_1, a_1 ∈ s ∧ inl a_1 = inl a) ↔ a ∈ s

α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
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
⊢ foldl (fun r l ↦ r ++ [l, a :: l]) [] (r ++ [l]) = sublistsAux a r ++ [l, a :: l]

Tactic:
foldl_append

Goal state after:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ foldl (fun r l ↦ r ++ [l, a :: l]) (foldl (fun r l ↦ r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 (h :: tl) ++
      flatMap (fun a ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
List.sublistsLen_zero,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [[]] ++ flatMap (fun a ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'