mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b

pp: case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s

Tactic:
· rw [← Icc_sdiff_right]
      exact subset_sdiff_singleton hc hb

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ↪o β
⊢ range ⇑f = range ⇑g ↔ f = g

Tactic:
rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]

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

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
h : BddAbove (range fun x ↦ f x ⊔ g x)
b : α
hb : b ∈ upperBounds (range fun x ↦ f x ⊔ g x)
⊢ BddAbove (range g)

Tactic:
exact ⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_right.trans (hb ⟨i, rfl⟩)⟩

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : b * (↑k * c) = 1
⊢ Invertible b

Tactic:
Nat.cast_commute k

Goal state after:
α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : b * (c * ↑k) = 1
⊢ Invertible b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
hb : b ≤ b + b
⊢ IsBot 0

Tactic:
le_add_iff_nonneg_right

Goal state after:
case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
hb : 0 ≤ b
⊢ IsBot 0
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
u : List β
⊢ Forall₂ (fun a b ↦ p a ∧ R a b) [] u ↔ (∀ (a : α), a ∈ [] → p a) ∧ Forall₂ R [] u

Tactic:
by
    simp only [forall₂_nil_left_iff, forall_prop_of_false not_mem_nil, imp_true_iff, true_and]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
· rintro ⟨l1, h1, h2⟩
    use l1.map f
    simp [h1, h2.map]

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
hlu : l ~ u
huv : Forall₂ r u v
⊢ (Forall₂ r ∘r Perm) l v

Tactic:
induction hlu generalizing v with

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

Goal state before:
pp: case mp
α : Type u
h : Injective length
⊢ Subsingleton α

Tactic:
refine ⟨fun x y => ?_⟩

Goal state after:
case mp
α : Type u
h : Injective length
x y : α
⊢ x = y
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a : α
⊢ count a l = count a (filter (fun b ↦ decide (P b)) l) + count a (filter (fun x ↦ decide ¬P x) l)

Tactic:
unfold count

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a : α
⊢ countP (fun x ↦ x == a) l =
    countP (fun x ↦ x == a) (filter (fun b ↦ decide (P b)) l) + countP (fun x ↦ x == a) (filter (fun x ↦ decide ¬P x) l)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

pp: case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

pp: case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

Tactic:
· cases hl

Goal state after:
case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

pp: case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝

Tactic:
· cases hl

Goal state after:
case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : L ≠ 0
⊢ (e₁ = e₂) = (f₁ = f₂)

Tactic:
subst H₁ H₂

Goal state after:
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
f₁ f₂ L : M
HL : L ≠ 0
⊢ (L * f₁ = L * f₂) = (f₁ = f₂)
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulMono M
inst✝ : PosMulReflectLE M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ ≤ e₂) = (f₁ ≤ f₂)

Tactic:
subst H₁ H₂

Goal state after:
M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulMono M
inst✝ : PosMulReflectLE M
f₁ f₂ L : M
HL : 0 < L
⊢ (L * f₁ ≤ L * f₂) = (f₁ ≤ f₂)
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulStrictMono M
inst✝ : PosMulReflectLT M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ < e₂) = (f₁ < f₂)

Tactic:
subst H₁ H₂

Goal state after:
M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulStrictMono M
inst✝ : PosMulReflectLT M
f₁ f₂ L : M
HL : 0 < L
⊢ (L * f₁ < L * f₂) = (f₁ < f₂)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
⊢ idxOf (l.getLast hl) l < l.length - 1

Tactic:
← Nat.not_le

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
⊢ ¬l.length - 1 ≤ idxOf (l.getLast hl) l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) * (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
rw [ih]

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x ↦ if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * (map (fun x ↦ if x = a then f x else g x) xs).prod =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
rw [ih]

Goal state after:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x ↦ if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ ↑(↑n + 1) * q = n • q + q

Tactic:
Rat.intCast_add,

Goal state after:
q✝ a b c : ℚ
n : ℕ
q : ℚ
⊢ (↑↑n + ↑1) * q = n • q + q
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Prop
x : α
l : List α
⊢ Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1

Tactic:
rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]

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

Goal state before:
pp: a b s x : ℕ
hx : x ∈ range' a b s
⊢ a ≤ x

Tactic:
obtain ⟨i, _, rfl⟩ := List.mem_range'.mp hx
  exact le_add_right a (s * i)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a

Tactic:
by
    rw [h]
    exact ⟨0, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b

Tactic:
by
  rcases hu with ⟨u, rfl⟩
  apply Units.mul_left_dvd

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * b * a = b

Tactic:
h.inv_mul_cancel

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ b = b
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)

Tactic:
apply mul_eq_mul_left_iff.2

Goal state after:
q r : ℚ
s : ℚ := ⋯
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den ∨
    c = 0
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a c₁ c₂ : R
b₁ b₂ : ℕ
d : R
x✝² : a ^ b₁ = c₁
x✝¹ : a ^ b₂ = c₂
x✝ : c₁ * c₂ = d
⊢ a ^ (b₁ + b₂) = d

Tactic:
by
  subst_vars; simp [_root_.pow_add]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = (⨆ x ∈ {0}, u x) ⊔ ⨆ x ∈ range Nat.succ, u x

Tactic:
iSup_singleton,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
by
  simp_rw [isLUB_iff_le_iff, mem_upperBounds] at ha₀ hb₀
  simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Ici (⨆ i, f i) ↔ x✝ ∈ ⋂ i, Ici (f i)

Tactic:
by simp only [mem_Ici, iSup_le_iff, mem_iInter]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
a : α
s : Set α
⊢ Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a

Tactic:
by
  simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]

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

Goal state before:
pp: case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
· exact False.elim (not_top_le_coe a (ha h₁))

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
⊢ y ≤ x

Tactic:
cases hs.total hx hy with
  | inr h' => exact h'
  | inl h' => simpa [lt_iff_le_not_ge, h'] using h

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e '' c = t

Tactic:
by
    rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]
    exact hc.2 (ht.image e.symm) ((e.toEquiv.subset_symm_image _ _).2 hf)

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by
  rw [← cast_le (K := K), cast_intCast]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by
  rw [← cast_le (K := K), cast_intCast]

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

Goal state before:
pp: n k : ℕ
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ

Tactic:
by
    rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) ≤ f x + f y

Tactic:
by
  rw [div_eq_mul_inv, ← map_inv_eq_map f y]
  exact map_mul_le_add _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ ⌊f a + 2⁻¹⌋ = ⌊f a + f 2⁻¹⌋

Tactic:
map_inv₀,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : LinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ ⌊f a + 2⁻¹⌋ = ⌊f a + (f 2)⁻¹⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
⊢ (∃ z, -x = ↑z) ↔ ∃ z, x = ↑z

Tactic:
constructor <;> rintro ⟨z, hz⟩ <;> use -z

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ x = ↑(-z)

case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ -x = ↑(-z)
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)
hny : y - 0 • a ∈ Ioc l (l + a)
⊢ y ∈ Icc l (l + a)

Tactic:
by simpa using Ioc_subset_Icc_self hny

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉ / b⌉ ≤ b * (↑⌈(b - 1)⁻¹⌉ / b)

Tactic:
rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]
    positivity

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ⋯
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ (↑q.den / ↑q.num).den = q.num.natAbs

Tactic:
suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact mod_cast this

Goal state after:
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ ↑(↑q.den / ↑q.num).den = ↑q.num.natAbs
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
refine ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans ?_, hy₂.trans' ?_⟩ <;> assumption_mod_cast

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ 2 • (x -ᵥ y) = 0 ↔ y = x

Tactic:
← nsmul_zero 2,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ 2 • (x -ᵥ y) = 2 • 0 ↔ y = x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : 2 • (x₁ -ᵥ x₂) = 0
⊢ x₁ = x₂

Tactic:
← nsmul_zero 2,

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : 2 • (x₁ -ᵥ x₂) = 2 • 0
⊢ x₁ = x₂
Module: Mathlib.Data.List.Count

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂) + countP p l₂

Tactic:
← countP_append

Goal state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
⊢ {b}.card + 1 = 2

Tactic:
card_singleton

Goal state after:
α : Type u_1
a b : α
⊢ 1 + 1 = 2
Module: Mathlib.Data.List.Nodup

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

Tactic:
rcases hx with (rfl | ⟨y, hy, hx⟩)

Goal state after:
case neg.inl
α : Type u
x hd : α
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
h : [hd].Nodup
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x

case neg.inr
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
u : Multiset α
a : α
s✝ : Multiset α
IH : ∀ {s : Multiset α}, s - s✝ ≤ u ↔ s ≤ u + s✝
s : Multiset α
⊢ s - a ::ₘ s✝ ≤ u ↔ s ≤ u + a ::ₘ s✝

Tactic:
simp [IH, erase_le_iff_le_cons]

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ m'.card = t.card

Tactic:
· simpa using hc

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ {b}.card = 1

Tactic:
card_singleton

Goal state after:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ 1 = 1
Module: Mathlib.Data.List.Dedup

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

Tactic:
by by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

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

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

Tactic:
by by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
| List.take n xs

Tactic:
Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
| List.filter (fun a ↦ elem a (List.take n xs)) xs
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).toFinset.val.card = s.val.card
⊢ Set.InjOn f ↑s

Tactic:
toFinset

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : { val := (Multiset.map f s.val).dedup, nodup := ⋯ }.val.card = s.val.card
⊢ Set.InjOn f ↑s