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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ ⇑((fun p ↦ (↑g).comp (p.comp ↑f.symm)) ((fun p ↦ (↑g.symm).comp (p.comp ↑f)) p)) = ⇑p

Tactic:
change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ (⇑g ∘ ⇑g.symm) ∘ ⇑p ∘ ⇑f ∘ ⇑f.symm = ⇑p
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
a b : ℤ
ha : a ≠ 0
⊢ a.gcd b ∈ lowerBounds {n | 0 < n ∧ a.gcd b ∣ n}

Tactic:
simp only [lowerBounds, and_imp, Set.mem_ofPred_eq]
    exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = max ↑a ↑b

Tactic:
max_def,

Goal state after:
α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = if ↑a ≤ ↑b then ↑b else ↑a
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
⊢ x + ↑n ≤ 0

Tactic:
by
    have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
    rwa [add_neg_cancel] at this

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
x : WithBot α
⊢ ↑a ≤ x → x ≤ ↑a

Tactic:
by cases x <;> simp; simpa using @h _

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

Goal state before:
pp: case pos.mp
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m → m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

pp: case pos.mpr
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ (m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n) → k + 1 = m

Tactic:
· rintro rfl
        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by lia⟩

Goal state after:
case pos.mpr
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ (m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n) → k + 1 = m
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ b ≤ unbotD a y

Tactic:
rwa [le_unbotD_iff]
  exact ne_bot_of_le_ne_bot (by simp) hy

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithTop α
⊢ x ≤ y →
    x ≤ z →
      x ≤
        match y, z with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

Tactic:
by cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithBot α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
by cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y z : WithZero α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
by cases x <;> cases y <;> cases z <;> simp; simpa using le_inf

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
⊢ image2 f s {b} = s

Tactic:
image2_singleton_right,

Goal state after:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
⊢ (fun a ↦ f a b) '' s = s
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Tactic:
· exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
wf : WellFounded (Function.swap r)
inst✝ : Nonempty α
⊢ ¬Relator.LeftTotal r

Tactic:
intro h
  obtain ⟨a, -, ha⟩ := wf.has_min Set.univ Set.univ_nonempty
  obtain ⟨b, hab⟩ := h a
  specialize ha b (Set.mem_univ b)
  contradiction

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

Goal state before:
pp: γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ Ici ⊤ = {⊤}

Tactic:
Ici_top

Goal state after:
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ {⊤} = {⊤}
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e

Tactic:
by
    have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d
    have pos_n : (0 < (n : A)) := Nat.cast_pos (n := n) |>.2 (of_decide_eq_true h)
    rw [eq]
    exact mul_pos pos_n pos_invOf_d

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
· simp [hb, hb.not_gt, one_le_div]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
⊢ l = [] → Forall₂ R [] l

Tactic:
rintro rfl; exact Forall₂.nil

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
⊢ l = [] → Forall₂ R l []

Tactic:
rintro rfl; exact Forall₂.nil

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : b ≤ 0
⊢ ∃ a' > a, a' * b < c

Tactic:
obtain ⟨a', ha'⟩ := exists_gt a
    exact ⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
wlog! B_pos : 0 < B generalizing B

Goal state after:
case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : B ≤ 0
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inr
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
apply iff_of_false
      · intro h
        rw [h.length_eq] at hn₁
        grind
      · grind [Perm.length_eq]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
x✝ : l₁.length < n ∨ l₁.length ≥ n
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
cases Nat.lt_or_ge (length l₁) n with

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ f a ++ (flatMap f l ++ (g a ++ flatMap g l)) ~ f a ++ (g a ++ flatMap (fun x ↦ f x ++ g x) l)

Tactic:
refine (Perm.trans ?_ (IH.append_left _)).append_left _

Goal state after:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
⊢ flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l

Tactic:
by
  induction l with | nil => simp | cons a l IH => ?_
  simp only [flatMap_cons, append_assoc]
  refine (Perm.trans ?_ (IH.append_left _)).append_left _
  rw [← append_assoc, ← append_assoc]
  exact perm_append_comm.append_right _

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

Goal state before:
pp: α : Type u
a : α
L : List α
⊢ L ⊆ [a] ↔ ∃ n, L = replicate n a

Tactic:
by
  simp only [eq_replicate_iff, subset_def, mem_singleton, exists_eq_left']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
L : List M
h : L.prod ≠ 1
⊢ 0 < L.length

Tactic:
by
  cases L
  · simp at h
  · simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ (x :: xs).prod * (y :: ys).prod =
    (zipWith (fun x1 x2 ↦ x1 * x2) (x :: xs) (y :: ys)).prod * (drop (y :: ys).length (x :: xs)).prod *
      (drop (x :: xs).length (y :: ys)).prod

Tactic:
by
    simp only [zipWith_cons_cons, prod_cons]
    conv =>
      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
    simp [mul_assoc]

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

Goal state before:
pp: q a b c : ℚ
x✝¹ : ℕ
x✝ : ℚ
⊢ ↑↑x✝¹.succ * x✝ = ↑↑x✝¹ * x✝ + x✝

Tactic:
simp [Rat.add_mul]

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

Goal state before:
pp: q : ℚ
hq : q.den = 1
⊢ ↑q.num = q

Tactic:
by
  conv_rhs => rw [← num_divInt_den q, hq]
  rw [intCast_eq_divInt]
  rfl

Goal state after:
Module: Mathlib.Data.PNat.Defs

Goal state before:
pp: n : ℤ
hn : 0 < n
⊢ ↑n.natAbs = n

Tactic:
Int.natAbs_of_nonneg hn.le

Goal state after:
n : ℤ
hn : 0 < n
⊢ n = n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: b c : ℤ
⊢ ↑c * ↑(b / b) = ↑(c * b) / ↑b

Tactic:
intCast_div_self,

Goal state after:
b c : ℤ
⊢ ↑c * (↑b / ↑b) = ↑(c * b) / ↑b
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * (b + c)

Tactic:
rw [mul_add]

Goal state after:
R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * b + a * c
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j = ⨆ i, f i

Tactic:
apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · refine iSup_le fun j ↦ ?_
    obtain ⟨i, jlt⟩ := exists_gt j
    exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

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

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Tactic:
have : Nonempty s := hs.to_subtype
  simp [biInter_eq_iInter, ← iInter_inter]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) = sSup ((fun a ↦ ↑a) '' s)

Tactic:
change _ = ite _ _ _

Goal state after:
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) =
    if ⊤ ∈ (fun a ↦ ↑a) '' s then ⊤
    else if BddAbove ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s) then ↑(sSup ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s)) else ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) = sInf ((fun a ↦ ↑a) '' s)

Tactic:
change _ = ite _ _ _

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) =
    if (fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s) then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s))
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
s t : Set α
⊢ sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2

Tactic:
by
  simp only [sSup_eq_iSup, biSup_inf_biSup]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : a = b
⊢ min a b = if a ≤ b then a else b

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ min a b = if a ≤ b then a else b

Tactic:
· simp [hab]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ min a b = if a ≤ b then a else b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : a = b
⊢ max a b = if a ≤ b then b else a

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ max a b = if a ≤ b then b else a

Tactic:
· simp [hab]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ max a b = if a ≤ b then b else a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
⊢ sSup s = sSup t

Tactic:
have Bs : BddAbove s := by
      rcases B with hB | ⟨b, hb⟩
      · exact hB
      · refine ⟨b, fun x hx ↦ ?_⟩
        rcases hs x hx with ⟨y, hy, hxy⟩
        exact hxy.trans (hb hy)
    have Bt : BddAbove t := by
      rcases B with ⟨b, hb⟩ | hB
      · refine ⟨b, fun y hy ↦ ?_⟩
        rcases ht y hy with ⟨x, hx, hyx⟩
        exact hyx.trans (hb hx)
      · exact hB
    apply le_antisymm
    · apply csSup_le s_ne (fun x hx ↦ ?_)
      rcases hs x hx with ⟨y, yt, hxy⟩
      exact hxy.trans (le_csSup Bt yt)
    · apply csSup_le t_ne (fun y hy ↦ ?_)
      rcases ht y hy with ⟨x, xs, hyx⟩
      exact hyx.trans (le_csSup Bs xs)

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
⊢ [[a, b]] = [[b, a]]

Tactic:
simp_rw [uIcc, inf_comm, sup_comm]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c

pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ [[a, c]]
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
· rw [uIoc_comm, union_comm, uIoc_comm, this _ (le_of_not_ge hac), uIoc_comm]
    rwa [uIcc_comm]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ [[a, c]]
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c
Module: Mathlib.Data.Int.CharZero

Goal state before:
pp: k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp [Int.ediv_zero]
  · exact cast_div n_dvd (cast_ne_zero.mpr hn)

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

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n.pred.succ < (n.pred + 1) * n.pred !

Tactic:
exact (Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2
    ((Nat.lt_of_lt_of_le hn (self_le_factorial _)))

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

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!

Tactic:
refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
    (factorial_le ?_)

Goal state after:
case refine_1
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i ≤ i + n

case refine_2
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 0 < i + n

case refine_3
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ 1 < (i + n)!

case refine_4
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ n + 1 ≤ i + n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n

Tactic:
rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -2 ≤ a - 1

Tactic:
rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]

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

Goal state before:
pp: case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ fract x ≤ 1

Tactic:
exact (fract_lt_one x).le

Goal state after:
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
inst✝ : IsOrderedRing R
z : ℤ
⊢ ↑z ≤ -a ↔ a ≤ -↑z

Tactic:
le_neg

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ a ≤ -↑z ↔ a ≤ -↑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
b : H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x + ↑n) = f x + n • b

Tactic:
simp [← map_add_nsmul]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) * (p₂ /ₛ p₃) = p₁ /ₛ p₃

Tactic:
apply smul_right_cancel p₃

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ ((p₁ /ₛ p₂) * (p₂ /ₛ p₃)) • p₃ = (p₁ /ₛ p₃) • p₃
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p : P
⊢ v₁ • p /ₛ v₂ • p = v₁ / v₂

Tactic:
by
  rw [sdiv_smul_eq_sdiv_div, smul_sdiv_assoc, sdiv_self, mul_one]

Goal state after:
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⌉.toNat = ⌈a⌉

Tactic:
Int.toNat_of_nonneg (Int.ceil_nonneg_of_neg_one_lt ha)

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ ⌈a⌉ = ⌈a⌉
Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x✝ : γ
⊢ x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t

Tactic:
simp [mem_smul, mem_smul_set, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP ((fun x_1 ↦ x_1 == f x) ∘ f) l = countP (fun x_1 ↦ x_1 == x) l

Tactic:
unfold Function.comp

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP (fun x_1 ↦ (fun x_2 ↦ x_2 == f x) (f x_1)) l = countP (fun x_1 ↦ x_1 == x) l
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
s : Multiset α
inst✝ : DecidableEq α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α)) _l) ↔
    ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → count a (Quot.mk (⇑(isSetoid α)) _l) = 1

Tactic:
simpa using List.nodup_iff_count_eq_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ Set.range (map c)

Tactic:
Set.range_list_map

Goal state after:
α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ {l | ∀ (x : α), x ∈ l → x ∈ Set.range c}
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp.cons.inl
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih : ∀ {as_1 : Multiset α}, a ::ₘ as_1 = as → ∃ b bs', r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

pp: case mp.cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
· exact ⟨b, bs, ha'b, h, rfl⟩

Goal state after:
case mp.cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ {a} + s = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
singleton_add

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ take (n + 1) (b :: l) = List.filter (fun a ↦ elem a (take (n + 1) (b :: l))) (b :: l)

Tactic:
by
    rw [take_succ_cons, Nodup.take_eq_filter_mem (Nodup.of_cons hl), filter_cons_of_pos (by simp)]
    congr 1
    refine List.filter_congr ?_
    intro x hx
    have : x ≠ b := fun h => (nodup_cons.1 hl).1 (h ▸ hx)
    simp +contextual [List.mem_filter, this, hx]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList.length = s.card

Tactic:
← coe_card,

Goal state after:
α : Type u_1
s : Multiset α
⊢ (↑s.toList).card = s.card