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

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

Tactic:
rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]

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

Goal state before:
pp: m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Tactic:
induction i using Nat.strong_induction_on with | _ i h

Goal state after:
case h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i
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:
rw [Fin.sub_val_of_le (one_le_of_ne_zero hi), Fin.val_one', Nat.mod_eq_of_lt
    (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))]

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

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
ha₂ : a₂ ∈ ↑s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂

Tactic:
rw [mem_coe] at ha₁ ha₂

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
b : β
hb : b ∈ t
⊢ #t ≤ #s.attach

Tactic:
card_attach

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
b : β
hb : b ∈ t
⊢ #t ≤ #s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_2.inr
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)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i < ↑j.castSucc
⊢ r (f i) (f j.succ)

Tactic:
· exact _root_.trans (ihj hij) (H j)

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

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

Tactic:
refine fun H i => Fin.induction (fun h ↦ ?_) ?_
    · simp at h
    · intro j ihj hij
      rw [← le_castSucc_iff] at hij
      obtain hij | hij := (le_def.1 hij).eq_or_lt
      · obtain rfl := Fin.ext hij
        exact H _
      · exact _root_.trans (ihj hij) (H j)

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

Goal state before:
pp: α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i ↦ f (Fin.cast ⋯ i)

Tactic:
simp_rw [Fin.cast_refl, id]

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

Goal state before:
pp: case pos
n : ℕ
p i : Fin n
hi : i ≤ p
⊢ ∃ a, p.predAbove a = i

Tactic:
exact ⟨i.castSucc, predAbove_castSucc_of_le p i hi⟩

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
j : Fin n
⊢ q j.succ ≤ cons x p j.succ ↔ tail q j ≤ p j

Tactic:
by simp [tail]

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_all [insert_subset_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ {a, b, c} ⊆ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ {a, b, c} = {a, b, c}

Tactic:
simp_all [insert_subset_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b c d : α
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
hsub : {a, b, c, d} ⊆ s
⊢ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp_all [insert_subset_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b c d : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
⊢ {a, b, c, d} ⊆ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧ {a, b, c, d} = {a, b, c, d}

Tactic:
simp_all [insert_subset_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card { x // ¬p x } = card α - card { x // p x }

Tactic:
rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
⊢ ⋯ ▸ p ((i.succAbove j).castPred ⋯) = p j

Tactic:
generalize_proofs H₁ H₂; revert H₂
    generalize hk : castPred ((succAbove i) j) H₁ = k
    rw [castPred_succAbove _ _ hlt] at hk; cases hk
    intro; rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Antisymm r
x : α
xs : List α
hx : x ∈ xs
hxs : Pairwise r xs
⊢ orderedInsert r x (xs.erase x) = xs

Tactic:
induction xs with

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
⊢ InjOn f s ↔ BijOn f s s

Tactic:
by
  refine ⟨fun h ↦ ⟨hm, h, ?_⟩, BijOn.injOn⟩
  have : Finite s := finite_coe_iff.mpr hs
  exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))

Tactic:
by
    rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List α
⊢ (map (⇑OrderDual.toDual) l).SortedLT ↔ l.SortedGT

Tactic:
grind [OrderDual.toDual_lt_toDual]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.toDual) l).SortedGT ↔ l.SortedLT

Tactic:
grind [OrderDual.toDual_lt_toDual]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))

Tactic:
haveI := decidableRel r l₁ l₂

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
Module: Mathlib.Data.List.Lex

Goal state before:
pp: 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!

Tactic:
rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h
    exact head_le_of_lt h

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l₁ l₂ l₃ : List α
h₁ : IsChain R (l₁ ++ l₂)
h₂ : IsChain R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ (l₁ ++ l₂).getLast? → ∀ (y : α), y ∈ l₃.head? → R x y

Tactic:
by
    simpa only [getLast?_append_of_ne_nil _ hn] using (isChain_append.1 h₂).2.2

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
⊢ List.Pairwise rᶜ l.reverse

Tactic:
by
  refine List.pairwise_iff_forall_infix.mpr fun l' hne hsub ↦ ?_
  have := wf.asymmetricₙ (by grind) <| h.infix <| l.reverse_reverse ▸ hsub.reverse
  simpa

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
classical simp [← h.le_dedup_iff_le, hn]

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

Goal state before:
pp: case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = [] ↔ l.rotate n = [].rotate ((([].length - n % [].length) % [].length + n % [].length) % [].length)

Tactic:
rotate_nil

Goal state after:
case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = [] ↔ l.rotate n = []
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
hk' : k = 0
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
simp_all! [k, length_reverse, ← rotate_rotate]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : ¬z = x
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = 0

Tactic:
simp [count_eq_zero, h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0

Tactic:
simp [count_eq_zero, h]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1 + 1) * (n + 1).choose 0 = (n + 1 + 1).choose (0 + 1) * (0 + 1)

Tactic:
simp [choose, mul_succ, Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s) * #(filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
← card_product,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x}) * #({x ∈ t | ¬q x})

Tactic:
← card_product,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #(filter p s ×ˢ filter q t) + #({x ∈ s | ¬p x} ×ˢ {x ∈ t | ¬q x})
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)

Tactic:
rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f (1 * y) = f 1 * f y

Tactic:
rw [one_mul, h1, one_mul]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
⊢ p = q

Tactic:
have := SetLike.ext'_iff.1 h
    rw [coe_toSubmonoid, coe_toSubmonoid] at this
    exact SetLike.ext'_iff.2 this

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ H = ⊥

Tactic:
rw [Subgroup.eq_bot_iff_forall]
  intro y hy
  rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]

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 ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → ∃ i, p i ∧ x ∈ K i

Tactic:
refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx

Goal state after:
case refine_1.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
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x✝ : G
⊢ x✝ ∈ ⋃ i, ⋃ (_ : p i), ↑(K i) → ∃ i, p i ∧ x✝ ∈ K i

case refine_1.refine_2
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
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∃ i, p i ∧ 1 ∈ K i

case refine_1.refine_3
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
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ (x y : G),
    x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) →
      y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → (∃ i, p i ∧ x ∈ K i) → (∃ i, p i ∧ y ∈ K i) → ∃ i, p i ∧ x * y ∈ K i

case refine_1.refine_4
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
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1.refine_4
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
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x✝ : G
hx✝ : x✝ ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
i : ι
hi' : p i
hi : x✝ ∈ K i
⊢ ∃ i, p i ∧ x✝⁻¹ ∈ K i

Tactic:
exact ⟨i, hi', inv_mem hi⟩

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f x = f y

Tactic:
rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]

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

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

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

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

Goal state before:
pp: case pos
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n - n.sqrt * n.sqrt, n.sqrt).1 (n - n.sqrt * n.sqrt, n.sqrt).2 = n

pp: case neg
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n

Tactic:
· simp [s, pair, h, sm]

Goal state after:
case neg
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0

Tactic:
cases b <;> dsimp [bit]

Goal state after:
case false
n : ℕ
h : n ≠ 0
⊢ ¬2 * n = 0

case true
n : ℕ
h : n ≠ 0
⊢ ¬2 * n + 1 = 0
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ 2 * n ≤ bit b n

Tactic:
cases b <;> dsimp [bit]

Goal state after:
case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n

case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ 2 * n + 1
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: x✝ : ℤ
⊢ x✝ ∈ AddSubgroup.closure {1} ↔ x✝ ∈ ⊤

Tactic:
simp [AddSubgroup.mem_closure_singleton]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ a • sᶜ = (a • s)ᶜ

Tactic:
by
  simp_rw [Set.compl_eq_univ_sdiff, smul_set_sdiff, smul_set_univ]

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

Goal state before:
pp: α : Type u_1
inst✝ : Nonempty α
a : α
n : ℕ
⊢ (ofList (List.replicate n a)).length = n

Tactic:
simp [length]

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

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

Tactic:
have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
  apply le_antisymm
  · exact map_normalClosure_le s f
  · exact normalClosure_le_normal (Set.image_mono subset_normalClosure)

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

Goal state before:

Tactic:
a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]

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✝ : CanonicallyOrderedMul M
xs : List M
x : M
h₁ : x ∈ xs
⊢ x ≤ xs.prod

Tactic:
induction xs with

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
ι : Type u_2
s✝ t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
x : α
hx : x ∈ s i
j : ι
hx' : (fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩ ∈ s j
⊢ ⟨i, ⟨x, hx⟩⟩ = ⟨j, ⟨(fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩, hx'⟩⟩

Tactic:
obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)

Goal state after:
α : Type u_1
ι : Type u_2
s✝ t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
x : α
hx : x ∈ s i
hx' : (fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩ ∈ s i
⊢ ⟨i, ⟨x, hx⟩⟩ = ⟨i, ⟨(fun x ↦ ↑x.snd) ⟨i, ⟨x, hx⟩⟩, hx'⟩⟩
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {y ∈ range ↑(ofNat s 0) | y ∈ s} = ∅

Tactic:
eq_empty_iff_forall_notMem

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (x : ℕ), x ∉ {y ∈ range ↑(ofNat s 0) | y ∈ s}
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:
rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
val✝ : Denumerable α
⊢ Nonempty (α ≃ β)

Tactic:
cases nonempty_denumerable β

Goal state after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
val✝¹ : Denumerable α
val✝ : Denumerable β
⊢ Nonempty (α ≃ β)
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
⊢ f (min a b) = f a ⊓ f b

Tactic:
obtain h | h := le_total a b
      · rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
      · rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List (α × β)
⊢ (map Prod.swap l).unzip = l.unzip.swap

Tactic:
simp only [unzip_eq_map, map_map]

Goal state after:
α : Type u
β : Type u_1
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.min' hs) = (image (⇑ofDual) s).max' ⋯

Tactic:
by
  simp [min'_eq_inf', max'_eq_sup']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.max' hs) = (image (⇑ofDual) s).min' ⋯

Tactic:
by
  simp [min'_eq_inf', max'_eq_sup']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.min' hs) = (image (⇑toDual) s).max' ⋯

Tactic:
by
  simp [min'_eq_inf', max'_eq_sup']

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.max' hs) = (image (⇑toDual) s).min' ⋯

Tactic:
by
  simp [min'_eq_inf', max'_eq_sup']

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

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

Tactic:
rcases init with - | ⟨hd', tl'⟩

Goal state after:
case mpr.nil
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
⊢ [] ++ tail = hd :: tl →
    ([], tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = ([], tail)

case mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (hd' :: tl', tail)