mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round (↑⌊x⌋ + fract x) = (⌊2 * (↑⌊x⌋ + fract x)⌋ + 1) / 2

Tactic:
round,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if 2 * fract (↑⌊x⌋ + fract x) < 1 then ⌊↑⌊x⌋ + fract x⌋ else ⌈↑⌊x⌋ + fract x⌉) = (⌊2 * (↑⌊x⌋ + fract x)⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑y) = round x + y

Tactic:
round,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract (x + ↑y) < 1 then ⌊x + ↑y⌋ else ⌈x + ↑y⌉) = round x + y
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract (x + ↑y) < 1 then ⌊x + ↑y⌋ else ⌈x + ↑y⌉) = round x + y

Tactic:
round,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract (x + ↑y) < 1 then ⌊x + ↑y⌋ else ⌈x + ↑y⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| = min (fract x) (1 - fract x)

Tactic:
round,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉)| = min (fract x) (1 - fract x)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋

Tactic:
refine mul_lt_floor ?_ ?_ ?_ <;> norm_num

Goal state after:
case refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 1 ≤ a
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.erase a < s

Tactic:
simpa [h] using lt_cons_self (s.erase a) a

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

Goal state before:
pp: α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
⊢ filter (fun _a ↦ p) s = if p then s else ∅

Tactic:
split_ifs <;> simp [*]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
split_ifs <;> simp [*]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
split_ifs <;> simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ insert x {x}ᶜ = univ

Tactic:
← compl_erase,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ ({x}.erase x)ᶜ = univ
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]

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
← val_castSucc

Goal state after:
n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩).castSucc = ↑i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ a.pred h₁ < a.castPred h₂

Tactic:
by
  rw [pred_lt_castPred_iff, le_def]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t

Tactic:
simp [disjoint_iff_inter_eq_empty]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = p 0

Tactic:
← cons_succ x p

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = cons x p (succ 0)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = p (last n)

Tactic:
← cons_succ x p

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = cons x p (last n).succ
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Subsingleton ↥s ↔ Subsingleton ↑↑s

Tactic:
coe_sort_coe

Goal state after:
α : Type u_1
s : Finset α
⊢ Subsingleton ↥s ↔ Subsingleton ↥s
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = #s

Tactic:
← subtype_card s H

Goal state after:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ append x₀ x i = (cons (x₀ 0) x ∘ Fin.cast ⋯) i

Tactic:
refine Fin.addCases ?_ ?_ i

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l

Tactic:
· exact h.mem

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

Goal state before:
pp: P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst✝ : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α

Tactic:
induction n using Nat.strong_induction_on generalizing α with | _ n ih
   =>  _ 

Goal state after:
case h
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
⊢ P α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ append x x₀ i = snoc x (x₀ 0) i

Tactic:
refine Fin.addCases ?_ ?_ i

Goal state after:
case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin (n + 1)
⊢ ∀ (i : Fin 1), append x x₀ (natAdd n i) = snoc x (x₀ 0) (natAdd n i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
⊢ append as (snoc bs b) = snoc (append as bs) b

Tactic:
funext i
  rcases i with ⟨i, isLt⟩
  simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1,
    eq_rec_constant, Nat.add_eq]
  split_ifs with lt_n lt_add sub_lt nlt_add lt_add <;> (try rfl)
  · have := Nat.lt_add_right m lt_n
    contradiction
  · obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt
    simp [Nat.add_comm n m] at sub_lt
  · have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add
    contradiction

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
by classical exact (truncOfCardLE h).nonempty

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

Goal state before:
pp: α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.head hl ≠ []
⊢ (l.head hl).head hl' = l.flatten.head ⋯

Tactic:
by
  cases l with grind

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

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : p 0
⊢ Fin.find p h = 0

Tactic:
grind [find_eq_zero]

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

Goal state before:
pp: case inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

pp: case inr.inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k = ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

pp: case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
· rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]
    · rwa [Fin.lt_def]

Goal state after:
case inr.inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k = ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : M
⊢ a * {b}.prod = a * b

Tactic:
prod_singleton

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
a b : M
⊢ a * b = a * b
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case neg
α : 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
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
· exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ IsChain (fun x1 x2 ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a

Tactic:
induction l using twoStepInduction with
  | nil => simp
  | singleton => simp
  | cons_cons a b l IH IH2 =>
    simp +contextual [isChain_cons_cons, eq_comm, IH2, replicate_succ]

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

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

Tactic:
Nat.zero_add,

Goal state after:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ l[n % l.length]? = l[n]?
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ m.bind f ≍ m.bind f'

Tactic:
simp only [heq_eq_eq] at hf

Goal state after:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → Multiset β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ m.bind f ≍ m.bind f'
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.offDiag.Nodup
⊢ l.Nodup

Tactic:
by
  let := Classical.decEq α
  simp only [nodup_iff_count_le_one, Prod.forall, count_offDiag_eq_mul_sub_ite] at *
  intro a
  specialize h a a
  contrapose h
  rw [Nat.not_le] at h
  suffices 1 + l.count a < l.count a * l.count a by simpa
  calc
    1 + l.count a < l.count a + l.count a := by simpa
    _ ≤ l.count a * l.count a := by
      rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h

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

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
set p := m - 1

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
← ascFactorial_eq_factorial_mul_choose

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r

Tactic:
← Nat.lt_iff_add_one_le,

Goal state after:
r n : ℕ
h : r < n / 2
⊢ r < n - r
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (s ×ˢ t).Finite

Tactic:
have := ht.to_subtype

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (s ×ˢ t).Finite
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this : Finite ↑s
⊢ (image2 f s t).Finite

Tactic:
have := ht.to_subtype

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this✝ : Finite ↑s
this : Finite ↑t
⊢ (image2 f s t).Finite
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
p q : Subsemigroup M
h : p.carrier = q.carrier
⊢ p = q

Tactic:
cases p

Goal state after:
case mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
q : Subsemigroup M
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝ } = q
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
inhabit ι
  refine Subset.antisymm (image_iInter_subset s f) fun y hy => ?_
  simp only [mem_iInter, mem_image] at hy
  choose x hx hy using hy
  refine ⟨x default, mem_iInter.2 fun i => ?_, hy _⟩
  suffices x default = x i by
    rw [this]
    apply hx
  replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
  apply h (hx _) (hx _)
  simp only [hy]

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

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ x = y

Tactic:
by
    refine mul_inv_eq_one.1 <| h _ (mul_mem ?_ (inv_mem ?_)) ?_ <;> simp_all

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i

Tactic:
refine ⟨?_, fun ⟨i, hi', hi⟩ ↦ ?_⟩
  · suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
      simpa only [closure_iUnion, closure_eq (K _)] using this
    refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
    · simp
    · exact ⟨i, hp, (K i).one_mem⟩
    · rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩
      rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
      exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩
    · rintro _ _ ⟨i, hi', hi⟩
      exact ⟨i, hi', inv_mem hi⟩
  · apply le_iSup (fun i ↦ ⨆ (_ : p i), K i) i
    simp [hi, hi']

Goal state after:
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 G
h : f.ker ≤ H
⊢ H ⊔ f.ker = H

Tactic:
sup_eq_left

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
h : f.ker ≤ H
⊢ f.ker ≤ H
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 K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ f.range ⊓ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)

Tactic:
inf_eq_right.mpr hH,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
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 : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
h : S ≤ MonoidHom.mrange f
⊢ map f (comap f S) = S

Tactic:
by
  simpa only [inf_of_le_left h] using map_comap_eq f S

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

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

Tactic:
cases a <;> dsimp [bit] <;> lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = (⋃ n, s n) ×ˢ ⋃ n, t n

Tactic:
rw [← Set.iUnion_prod]

Goal state after:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = ⋃ x, s x.1 ×ˢ t x.2
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
H K : Subgroup G
inst✝¹ : H.Characteristic
inst✝ : K.Characteristic
⊢ (H ⊔ K).Characteristic

Tactic:
simp_all [characteristic_iff_map_eq, map_sup]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ f (e * e) = f e

Tactic:
he.eq

Goal state after:
M : Type u_4
N : Type u_5
F : Type u_6
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M
he : IsIdempotentElem e
f : F
⊢ f e = f e
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ max (map f l).prod (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
rw [max_le_iff]

Goal state after:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod ∧ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, S i
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ motive x

Tactic:
by
  rw [iSup_eq_closure] at hx
  refine closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
  exact mem _ _ hi

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

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
⊢ ∀ (y : N) (z : α), (1 • y) • z = 1 • y • z

Tactic:
intro y z

Goal state after:
case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
y : N
z : α
⊢ (1 • y) • z = 1 • y • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
⊢ ∀ (n : N) (a : α), 1 • n • a = n • 1 • a

Tactic:
intro y z

Goal state after:
case refine_1
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
y : N
z : α
⊢ 1 • y • z = y • 1 • z
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
⊢ ∀ (m : α), m ∈ foldl (argAux r) (some a✝) (l✝ ++ [a✝²]) → m ∈ a✝ :: (l✝ ++ [a✝²])

Tactic:
simp only [foldl_append, foldl_cons, foldl_nil, argAux]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) (foldl (argAux r) (some a✝) l✝) →
      m ∈ a✝ :: (l✝ ++ [a✝²])
Module: Mathlib.Data.List.MinMax

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

Tactic:
cases not_le_of_gt ‹_› ‹_›

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
  by_contra h
  have (a : ℕ) (ha : a ∈ s) : a < x + 1 :=
    lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]⟩
  classical
  exact Fintype.false
    ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
      (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy) (by simp [-Multiset.range_succ])).toFinset,
      by simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ] ⟩

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ toFunAux (ofNat s 0) = 0

Tactic:
by
    rw [toFunAux_eq, card_eq_zero, eq_empty_iff_forall_notMem]
    rintro n hn
    rw [mem_filter, ofNat, mem_range] at hn
    exact bot_le.not_gt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ l.maximum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
m : α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → idxOf m l ≤ idxOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ (⇑f ⊔ ⇑g) ⊤ = ⊤

Tactic:
by rw [Pi.sup_apply, map_top, map_top, sup_top_eq]

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]
  rfl

Goal state after: