mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ IsNNRat (fract (↑n * ⅟↑d)) (n % d) d

Tactic:
refine ⟨inv, ?_⟩

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ fract (↑n * ⅟↑d) = ↑(n % d) * ⅟↑d
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ IsRat (fract (↑(negOfNat n) * ⅟↑d)) (-↑n % ↑d) d

Tactic:
refine ⟨inv, ?_⟩

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ fract (↑(negOfNat n) * ⅟↑d) = ↑(-↑n % ↑d) * ⅟↑d
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 b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + 1 = a + (b - 1) * (b - 1)⁻¹

Tactic:
rw [mul_inv_cancel₀]

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a b : R
⊢ Int.cast ⁻¹' Ico a b = Ico ⌈a⌉ ⌈b⌉

Tactic:
by
  ext
  simp [ceil_le, lt_ceil]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x✝ : Archimedean K
x : K
n : ℕ
h : x < ↑n
⊢ x < ↑↑n

Tactic:
rwa [Rat.cast_natCast]

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

Goal state before:
pp: case inr.inr
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)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (f x) (f y)

Tactic:
· -- 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.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
x✝ : ↑(Ico 0 1) → G
x : ↑(Ico 0 1)
⊢ (fun f x ↦ f ↑x) ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x✝) x = x✝ x

Tactic:
simp [Int.fract_eq_self.2 x.2, Int.floor_eq_zero_iff.2 x.2]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
⊢ ∀ (x : WithBot M) {y : WithBot M}, 0 < y → ∃ n, x ≤ n • y

Tactic:
intro x y hxy

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x y : WithBot M
hxy : 0 < y
⊢ ∃ n, x ≤ n • y
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
⊢ ∀ (x : WithZero M) {y : WithZero M}, 1 < y → ∃ n, x ≤ y ^ n

Tactic:
intro x y hxy

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
x y : WithZero M
hxy : 1 < y
⊢ ∃ n, x ≤ y ^ n
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ l <+~ [a] ↔ l = [] ∨ l = [a]

Tactic:
by
  constructor
  · rw [subperm_iff]
    rintro ⟨s, hla, h⟩
    rwa [perm_singleton.mp hla, sublist_singleton] at h
  · rintro (rfl | rfl)
    exacts [nil_subperm, Subperm.refl _]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ • p₁ /ₛ v₂ • p₂ = v₁ / v₂ * (p₁ /ₛ p₂)

Tactic:
by
  rw [sdiv_smul_eq_sdiv_div, smul_sdiv_assoc, mul_div_assoc, ← mul_comm_div]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ count a (l₁.diff (b :: l₂)) = count a l₁ - count a (b :: l₂)

Tactic:
by
    simp only [diff_cons, count_diff, count_erase, beq_iff_eq, Nat.sub_right_comm, count_cons,
      Nat.sub_add_eq]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
⊢ ∀ (a : Multiset α), a = 0

Tactic:
by rintro ⟨_ | ⟨a, l⟩⟩; exacts [rfl, isEmptyElim a]

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ ↑l = ↑[a] ↔ l = [a]

Tactic:
coe_eq_coe,

Goal state after:
α : Type u_1
l : List α
a : α
⊢ l ~ [a] ↔ l = [a]
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (some '' {x | x ∈ l})

Tactic:
by
  rw [← range_list_get, ← range_comp]
  refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)
  · exact (le_or_gt l.length n).imp getElem?_eq_none_iff.mpr
      (fun hlt => ⟨⟨_, hlt⟩, (getElem?_eq_getElem hlt).symm⟩)
  · exact ⟨_, getElem?_eq_none_iff.mpr le_rfl⟩
  · exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩

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

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
⊢ ↑m.toList = ↑[a] ↔ m = {a}

Tactic:
coe_toList,

Goal state after:
α : Type u_1
a : α
m : Multiset α
⊢ m = ↑[a] ↔ m = {a}
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
simp only [h, if_true]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
⊢ count (f x) (map f s) = count x s

Tactic:
by
  by_cases H : x ∈ s
  · exact count_map_eq_count f _ hf.injOn _ H
  · rw [count_eq_zero_of_notMem H, count_eq_zero, mem_map]
    rintro ⟨k, hks, hkx⟩
    rw [hf hkx] at hks
    contradiction

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
obtain h | h := (rev i).succ_le_or_le_castSucc p
  · rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]
  · rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]

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

Goal state before:
pp: m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h : m = n
⊢ Fin.cast h ⊤ = ⊤

Tactic:
simp [← val_inj, h]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
i : Fin n
hi : f i.castSucc = f i.succ
this : i.castSucc = i.succ
⊢ False

Tactic:
simp [Fin.ext_iff] at this

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

Goal state before:
pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
by_cases h1 : 1 ≠ i ∧ 1 ≠ j

Goal state after:
case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ succ 0 = 1

Tactic:
cases n
  · exact (NeZero.ne 0 rfl).elim
  · rfl

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ succ 1 = 2

Tactic:
cases n
  · exact (NeZero.ne 0 rfl).elim
  · rfl

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨↑i + 1, ⋯⟩

Tactic:
split_ifs with h
  exacts [Fin.ext (congr_arg Fin.val h :), rfl]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ b ≤ a.castSucc.pred ha ↔ b < a

Tactic:
le_pred_iff,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ b.succ ≤ a.castSucc ↔ b < a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ a.castPred ha ≤ b.pred hb ↔ a < b

Tactic:
le_pred_iff,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ (a.castPred ha).succ ≤ b ↔ a < b
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
simp_rw [ofFn_succ', succ_mul]
    simp [ofFn_add, IH]
    rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
⊢ #∅ ≤ 1 ↔ ∀ a ∈ ∅, ∀ b ∈ ∅, a = b

case inr
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
⊢ ∃ x, s ⊆ {x}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Goal state after:
case refine_1.inl
α : Type u_1
inst✝ : Nonempty α
H : #∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}

case refine_1.inr
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
· rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
      succAbove_pred_of_lt _ _ h]

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

Goal state before:
pp: case mpr
α : 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
⊢ ∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}

Tactic:
exact ⟨a, b, c, d, {a, b, c, d}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
inst✝ : DecidableEq α
⊢ x ∈+ l ↔ 2 ≤ count x l

Tactic:
by
  simp [replicate_succ, duplicate_iff_sublist, ← replicate_sublist_iff]

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

Goal state before:
pp: case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ cons a (snoc q b) j.castSucc.succ = snoc (cons a q) b j.castSucc.succ

Tactic:
rw [cons_succ]
      simp [← castSucc_succ]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
L : List α
a : α
⊢ (orderedInsert r a L).length = L.length + 1

Tactic:
by
  induction L <;> grind

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

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
have : Nonempty γ := (h ∅ finite_empty).nonempty

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
this : Nonempty γ
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
as bs : List α
x : α
hs : as <+ bs
hb : Pairwise r bs
⊢ orderedInsert r x as <+ orderedInsert r x bs

Tactic:
by
  cases as with
  | nil => simp
  | cons a as =>
    cases bs with
    | nil => contradiction
    | cons b bs =>
      unfold orderedInsert
      cases hs <;> split_ifs with hr
      · exact .cons_cons _ <| .cons _ ‹a :: as <+ bs›
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        simp only [hr, orderedInsert_cons, ite_true] at ih
        exact .trans ih <| .cons _ (.refl _)
      · have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
        exact absurd (trans_of _ ‹r x b› hba) hr
      · have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        rw [orderedInsert_cons, if_neg hr] at ih
        exact .cons _ ih
      · simp_all
      · exact .cons_cons _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons

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.dropLast
⊢ R a (l.getLast ⋯)

Tactic:
← pairwise_reverse

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
h : l' < l
hl' : l' ≠ []
⊢ l'.head! ≤ l.head!

Tactic:
replace h : List.Lex (· < ·) l' l := h

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
⊢ R x y

Tactic:
rw [← cons_head?_tail hy] at h
  exact h.rel

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
ha : IsChain (fun x1 x2 ↦ x1 > x2) [a]
hmas : b :: bs < []
⊢ a > b

Tactic:
exact (List.not_lt_nil _ hmas).elim

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

Goal state before:
pp: α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = ↑(List.flatMap f l)

Tactic:
by
  rw [List.flatMap, ← coe_join, List.map_map]
  rfl

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

Goal state before:
pp: case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
hk₁

Goal state after:
case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (insert a s).pi t = (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)

Tactic:
apply eq_of_veq

Goal state after:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val = ((t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)).val
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Tactic:
by
  rcases s with ⟨⟨s⟩, hs⟩
  exact hs.mem_offDiag

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

Goal state before:
pp: α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #(s.piDiag ι) = #s

Tactic:
piDiag,

Goal state after:
α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #(image (const ι) s) = #s
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
⊢ #u = (#s).choose 2

Tactic:
have union : u.disjUnion v disj = s.offDiag := by grind

Goal state after:
α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
union : u.disjUnion v disj = s.offDiag
⊢ #u = (#s).choose 2
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: S : Type u_3
M : Type u_4
inst✝² : SetLike S M
inst✝¹ : Mul M
inst✝ : MulMemClass S M
s : S
⊢ IsMulCommutative ↥s ↔ ∀ (a : M), a ∈ s → ∀ (b : M), b ∈ s → a * b = b * a

Tactic:
by
  simp [isMulCommutative_iff]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : α
ha : m a ∈ s
b : α
hb : m b ∈ t
⊢ (fun x1 x2 ↦ x1 * x2) (m a) (m b) ∈ range ⇑m

Tactic:
exact ⟨a * b, map_mul ..⟩

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 b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S

Tactic:
rw [hb, ha]

Goal state after:
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ a * (b * n * b⁻¹) * a⁻¹ ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
S : ι → Subgroup G
x : G
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
⊢ Injective fun g ↦ ↑g.1 * ↑g.2

Tactic:
intro x y hxy

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) y
⊢ x = y
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 : s.prod t ≤ u
⊢ map (inl M N) s ≤ u

Tactic:
rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, Submonoid.one_mem _⟩

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'
⊢ comap (f.prodMap g) ⊥ = (comap f ⊥).prod (comap g ⊥)

Tactic:
← prod_map_comap_prod',

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.prodMap g) (⊥.prod ⊥)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer ↑(comap f H) ≤ comap f (normalizer ↑H)

Tactic:
rw [← map_le_iff_le_comap]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ map f (normalizer ↑(comap f H)) ≤ normalizer ↑H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s : Set α
a b : α
⊢ s * {a, b} = s <• a ∪ s <• b

Tactic:
by
  rw [insert_eq, mul_union, mul_singleton, mul_singleton]; rfl

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
⊢ ofNat β n = e.symm (ofNat α n)

Tactic:
by
  let := ofEquiv _ e
  refine ofNat_of_decode ?_
  rw [decode_ofEquiv e]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
d : α
⊢ l.max?.getD d = WithBot.unbotD d l.maximum

Tactic:
by
  cases hy : l.maximum with
  | bot => simp [List.maximum_eq_bot.mp hy]
  | coe y =>
    rw [List.maximum_eq_coe_iff] at hy
    simp only [WithBot.unbotD_coe]
    cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

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

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i ↦ ⨆ (_ : i ∈ s), f i)

pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i

Tactic:
· classical
      refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
      intro
      simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind

Goal state after:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i