mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by simp_all [insert_subset_iff]

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

Goal state before:
pp: n : ℕ
α : Sort u_2
a : α
f : Fin n → α
i : Fin n
⊢ (snoc f a ∘ castSucc) i = f i

Tactic:
by rw [Function.comp_apply, snoc_castSucc]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.8
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Trunc (α ≃ Fin (card α))

Tactic:
unfold card Finset.card

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.8
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Trunc (α ≃ Fin univ.val.card)
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.6
inst✝ : Fintype α
⊢ Trunc { f // Bijective f }

Tactic:
unfold card Finset.card

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.6
inst✝ : Fintype α
⊢ Trunc { f // Bijective f }
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
⊢ (if h : j.castSucc < i then ⋯ ▸ p ((i.succAbove j).castPred ⋯) else ⋯ ▸ p ((i.succAbove j).pred ⋯)) = p j

Tactic:
split_ifs with hlt

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

case neg
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).pred ⋯) = p j
Module: Mathlib.Data.List.Sort

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

Tactic:
induction xs <;> grind

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ orderedInsert r x xs

Tactic:
induction xs <;> grind

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

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
refine ⟨u, fun n ↦ ?_⟩

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ P (u n) (u '' Iio n)
Module: Mathlib.Data.List.Sort

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

Tactic:
exact ih hr h |>.trans (sublist_orderedInsert ..)

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:
rw [Fin.natAdd_lt_natAdd_iff] at hi
    exact Fin.find_min hⱼ hi

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

Goal state before:
pp: case succ
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ n • s ∨ a ∈ s
⊢ a ∈ s

Tactic:
exact h.elim ih id

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length

Tactic:
length_drop,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ l.length - n % l'.length = (drop (n % l'.length) l').length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ l.length - n % l'.length = (drop (n % l'.length) l').length

Tactic:
length_drop,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
⊢ l.length - n % l'.length = l'.length - n % l'.length
Module: Mathlib.Data.List.Rotate

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

Tactic:
length_drop,

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < l.length - n % l.length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?
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 < (drop (n % l.length) l).length + n % l.length

Tactic:
length_drop,

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 - n % l.length + n % l.length
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:
by
  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.Fintype.Pi

Goal state before:
pp: α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ (univ.pi fun a ↦ univ) = univ

Tactic:
by
  ext; simp

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

Goal state before:
pp: case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (univ.pi fun i ↦ ↑(t i)).Finite

Tactic:
rw [← Fintype.coe_piFinset]
    apply Finset.finite_toSet

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
M : Type ?u.7
N : Type ?u.9
inst✝³ : Monoid M
inst✝² : MulOneClass N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ (x * y) • 1 = x • 1 * y • 1

Tactic:
smul_one_mul,

Goal state after:
M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
M : Type ?u.7
N : Type ?u.9
inst✝³ : Monoid M
inst✝² : MulOneClass N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ (x * y) • 1 = x • y • 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ f ⁻¹' ⋂ i, s i = ⋂ i, f ⁻¹' s i

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t

Tactic:
by
  rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]
  simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a * x) '' t = (fun x ↦ a⁻¹ * x) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a⁻¹ * x) ((fun x ↦ a * x) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a * x) ((fun x ↦ a⁻¹ * x) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x * b) '' t = (fun x ↦ x * b⁻¹) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b⁻¹) ((fun x ↦ x * b) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x * b⁻¹) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a / x) '' t = (fun x ↦ x⁻¹ * a) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ x⁻¹ * a) ((fun x ↦ a / x) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a c : α
⊢ (fun x ↦ a / x) ((fun x ↦ x⁻¹ * a) c) = c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x / b) '' t = (fun x ↦ x * b) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x / b) c) = c

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x / b) ((fun x ↦ x * b) c) = c
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a.mem
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x : M
hx : x ∈ s
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
exact Or.inr <| Subsemigroup.subset_closure hx

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ S

Tactic:
simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Nontrivial ↥H
⊢ ∃ x ∈ H, x ≠ 1

Tactic:
← Subgroup.nontrivial_iff_exists_ne_one

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Nontrivial ↥H
⊢ Nontrivial ↥H
Module: Mathlib.Algebra.Group.Subgroup.Map

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
H : Type u_5
inst✝ : Group H
f : G ≃* H
sg : Subgroup H
⊢ Subgroup.comap (↑f.symm) (Subgroup.comap (↑f) sg) = sg

Tactic:
by simp [Subgroup.comap_comap]

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

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
H : Type u_5
inst✝ : Group H
f : G ≃* H
sh : Subgroup G
⊢ Subgroup.comap (↑f) (Subgroup.comap (↑f.symm) sh) = sh

Tactic:
by simp [Subgroup.comap_comap]

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

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

Tactic:
rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid N
x : M × N
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (MonoidHom.snd M N) s

Tactic:
by simp [mem_prod, MonoidHom.coe_snd]

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

Goal state before:
pp: case succ.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && n.bodd ^^ false) = (false && !n.bodd)

Tactic:
cases bodd n

Goal state after:
case succ.false.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && false ^^ false) = (false && !false)

case succ.false.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (false && true ^^ false) = (false && !true)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && n.bodd ^^ true) = (true && !n.bodd)

Tactic:
cases bodd n

Goal state after:
case succ.true.false
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && false ^^ true) = (true && !false)

case succ.true.true
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (true && true ^^ true) = (true && !true)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ unpair (pair a b) = (a, b)

Tactic:
dsimp only [pair]; split_ifs with h
  · show unpair (b * b + a) = (a, b)
    have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
    simp [unpair, be, Nat.add_sub_cancel_left, h]
  · show unpair (a * a + a + b) = (a, b)
    have ae : sqrt (a * a + (a + b)) = a := by
      rw [sqrt_add_eq]
      exact Nat.add_le_add_left (le_of_not_gt h) _
    simp [unpair, ae, Nat.add_assoc, Nat.add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ decode (encode x) = some y

Tactic:
e,

Goal state after:
α : Type u_1
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ decode (encode y) = some y
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
⊢ (decode₂ α ↑n).isSome = true

Tactic:
obtain ⟨x, hx⟩ := n.2

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (decode₂ α ↑n).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match n.bodd, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none

Tactic:
cases bodd n

Goal state after:
case false
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match false, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none

case true
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match true, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m)) =
    none
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 N
x : G × N
⊢ x ∈ ⊤.prod H ↔ x ∈ comap (MonoidHom.snd G N) H

Tactic:
by simp [mem_prod, MonoidHom.coe_snd]

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

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

Tactic:
rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]

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

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
simp_rw [← hh]

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩
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
⊢ x * y = y * x

Tactic:
mul_eq_one_iff_eq_inv

Goal state after:
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⁻¹)⁻¹
⊢ x * y = y * x
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (s.disjSum t).card = s.card + t.card

Tactic:
rw [disjSum, card_add, card_map, card_map]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match n.bodd, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit n.bodd n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match n.bodd, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit n.bodd n.div2

Tactic:
cases bodd n

Goal state after:
case false
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit false n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit false n.div2

case true
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit true n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit true n.div2
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).sup = a ⊔ s.sup

Tactic:
by
  rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]; simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
set t : List s :=
      ((List.range x).filter fun y => y ∈ s).pmap
        (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
        (by intro a ha; simpa using! (List.mem_filter.mp ha).2) with ht

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
⊢ ∃ a, ofNat s a = ⟨x, hx⟩
Module: Mathlib.Data.Finset.Max

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

Tactic:
rw [min_eq_inf_withTop, inf_image]
  exact congr_fun WithTop.map_id _

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).min

Tactic:
rw [min_eq_inf_withTop, inf_image]
  exact congr_fun WithTop.map_id _

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')

Tactic:
refine
      ⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩ <;>
    simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff] <;>
    intro i' hi' j' hj'
  · exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)
  · exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ x ∈ (powersetCard n.succ u).biUnion id

Tactic:
simp only [mem_biUnion, id]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
a₁✝ a₂✝ : WithBot α
a₁ a₂ : α
h₁ : WithBot.recBotCoe True p ↑a₁
h₂ : WithBot.recBotCoe True p ↑a₂
⊢ WithBot.recBotCoe True p (↑a₁ ⊔ ↑a₂)

Tactic:
exact hp a₁ h₁ a₂ h₂

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

Goal state before:
pp: case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : ∀ i ∈ insert a✝¹ s✝, Monotone (f i)
⊢ ⨆ j, ⨅ i ∈ insert a✝¹ s✝, f i j = ⨅ i ∈ insert a✝¹ s✝, ⨆ j, f i j

Tactic:
| insert _ _ ihs =>

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
refine eq_of_forall_ge_iff fun c ↦ ?_

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
⊢ ⨆ p, f p ≤ c ↔ ⨆ b, ⨆ c, f (b, c) ≤ c
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type u
ι : Type v
κ✝ : ι → Sort w
inst✝² : Nonempty ((a : ι) → κ✝ a)
inst✝¹ : Order.Frame α
s : Set ι
hs : s.Finite
f✝ : (a : ι) → κ✝ a → α
κ : ι → Type w
inst✝ : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
this : Finite ↑s
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
have : Nonempty (Π a : { a // a ∉ s }, κ ↑a) := ‹Nonempty (Π a, κ a)›.map fun f a ↦ f a

Goal state after:
α : Type u
ι : Type v
κ✝ : ι → Sort w
inst✝² : Nonempty ((a : ι) → κ✝ a)
inst✝¹ : Order.Frame α
s : Set ι
hs : s.Finite
f✝ : (a : ι) → κ✝ a → α
κ : ι → Type w
inst✝ : Nonempty ((a : ι) → κ a)
f : (a : ι) → κ a → α
this✝ : Finite ↑s
this : Nonempty ((a : { a // a ∉ s }) → κ ↑a)
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
x✝ : a ⋖ c ∧ c ⋖ b
hac : a ⋖ c
hcb : c ⋖ b
⊢ {c} ∪ {c} = {c}

Tactic:
union_self

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
x✝ : a ⋖ c ∧ c ⋖ b
hac : a ⋖ c
hcb : c ⋖ b
⊢ {c} = {c}