mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
by_cases hl : l = []

Goal state after:
case pos
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case pos
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup

Tactic:
· simp_all

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.reverse.tail.Nodup ↔ l.tail.Nodup)
h : (a :: l)[0]? = (a :: l).getLast?
hl : ¬l = []
⊢ (a :: l).reverse.tail.Nodup ↔ (a :: l).tail.Nodup
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'

Tactic:
intro h
        rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
        rcases h with ⟨b, bs, hab, h₀, rfl⟩
        exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩

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

Goal state before:
pp: α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup

Tactic:
simp [List.dropLast_eq_take]

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

Goal state before:
pp: α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l.concat a).Nodup

Tactic:
rw [concat_eq_append]; exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)

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

Goal state before:
pp: α : Type u
l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
h : l₂.Nodup
⊢ (l₁ ∪ l₂).Nodup

Tactic:
by
  induction l₁ generalizing l₂ with
  | nil => exact h
  | cons a l₁ ih => exact (ih h).insert

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

Goal state before:
pp: case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : ¬head✝ ∈ l₂
⊢ tail✝.bagInter l₂ <+ (head✝ :: tail✝) ∩ l₂

Tactic:
· simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : ¬a ∈ l₁
⊢ List.count a l₁.dedup = List.count a l₂.dedup

Tactic:
simp [h, count_eq_zero_of_not_mem, mt p.mem_iff.2]

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
rw [h₁]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ (List.take n' xs.reverse).reverse ~ ys ∩ (List.take n' xs.reverse).reverse
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mpr
α : Type u_1
x y : α
⊢ x = y → [x] <:+: [y]

Tactic:
· rintro rfl; rfl

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.tails.length
⊢ l.tails[n] = drop n l

Tactic:
by
  induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.inits.length
⊢ l.inits[n] = take n l

Tactic:
by
  induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

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

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
⊢ {a}.disjUnion s ⋯ = cons a s ⋯

Tactic:
singleton_disjUnion

Goal state after:
α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
⊢ cons a s ⋯ = cons a s ⋯
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (union s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

Tactic:
simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (union s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

Tactic:
simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s.disjUnion t h
⊢ (disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

Tactic:
simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s.disjUnion t h
⊢ (disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

Tactic:
simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n))

Tactic:
by
  ext (⟨⟩ | ⟨n⟩) <;> simp [Nat.zero_lt_succ n]

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

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

Tactic:
pred_castSucc_lt_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
y : Fin n
h : y.castSucc ≠ last n
⊢ (y.castSucc.castPred h).castSucc = y.castSucc

Tactic:
rw [castPred_castSucc]

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
rw [Fin.val_neg', Fin.val_one, Nat.add_one_sub_one, Nat.mod_eq_of_lt]

Goal state after:
case succ
n✝ : ℕ
⊢ n✝ + 1 < n✝ + 1 + 1
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
have hkb : k < b := by lia

Goal state after:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ Set.InjOn f ↑s

Tactic:
rw [← card_image_iff]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ #(image f s) = #s
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x

Tactic:
exact succAbove_ne _ _

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
exact ⟨u.erase a, by grind⟩

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

Goal state before:
pp: case refine_1
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn Fin.elim0).Nodup → Function.Injective Fin.elim0

Tactic:
intro _
    exact Function.injective_of_subsingleton _

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ m + n = n

Tactic:
by rw [hu, Nat.zero_add]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b

Tactic:
hx a,

Goal state after:
α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ x = b
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
· simp_all

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
⊢ l'.head! ≤ l.head!

Tactic:
by_cases hl : l = []

Goal state after:
case pos
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : l = []
⊢ l'.head! ≤ l.head!

case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l

Tactic:
exact h.imp .cons (congr_arg _)

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l

Tactic:
by
  rw [rotate_eq_rotate']; exact rotate'_eq_drop_append_take

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Tactic:
simp [rotate_cons_succ, hn]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (a :: l).reverse.alternatingProd = (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)

Tactic:
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
      alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, inv_inv]

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)

Tactic:
by
  rw [← length_reverse, ← rotate_eq_iff]
  induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate_cons_succ, ← rotate_rotate, hn]
      simp

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝ : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
hab : Rel r a✝ b✝
hst : Rel (Rel r) as✝ bs✝
ih : Rel r as✝.join bs✝.join
⊢ Rel r (a✝ ::ₘ as✝).join (b✝ ::ₘ bs✝).join

Tactic:
simpa using hab.add ih

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

Goal state before:
pp: ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
j : ι
x✝ : j ≠ i
⊢ z j ∈ v j

Tactic:
by simpa using hz j

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)

Tactic:
simpa using biInter_range

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

Goal state before:
pp: case mp.inl
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
exact hs.zpow

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

Goal state before:
pp: case refine_1
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
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i → ∃ i, p i ∧ x ∈ K i

Tactic:
suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
      simpa only [closure_iUnion, closure_eq (K _)] using this

Goal state after:
case refine_1
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
⊢ x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → ∃ i, p i ∧ x ∈ K i
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op

Tactic:
op_closure

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op

Tactic:
op_closure

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ n % 2 = n.bodd.toNat

Tactic:
cases n using bitCasesOn with
  | bit b n => cases b <;> simp

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op

Tactic:
op_closure

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
⊢ encode ((decode₂ α x).get h) = x

Tactic:
← decode₂_isPartialInv (Option.get _ h),

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
⊢ decode₂ α x = some ((decode₂ α x).get h)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: a b k : ℤ
⊢ (fun x ↦ x • a) k = b ↔ b = a * k

Tactic:
by rw [mul_comm, eq_comm, ← smul_eq_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Characteristic
⊢ (⨅ i ∈ s, H i).Characteristic

Tactic:
simp [← iInf_subtype'', characteristic_iInf, h]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ Commute x y

Tactic:
change x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ 1 ≤ l.prod

Tactic:
induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [prod_cons]
    exact one_le_mul (hl₁ hd mem_cons_self) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))

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

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 : α), 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 : α), 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'

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 : α), 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 : α), i ∈ l → min (f i) (g i) ≤ g i
Module: Mathlib.Data.Sigma.Lex

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

Tactic:
exact Lex.left _ _ (symm hij)

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_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
this : x ∈ closure s
⊢ motive x

Tactic:
induction this using closure_induction_left with

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

Goal state before:
pp: case none
α : 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
harg : argmax f l = none
⊢ m ∈ none

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
⊢ m ∈ some n

Tactic:
· simp_all

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
⊢ m ∈ some n
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ (head✝ :: tail✝ ++ l₂).maximum = max (head✝ :: tail✝).maximum l₂.maximum

Tactic:
maximum_cons,

Goal state after:
case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ (head✝ :: tail✝ ++ l₂).maximum = max (max (↑head✝) tail✝.maximum) l₂.maximum
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ (head✝ :: (tail✝ ++ l₂)).maximum = max (max (↑head✝) tail✝.maximum) l₂.maximum

Tactic:
maximum_cons,

Goal state after:
case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ max (↑head✝) (tail✝ ++ l₂).maximum = max (max (↑head✝) tail✝.maximum) l₂.maximum
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
| #({y ∈ range ↑(succ (ofNat s n)) | y ∈ s}) = n + 1

Tactic:
rhs

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
| n + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ l[i] ∈ l

Tactic:
exact getElem_mem _

Goal state after:
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 ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = (hd :: tl).maximum

Tactic:
maximum_cons,

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 ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = max (↑hd) tl.maximum
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
⊢ ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
intro r₁ r₂

Goal state after:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case trans
α : Type u_1
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : powersetAux' l₁✝ ~ powersetAux' l₂✝
IH₂ : powersetAux' l₂✝ ~ powersetAux' l₃✝
⊢ powersetAux' l₁✝ ~ powersetAux' l₃✝

Tactic:
exact IH₁.trans IH₂

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ List.map (fun x ↦ (x, ↑l₂ - x)) (powersetAux l₁) ~ List.map (fun x ↦ (x, ↑l₂ - x)) (powersetAux l₂)

Tactic:
exact (powersetAux_perm p).map _

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

Goal state before:
pp: α : Type u
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂

Tactic:
induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_

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

Goal state before:
pp: α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux n l₁ ~ powersetCardAux n l₂

Tactic:
induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_

Goal state after:
case succ
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂