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

Goal state before:
pp: case mp.cons
α : Type u_1
xs : List α
x head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ w✝ : List α
h : head✝ :: tail✝ ++ head✝² :: head✝¹ :: tail✝¹ ++ w✝ = [x]
⊢ head✝² :: head✝¹ :: tail✝¹ = [] ∨ head✝² :: head✝¹ :: tail✝¹ = [x]

Tactic:
simp at h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ∈ s.erase b

Tactic:
simp only [mem_erase]; exact And.intro

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ RightInverse (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩

Tactic:
by rintro (_ | y) <;> grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
⊢ (replicate n a).toFinset = {a}

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ {a}
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Finset α
⊢ filter p s = filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)

Tactic:
by
  simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)

Tactic:
by
  simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a : α
⊢ (replicate n a).toFinset = if n = 0 then ∅ else {a}

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ if n = 0 then ∅ else {a}
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (Multiset.map Subtype.val s.attach.val).dedup = s.val

Tactic:
attach_val,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (Multiset.map Subtype.val s.val.attach).dedup = s.val
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s

Tactic:
ext x

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑a - 1 ≤ ↑(b.castPred ⋯)

Tactic:
calc
      _ ≤ _ := Nat.pred_le _
      _ ≤ _ := H

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [coe_int_sub_eq_ite]
  split
  · rw [Int.emod_eq_of_lt] <;> omega
  · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt] <;> omega

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)

Tactic:
by
  split <;> fin_omega

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

Goal state before:
pp: n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
⊢ ↑(i - 1) = ↑i - 1

Tactic:
Fin.sub_val_of_le (one_le_of_ne_zero hi),

Goal state after:
n : ℕ
i : Fin n.succ
this : NeZero n.succ
hi : i ≠ 0
⊢ ↑i - ↑1 = ↑i - 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.succ ≤ p ∨ p ≤ i.castSucc

Tactic:
rw [le_castSucc_iff, ← castSucc_lt_iff_succ_le]
  exact p.castSucc_lt_or_lt_succ i

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

Goal state before:
pp: case mpr.refine_1
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
h : (fun x1 x2 ↦ x1 < x2) i 0
⊢ r (f i) (f 0)

Tactic:
simp at h

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i ≠ 0
⊢ predAbove 0 i = i.pred hi

Tactic:
by
  obtain ⟨y, rfl⟩ := exists_succ_eq.2 hi
  exact predAbove_zero_succ

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

Goal state before:
pp: α β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
h : α = β
⊢ α ≃ β

Tactic:
by rw [h]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by
  simp_rw [two_lt_card_iff, exists_and_left]

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
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n' + m = n + m

Tactic:
by rw [h]

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
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m' = n + m

Tactic:
by rw [h]

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

Goal state before:
pp: case mpr
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
refine
      ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          ?_,
        ?_⟩

Goal state after:
case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ StrictMono fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length

case mpr.refine_2
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ ∀ (ix : ℕ),
    l[ix]? =
      l'[(OrderEmbedding.ofStrictMono (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ?mpr.refine_1)
          ix]?
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Multiset α
⊢ ⋯.toFinset = s.toFinset

Tactic:
ext x

Goal state after:
α : Type u
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ s.toFinset
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
hs : a :: as <+ b :: bs
⊢ (if r x a then x :: a :: as else a :: orderedInsert r x as) <+
    if r x b then x :: b :: bs else b :: orderedInsert r x bs

Tactic:
cases hs <;> split_ifs with hr

Goal state after:
case pos
α : 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
⊢ x :: a :: as <+ x :: b :: bs

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
⊢ x :: a :: as <+ b :: orderedInsert r x bs

case pos
α : 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 <+ x :: b :: bs

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

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
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)

Tactic:
by
  dsimp only [fold]
  rw [cons_val, Multiset.map_cons, fold_cons_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedGT ↔ StrictAnti f

Tactic:
simp only [sortedGT_iff_strictAnti_get, StrictAnti, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_lt_mk]

Goal state after:
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 γ
hi : Std.IdempotentOp op
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => rw [fold_empty, image_empty, fold_empty]
  | cons x xs hx ih =>
    have := Classical.decEq γ
    rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
    simp only [Function.comp_apply]

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

Goal state before:
pp: n : ℕ
p : Fin n → Bool
⊢ find? p = if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none

Tactic:
by
  split_ifs <;> grind

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
⊢ f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)

Tactic:
ext x

Goal state after:
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c

Tactic:
change _ > _ ↔ _
  apply fold_op_rel_iff_and
  intro x y z
  change _ < _ ↔ _
  exact max_lt_iff

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

Goal state before:
pp: α : 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
hp : ¬p a = true
⊢ 0 = if p a = true then 1 else 0

Tactic:
simp [hp]

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

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

Tactic:
rcases lt_or_ge m (l.drop (n % l.length)).length with hm | hm

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (s.prod * t.prod)

Tactic:
exact dvd_mul_right _ _

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₁.prod * l.prod

Tactic:
exact dvd_mul_right _ _

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

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m < l.length - n % l.length + n % l.length

Tactic:
Nat.sub_add_cancel hlt.le

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m < l.length
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
⊢ (s.dedup.bind f).dedup = (s.bind f).dedup

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ count x (s.dedup.bind f).dedup = count x (s.bind f).dedup
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ choose 0 x✝ * x✝! * (0 - x✝)! = 0!

Tactic:
simp [Nat.eq_zero_of_le_zero hk]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) ≍ cons (a ::ₘ m) a' b' (cons m a b f)

Tactic:
apply hfunext rfl
  simp only [heq_iff_eq]
  rintro a'' _ rfl
  refine hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => ?_
  rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)
  on_goal 1 => rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
  all_goals simp [*, Pi.cons_same, Pi.cons_ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #(s ×ˢ t) ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)

Tactic:
card_product

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.offDiag = #s * #s - #s

Tactic:
rw [← sq]

Goal state after:
α : Type u_1
s : Finset α
⊢ #s.offDiag = #s ^ 2 - #s
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case of_succ
n r k : ℕ
hk : k < n / 2
ih : n.choose (k + 1) ≤ n.choose (n / 2)
⊢ n.choose k ≤ n.choose (n / 2)

Tactic:
| of_succ k hk ih =>

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
a✝ : α
h : a✝ ∈ 0
⊢ Pi.empty β a✝ h ∈ t a✝

Tactic:
exact (notMem_zero _ h).elim

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b

Tactic:
by rw [h]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
h : a = 1
⊢ IsConj 1 a

Tactic:
by rw [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi

Tactic:
simp only [iInter, iInf_subtype']
  have : Nonempty { i // p i } := nonempty_subtype.2 hp
  apply InjOn.image_iInter_eq
  simpa only [iUnion, iSup_subtype'] using h

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: α : Type u_2
m : Type u_5
n : Type u_6
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
inst✝ : One α
σ : n ≃ m
i : m
x : α
⊢ mulSingle i x ∘ ⇑σ = mulSingle (σ.symm i) x

Tactic:
ext x

Goal state after:
α : Type u_2
m : Type u_5
n : Type u_6
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
inst✝ : One α
σ : n ≃ m
i : m
x✝ : α
x : n
⊢ (mulSingle i x✝ ∘ ⇑σ) x = mulSingle (σ.symm i) x✝ x
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
⊢ s ×ˢ ⋂ i, t i = ⋂ i, s ×ˢ t i

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ x ∈ s ×ˢ ⋂ i, t i ↔ x ∈ ⋂ i, s ×ˢ t i
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹

Tactic:
ext x

Goal state after:
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (s.pi t)⁻¹ ↔ x ∈ s.pi fun i ↦ (t i)⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_8
inst✝ : Monoid M
f : G →* M
⊢ f.toHomUnits.ker = f.ker

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝¹ : Group G
M : Type u_8
inst✝ : Monoid M
f : G →* M
x : G
⊢ x ∈ f.toHomUnits.ker ↔ x ∈ f.ker
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
H : Subgroup N
h : H ≤ f.range
⊢ map f (comap f H) = H

Tactic:
rwa [map_comap_eq, inf_eq_right]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
hs : s.Normal
x : G
h : x ∈ s ⊔ t ↔ ∃ y ∈ t, ∃ z ∈ s, y * z = x
x✝ : ∃ y ∈ t, ∃ z ∈ s, y * z = x
y : G
hy : y ∈ t
z : G
hz : z ∈ s
hp : y * z = x
⊢ y * z * y⁻¹ * y = x

Tactic:
simp [hp]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ (normalizer ↑H).op = normalizer ↑H.op

Tactic:
ext x

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ x ∈ (normalizer ↑H).op ↔ x ∈ normalizer ↑H.op
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
⊢ ∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a * b ∈ ⇑f '' ↑S

Tactic:
rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
    exact ⟨x * y, S.mul_mem hx hy, by rw [map_mul]⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
⊢ mker f.mrangeRestrict = mker f

Tactic:
ext x

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
x : M
⊢ x ∈ mker f.mrangeRestrict ↔ x ∈ mker f
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inl M N) = ⊥

Tactic:
ext x

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : M
⊢ x ∈ mker (inl M N) ↔ x ∈ ⊥
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inr M N) = ⊥

Tactic:
ext x

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : N
⊢ x ∈ mker (inr M N) ↔ x ∈ ⊥
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
⊢ pair (unpair n).1 (unpair n).2 = n

Tactic:
by
  dsimp only [unpair]; let s := sqrt n
  have sm : s * s + (n - s * s) = n := Nat.add_sub_cancel' (sqrt_le _)
  split_ifs with h
  · simp [s, pair, h, sm]
  · have hl : n - s * s - s ≤ s := Nat.sub_le_iff_le_add.2
      (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
    simp [s, pair, hl.not_gt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (decode (encode (rep (Quot.mk (⇑s) l)))) = some (Quot.mk (⇑s) l)

Tactic:
rw [encodek]

Goal state after:
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (some (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer ↑(closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ h ∈ normalizer ↑(closure s)
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 G
f : G ≃* N
⊢ map f.toMonoidHom (normalizer ↑H) = normalizer ↑(map f.toMonoidHom H)

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ x ∈ map f.toMonoidHom (normalizer ↑H) ↔ x ∈ normalizer ↑(map f.toMonoidHom H)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)

Tactic:
exact normalClosure_le_normal (Set.image_mono subset_normalClosure)

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
x₁ x₂ : Lex (α × β)
⊢ x₁ < x₂ ↔ x₁ ≤ x₂ ∧ ¬x₂ ≤ x₁

Tactic:
by grind [le_iff, lt_iff, lt_iff_le_not_ge]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
⊢ S = ⊥ → card ↥S = 1

Tactic:
by rintro rfl; exact card_bot

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
by
  rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx

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

Goal state after:
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
v : β
hv : v < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 * 1 ∈ {1, a}

Tactic:
rw [one_mul]; exact .inl rfl

Goal state after: