mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
⊢ #s = #t

Tactic:
refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)
  rw [← left_inv a1 h1, ← left_inv a2 h2]
  simp only [eq]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ #s ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
refine ⟨fun H => ?_, ?_⟩
  · obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
    · exact ⟨Classical.arbitrary α, empty_subset _⟩
    · exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩
  · rintro ⟨x, hx⟩
    rw [← card_singleton x]
    exact card_le_card hx

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ #sᶜ.toFinset = card α - #s.toFinset

Tactic:
← Finset.card_compl,

Goal state after:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ #sᶜ.toFinset = #s.toFinsetᶜ
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
n : ℕ
hn' : n < #s
hn : ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
⊢ ∃ n ≤ #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
exact ⟨n, hn'.le, hn⟩

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

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
· simp [init, h, castSucc_inj]

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

Goal state before:
pp: case step
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : (n + 2).le 0
⊢ False

Tactic:
| step h =>

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ insertNth 0 x p = cons x fun j ↦ cast ⋯ (p j)

Tactic:
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩
  ext j
  convert! (cons_succ x p j).symm

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

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

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:
· have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert_cons, if_neg hr] at ih
        exact .cons _ ih

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

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.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
H : Set.InjOn g ↑s
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

Tactic:
simp only [fold, image_val_of_injOn H, Multiset.map_map]

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

Goal state before:
pp: case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)

Tactic:
| right i =>

Goal state after:
case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)

Tactic:
rw [Fin.natAdd_lt_natAdd_iff] at hi

Goal state after:
case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : i < Fin.find (fun j ↦ p (natAdd m j)) ⋯
⊢ ¬p (natAdd m i)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ u ∈ map (fun x ↦ a + x) s' → False

Tactic:
mem_map

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ Forall₂ R l.dropLast l.tail

Tactic:
induction l using twoStepInduction

Goal state after:
case nil
α : Type u_1
R : α → α → Prop
⊢ IsChain R [] ↔ Forall₂ R [].dropLast [].tail

case singleton
α : Type u_1
R : α → α → Prop
x✝ : α
⊢ IsChain R [x✝] ↔ Forall₂ R [x✝].dropLast [x✝].tail

case cons_cons
α : Type u_1
R : α → α → Prop
x✝ y✝ : α
xs✝ : List α
a✝¹ : IsChain R xs✝ ↔ Forall₂ R xs✝.dropLast xs✝.tail
a✝ : ∀ (y : α), IsChain R (y :: xs✝) ↔ Forall₂ R (y :: xs✝).dropLast (y :: xs✝).tail
⊢ IsChain R (x✝ :: y✝ :: xs✝) ↔ Forall₂ R (x✝ :: y✝ :: xs✝).dropLast (x✝ :: y✝ :: xs✝).tail
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
l : List β
⊢ IsChain R (map f l) ↔ IsChain (fun a b ↦ R (f a) (f b)) l

Tactic:
induction l using twoStepInduction

Goal state after:
case nil
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
⊢ IsChain R (map f []) ↔ IsChain (fun a b ↦ R (f a) (f b)) []

case singleton
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ : β
⊢ IsChain R (map f [x✝]) ↔ IsChain (fun a b ↦ R (f a) (f b)) [x✝]

case cons_cons
α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
x✝ y✝ : β
xs✝ : List β
a✝¹ : IsChain R (map f xs✝) ↔ IsChain (fun a b ↦ R (f a) (f b)) xs✝
a✝ : ∀ (y : β), IsChain R (map f (y :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (y :: xs✝)
⊢ IsChain R (map f (x✝ :: y✝ :: xs✝)) ↔ IsChain (fun a b ↦ R (f a) (f b)) (x✝ :: y✝ :: xs✝)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
⊢ IsChain S (pmap f l hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) l

Tactic:
induction l using twoStepInduction

Goal state after:
case nil
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
hl : ∀ (a : α), a ∈ [] → p a
⊢ IsChain S (pmap f [] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) []

case singleton
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ : α
hl : ∀ (a : α), a ∈ [x✝] → p a
⊢ IsChain S (pmap f [x✝] hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) [x✝]

case cons_cons
α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
x✝ y✝ : α
xs✝ : List α
a✝¹ :
  ∀ (hl : ∀ (a : α), a ∈ xs✝ → p a), IsChain S (pmap f xs✝ hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) xs✝
a✝ :
  ∀ (y : α) (hl : ∀ (a : α), a ∈ y :: xs✝ → p a),
    IsChain S (pmap f (y :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (y :: xs✝)
hl : ∀ (a : α), a ∈ x✝ :: y✝ :: xs✝ → p a
⊢ IsChain S (pmap f (x✝ :: y✝ :: xs✝) hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) (x✝ :: y✝ :: xs✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun x ↦ count x (a :: as)) (filter p (a :: as).dedup)).sum = countP p (a :: as)

Tactic:
simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
    congr 1
    · refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
    · simp only [beq_iff_eq]
      by_cases hp : p a
      · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]
      · exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n = [] ↔ l = []

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

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

Goal state before:
pp: case succ
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f (f^[i] l[0]) = l[i + 1]

Tactic:
h (by lia)

Goal state after:
case succ
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f l[i] = l[i + 1]
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
⊢ (n • s).dedup = s.dedup

Tactic:
ext a; by_cases h : a ∈ s <;> simp [h, hn]

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

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (l.rotate n)[m]? = l[(m + n) % l.length]?

Tactic:
rw [rotate_eq_drop_append_take_mod]
  rcases lt_or_ge m (l.drop (n % l.length)).length with hm | hm
  · rw [getElem?_append_left hm, getElem?_drop, ← add_mod_mod]
    rw [length_drop, Nat.lt_sub_iff_add_lt] at hm
    rw [mod_eq_of_lt hm, Nat.add_comm]
  · have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
    rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]
    · congr 1
      rw [length_drop] at hm
      have hm' := Nat.sub_le_iff_le_add'.1 hm
      have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
      conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
      lia
    · rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
g : α → Multiset β
⊢ ∀ (a : α) (s : Multiset α),
    (s.bind fun a ↦ f a ::ₘ g a) = map f s + s.bind g →
      ((a ::ₘ s).bind fun a ↦ f a ::ₘ g a) = map f (a ::ₘ s) + (a ::ₘ s).bind g

Tactic:
by simp +contextual [add_comm, add_left_comm, add_assoc]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → Option β
a : α
m : Multiset α
ih : filterMap f m = m.bind fun a ↦ (Option.map singleton (f a)).getD 0
⊢ filterMap f (a ::ₘ m) = (a ::ₘ m).bind fun a ↦ (Option.map singleton (f a)).getD 0

Tactic:
simp [filterMap_cons, ih]

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
s : Multiset ι
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
l : List ι
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) ⟦l⟧).prod = f (map f₁ ⟦l⟧).prod (map f₂ ⟦l⟧).prod

Tactic:
by
    simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
classical
  refine s.induction ?_ ?_
  · simp
  · intro i s his ih
    simp only [disjoint_union_left, biUnion_insert, forall_mem_insert, ih]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
⊢ count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0

Tactic:
by
  induction l with
  | nil => simp
  | cons c l ihl =>
    have H₁ {x y z : α} : count (x, y) (map (z, ·) l) = if z = x then count y l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    have H₂ {x y z : α} : count (x, y) (map (·, z) l) = if z = y then count x l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    simp only [(offDiag_cons_perm _ _).count_eq, count_append, ihl, H₁, H₂, count_cons, beq_iff_eq]
    have := Nat.le_mul_self (count c l)
    split_ifs <;> simp_all <;> grind

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x : α × α
⊢ x ∈ l.offDiag ↔ x.fst ∈ l ∧ x.snd ∈ l ∧ x.fst ≠ x.snd

Tactic:
by
  rcases x with ⟨x, y⟩
  simp_rw [mem_offDiag_iff_getElem, mem_iff_getElem, Ne]
  constructor
  · rintro ⟨i, hi, j, hj, hne, rfl, rfl⟩
    exact ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, mt h.getElem_inj_iff.1 hne⟩
  · rintro ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, hne⟩
    exact ⟨i, hi, j, hj, mt h.getElem_inj_iff.2 hne, rfl, rfl⟩

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

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ 0 < (n - k)! * (k - s)! * s !

Tactic:
apply_rules [factorial_pos, Nat.mul_pos]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
⊢ (cons m a (f a ⋯) fun a' ha' ↦ f a' ⋯) = f

Tactic:
by
  ext a' h'
  by_cases h : a' = a
  · subst h
    rw [Pi.cons_same]
  · rw [Pi.cons_ne _ h]

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

Goal state before:
pp: case inr
r n : ℕ
b : n < r
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rw [choose_eq_zero_of_lt b]

Goal state after:
case inr
r n : ℕ
b : n < r
⊢ 0 ≤ n.choose (n / 2)
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
M : Type ?u.6
N : Type ?u.8
inst✝¹ : Semigroup M
inst✝ : Semigroup N
s : Set M
f : M → N
hs : closure s = ⊤
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
by simp only [← mul_assoc, h₁, h₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t

Tactic:
exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy

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

Goal state before:
pp: case mem.mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x✝ y✝ : M
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : motive x✝ z hx✝ ⋯
h₂ : motive y✝ z hy✝ ⋯
⊢ motive (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case mem.mul
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x✝ y✝ : G
hx✝ : x✝ ∈ closure k
hy✝ : y✝ ∈ closure k
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

Goal state after:
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
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ map f ⊤ = ⊤

Tactic:
map_top_of_surjective _ hf

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Group.Submonoid.Operations

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

Tactic:
simp_rw [SetLike.ext'_iff]

Goal state after:
ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ ↑(pi Set.univ S) = ↑⊥ ↔ ∀ (i : ι), ↑(S i) = ↑⊥
Module: Mathlib.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:
rw [← decode₂_isPartialInv (Option.get _ h), Option.some_get]

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

Goal state before:
pp: case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]

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

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

Tactic:
simp_rw [SetLike.ext'_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ s * {b} = s <• a ∪ s <• b

Tactic:
mul_singleton

Goal state after:
α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ (fun x ↦ x * a) '' s ∪ (fun x ↦ x * b) '' s = s <• a ∪ s <• b
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ H.normalCore ≤ map (↑(MulAut.conj g)) H

Tactic:
← Normal.map_conj_eq H.normalCore g,

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ map (↑(MulAut.conj g)) H.normalCore ≤ map (↑(MulAut.conj g)) H
Module: Mathlib.Algebra.Group.Subgroup.Basic

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
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₃
x : G₁
hx : x ∈ f.ker
⊢ (φ.comp f) x = 1

Tactic:
simp [mem_ker.mp hx]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
a : α
b : β
⊢ (a, b) ∈ x • graphOn (⇑f) s ↔ (a, b) ∈ graphOn (fun a ↦ x.2 / f x.1 * f a) (x.1 • s)

Tactic:
simp [mem_smul_set_iff_inv_smul_mem, inv_mul_eq_iff_eq_mul, mul_left_comm _ _⁻¹,
    eq_inv_mul_iff_mul_eq, ← mul_div_right_comm, div_eq_iff_eq_mul, mul_comm b]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
a b : Lex (α × β)
this✝ : DecidableLT (Lex (α × β))
this : Std.LawfulBEqOrd (Lex (α × β))
⊢ ∀ {x y : Lex (α × β)}, compare x y = Ordering.lt ↔ x < y

Tactic:
simp [compare_def, compareLex, compareOn, Ordering.then_eq_lt, toLex_lt_toLex,
        compare_lt_iff_lt]

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

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
simp [mem_sup]
  aesop

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

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

Tactic:
mem_map

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
rw [if_pos rfl]
      exact Nat.zero_le _

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
⊢ ∃ n, ↑x + n + 1 ∈ s

Tactic:
by_contra h

Goal state after:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
⊢ False
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, a ∈ map Embedding.inl s → a ∉ map Embedding.inr t

Tactic:
mem_map

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, (∃ a_1 ∈ s, Embedding.inl a_1 = a) → ¬∃ a_2 ∈ t, Embedding.inr a_2 = a
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)) = max (↑hd) tl.maximum

Tactic:
foldr,

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.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).min = ↑a

Tactic:
exact min_insert

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'

Tactic:
exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)

Goal state after: