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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ = ⌈a⌉

Tactic:
← Int.ceil_toNat,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉.toNat = ⌈a⌉
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
⊢ R (f x) (f y)

Tactic:
· -- Now find `n` such that `l + n • a < y ≤ l + (n + 1) • a`
    rcases existsUnique_sub_zsmul_mem_Ioc ha y l with ⟨n, hny, -⟩
    rcases lt_trichotomy n 0 with hn | rfl | hn
    · -- Since `l ≤ x ≤ y`, the case `n < 0` is impossible
      refine absurd ?_ hxy.not_ge
      calc
        y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
        _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
        _ ≤ l + (0 : ℤ) • a := by gcongr; lia
        _ ≤ x := by simpa using hx.1
    · -- If `n = 0`, then `l < y ≤ l + a`, hence we can apply the assumption
      exact hf x (Ico_subset_Icc_self hx) y (by simpa using Ioc_subset_Icc_self hny) hxy
    · -- In the remaining case `0 < n` we use transitivity.
      -- If `R = (· < ·)`, then the proof looks like
      -- `f x < f (l + a) ≤ f (l + n • a) < f y`
      trans f (l + (1 : ℤ) • a)
      · grind
      have hy : R (f (l + n • a)) (f y) := by
        rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]
        refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1; simpa
      rw [← Int.add_one_le_iff, zero_add] at hn
      rcases hn.eq_or_lt with rfl | hn; · assumption
      trans f (l + n • a)
      · refine Int.rel_of_forall_rel_succ_of_lt R (f := (f <| l + · • a)) (fun k ↦ ?_) hn
        simp_rw [add_comm k 1, add_zsmul, ← add_assoc, one_zsmul, map_add_zsmul]
        refine hR (k • b) (hf _ ?_ _ ?_ ?_) <;> simpa
      · assumption

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

Goal state before:
pp: case cons
α : Type u
x hd : α
tl : List α
hl : tl.Nodup → (tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x)
h : (hd :: tl).Nodup
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
| cons hd tl hl =>

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

Goal state before:
pp: case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
· apply ih d.2 h₁ h₂ h₃

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

Goal state before:
pp: α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) ↑l
⊢ b₁ ∈ replicate (↑l).card b₂

Tactic:
rwa [map_const] at h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
simp [ha, List.dedup_cons_of_mem]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
simp [ha, List.dedup_cons_of_mem]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
simp [ha, List.dedup_cons_of_mem]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
simp [ha, List.dedup_cons_of_mem]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∪ ys = ys

Tactic:
by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset 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]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hd : α
tl : List α
hl : (tl ++ l').toFinset = tl.toFinset ∪ l'.toFinset
⊢ (hd :: tl ++ l').toFinset = (hd :: tl).toFinset ∪ l'.toFinset

Tactic:
| cons hd tl hl =>

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
i : ℕ
hi : i < n
ha : f i hi ∈ s
⊢ ∃ i_1, ∃ (hi_1 : i_1 ∈ range n), f i_1 ⋯ = f i hi

Tactic:
use i, mem_range.2 hi

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i ≤ last n

Tactic:
exact Fin.le_last i

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ a.succAbove 0 = 0

Tactic:
rw [Fin.succAbove_of_castSucc_lt]
  · exact castSucc_zero'
  · exact Fin.pos_iff_ne_zero.2 ha

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
⊢ Surjective f

Tactic:
intro x
  have := Classical.propDecidable
  cases nonempty_fintype α
  have h₁ : image f univ = univ :=
    eq_of_subset_of_card_le (subset_univ _)
      ((card_image_of_injective univ hinj).symm ▸ le_rfl)
  have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
  obtain ⟨y, h⟩ := mem_image.1 h₂
  exact ⟨y, h.2⟩

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))

Tactic:
← finSumFinEquiv.injective_comp,

Goal state after:
m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys ∘ ⇑finSumFinEquiv) ↔ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ (fun i ↦ #(g i) - 1) j ≤ (fun i ↦ #(g i) - 1) i

Tactic:
dsimp

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ #(g j) - 1 ≤ #(g i) - 1
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: case h.h
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ map f univ ⊆ s

pp: case h.h₂
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ #s ≤ #(map f univ)

Tactic:
· simp [← coe_subset, hf]

Goal state after:
case h.h₂
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range ⇑f ⊆ ↑s
⊢ #s ≤ #(map f univ)
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
⊢ i.insertNth x p (i.succAbove j) = p j

Tactic:
simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff_castSucc_lt]

Goal state after:
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
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)

Tactic:
← fold_add op,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ fold op (op b₁ b₂) (s₁ ∪ s₂ + s₁ ∩ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
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
⊢ Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
Multiset.map_cons,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
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 : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
Multiset.map_cons,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (f a ::ₘ Multiset.map f s.val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l c : List α
hr : Pairwise r c
hc : c <+ l
⊢ c <+ insertionSort r l

Tactic:
by
  induction l generalizing c with
  | nil         => grind
  | cons _ _ ih =>
    cases hc with
    | cons  _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
      exact cons_sublist_orderedInsert (ih hp h) hr

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise r (l.merge l' fun x1 x2 ↦ decide (r x1 x2))

Tactic:
by
  simpa using pairwise_merge (le := (r · ·))
    (fun a b c h₁ h₂ => by simpa using _root_.trans (by simpa using h₁) (by simpa using h₂))
    (fun a b => by simpa using Std.Total.total a b)
    l l' (by simpa using h) (by simpa using h')

Goal state after:
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 : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
← fold_add op,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁ ∪ s₂).val + Multiset.map f (s₁ ∩ s₂).val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m

Tactic:
simp_rw [← not_le, find_le_iff, not_exists, not_and]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l.tail
⊢ R (l.head ⋯) a

Tactic:
by
  grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hhead : R (l.head ⋯) (l.head ⋯)
⊢ R (l.head ⋯) a

Tactic:
by
  grind +splitIndPred

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

Goal state before:
pp: α : Type u
inst✝ : LT α
l l' : List α
⊢ l.lt l' ↔ Lex (fun x1 x2 ↦ x1 < x2) l l'

Tactic:
List.lt

Goal state after:
α : Type u
inst✝ : LT α
l l' : List α
⊢ Lex (fun x1 x2 ↦ x1 < x2) l l' ↔ Lex (fun x1 x2 ↦ x1 < x2) l 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 : List α
h : IsChain R l
⊢ IsChain R l.tail

Tactic:
by
  grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
l_ne_nil : l ≠ []
hl : IsChain R l
h : R x (l.head l_ne_nil)
⊢ IsChain R (x :: l)

Tactic:
by
  grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • s) = n • filter p s

Tactic:
refine s.induction_on ?_ ?_

Goal state after:
case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • 0) = n • filter p 0

case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
k : ℕ
⊢ (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Tactic:
by
  have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) := by
    cases l
    · simp
    · rw [length_cyclicPermutations_of_ne_nil] <;> simp
  refine ext_get this fun n hn hn' => ?_
  rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
  cases l <;> simp

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

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

Tactic:
choose_mul_factorial_mul_factorial <| Nat.le_add_left k n,

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k)!
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
val✝ : Fintype ι
⊢ (univ.pi t).Finite

Tactic:
lift t to ∀ d, Finset (κ d) using ht

Goal state after:
case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (univ.pi fun i ↦ ↑(t i)).Finite
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle k u * mulSingle l v) m = (mulSingle m u * mulSingle n v) m
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
have hn := congr_fun h n

Goal state after:
case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle k u * mulSingle l v) m = (mulSingle m u * mulSingle n v) m
hn : (mulSingle k u * mulSingle l v) n = (mulSingle m u * mulSingle n v) n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hS : S.Nonempty
hT : T.Nonempty
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
obtain ⟨s₁, h₁⟩ := hS

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hT : T.Nonempty
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t

Tactic:
image2_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ x ∈ ⋂ i, s i, ∀ y ∈ t, f x y ∈ ⋂ i, image2 f (s i) t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)

Tactic:
image2_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ y ∈ ⋂ i, t i, f x y ∈ ⋂ i, image2 f s (t i)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, image2 f (s i j) t

Tactic:
image2_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ x ∈ ⋂ i, ⋂ j, s i j, ∀ y ∈ t, f x y ∈ ⋂ i, ⋂ j, image2 f (s i j) t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, image2 f s (t i j)

Tactic:
image2_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ y ∈ ⋂ i, ⋂ j, t i j, f x y ∈ ⋂ i, ⋂ j, image2 f s (t i j)
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : ↥H
n : ℤ
⊢ ↑(x ^ n) = ↑x ^ n

Tactic:
dsimp

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
⊢ map f f.ker = ⊥

Tactic:
rw [map_eq_bot_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Tactic:
rw [codisjoint_iff, ← subgroupOf_sup, subgroupOf_self]
  exacts [le_sup_left, le_sup_right]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.op.toSubsemigroup = H.op

Tactic:
dsimp

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.toSubsemigroup = H.unop

Tactic:
dsimp

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
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ mker (f.prodMap g) = (mker f).prod (mker g)

Tactic:
← comap_bot',

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ comap (f.prodMap g) ⊥ = (mker f).prod (mker g)
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ comap (f.prodMap g) ⊥ = (mker f).prod (mker g)

Tactic:
← comap_bot',

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ comap (f.prodMap g) ⊥ = (comap f ⊥).prod (mker g)
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ comap (f.prodMap g) ⊥ = (comap f ⊥).prod (mker g)

Tactic:
← comap_bot',

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
M' : Type u_5
N' : Type u_6
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ comap (f.prodMap g) ⊥ = (comap f ⊥).prod (comap g ⊥)
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✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑(x * y), ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
simp_rw [Units.val_mul]; rfl

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

Goal state before:
pp: case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b

Tactic:
· apply Nat.add_lt_add_right; assumption

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ (fun n ↦ (decode₂ α ↑n).get ⋯) ((fun a ↦ ⟨encode a, ⋯⟩) x✝) = x✝

Tactic:
dsimp

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ (decode₂ α (encode x✝)).get ⋯ = x✝
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 : α
⊢ Quotient.mk'' <$> decode (encode (rep (Quot.mk (⇑s) l))) = some (Quot.mk (⇑s) l)

Tactic:
dsimp

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'' (decode (encode (rep (Quot.mk (⇑s) l)))) = some (Quot.mk (⇑s) l)