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

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : a * b < a * c
hbc : b ≤ c
⊢ 0 < a

Tactic:
by
  by_cases! ha : 0 < a
  · exact ha
  · grind [mul_le_mul_of_nonpos_left hbc ha]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 2 * a * b + 2 * a * b ≤ a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
by gcongr; exact two_mul_le_add_sq _ _

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f (a ⊓ b) ≤ f ⊥

Tactic:
exact f.monotone ha.le_bot

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ |n| = 1 ↔ a ^ n = 1

Tactic:
rw [← Int.natCast_natAbs, zpow_natCast, pow_natAbs_eq_one]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n ≤ 0 ↔ n = 0

Tactic:
by norm_cast; lia

Goal state after:
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
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0

Tactic:
add_neg_cancel

Goal state after:
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
this : x + ↑n ≤ 0
⊢ x + ↑n ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + c

Tactic:
· rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
    rw [← coe_add, ← coe_add _ c, coe_le_coe]
    gcongr

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

Goal state before:
pp: x y : WithZero (Multiplicative ℤ)
hy : y ≠ 0
⊢ x < y * exp 1 ↔ x ≤ y

Tactic:
lift y to Multiplicative ℤ using hy
  obtain rfl | hx := eq_or_ne x 0
  · simp
  lift x to Multiplicative ℤ using hx
  rw [← log_le_log, ← log_lt_log] <;> simp [log_mul, Int.lt_add_one_iff]

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✝ : DistribLattice α
x y z : WithBot α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_inf, ← coe_sup]
    simpa [← coe_inf, ← coe_sup] using le_sup_inf

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact Nat.zero_le _
  · exact cast_le.1 ((floor_le ha).trans <| le_ceil _)

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b

Tactic:
simpa only [← sub_eq_add_neg] using dvd_add_left (dvd_neg.2 h)

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

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
have hd := nonneg_of_le_add_right (hb.trans_eq hbd)

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t

Tactic:
exact ⟨ha', hb'⟩

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
rw [image2_swap f]
  exact image_image2_distrib fun _ _ => h_antidistrib _ _

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
ho : Odd n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
simp only [ho, and_true, ← ho.neg_pow, (ho.strictMono_pow (R := R)).injective.eq_iff]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
⊢ (fun i ↦ if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x

Tactic:
ext i

Goal state after:
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
⊢ (if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x i
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j

Tactic:
· right
    exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
c n : ℕ
x a : α
n' : ℕ
a' : α
h₁ : c * n = n'
h₂ : smul c a = a'
⊢ smul c (term n x a) = term n' x a'

Tactic:
by
  simp [h₂.symm, h₁.symm, term, smul, nsmul_add, mul_nsmul']

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

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
hl : l ≠ []
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod

Tactic:
induction l with
  | nil => simp at hl
  | cons a l ih =>
    by_cases hl_empty : l = []
    · simp [*]
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih hl_empty base.2)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ (a✝, b✝) :: zipWith Prod.mk l₁✝ l₂✝
⊢ R x y

Tactic:
mem_cons

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
⊢ R x y
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?
⊢ l₁ = l₂

Tactic:
by
  apply ext_getElem?
  grind

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:
simp only [zipWith_cons_cons, prod_cons]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
⊢ foldr f b (a :: l) = b

Tactic:
by rw [foldr_cons, foldr_fixed' hf l, hf a]

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

Goal state before:
pp: case succ
a b : ℕ
ih : range' a b 0 = replicate b a
⊢ range' a (b + 1) 0 = replicate (b + 1) a

Tactic:
| succ b ih =>

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

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
h : m * n ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂

Tactic:
obtain ⟨a₁, a₂, ⟨b, rfl⟩, ⟨c, rfl⟩, rfl⟩ := hm (dvd_of_mul_right_dvd h)

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * b * (a₂ * c)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = ↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }

Tactic:
by
    have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
    have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
    rw [mk_eq_divInt, mk_eq_divInt] at h ⊢
    rw [cast_divInt_of_ne_zero _ (by simpa), cast_divInt_of_ne_zero _ (by simpa)] at h
    norm_cast at h
    rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq,
      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁,
      ← Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
      at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ ⨆ i, (↑i).down = ⨆ a ∈ s, a.down

Tactic:
iSup_subtype''

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ ⨆ t ∈ s, t.down = ⨆ a ∈ s, a.down
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
⊢ ⨆ i, f i = ⨆ i, f { down := i }

Tactic:
simp only [iSup]

Goal state after:
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
⊢ sSup (range fun i ↦ f i) = sSup (range fun i ↦ f { down := i })
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
⊢ ⨆ i ∈ s, a = a

Tactic:
have : Nonempty s := Set.nonempty_coe_sort.mpr hs
  rw [← iSup_subtype'', iSup_const]

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

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : Set β
t : ι → Set β
⊢ s \ ⋂ i, t i = ⋃ i, s \ t i

Tactic:
by
  simp only [sdiff_eq, compl_iInter, inter_iUnion]

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

Goal state before:
pp: β : Type u_2
inst✝ : CompleteLattice β
s : Set (Set β)
⊢ sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

Tactic:
simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
ext i

Goal state after:
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
i : ι
⊢ (⨅ a, ⨆ b, f a b) i = (⨆ g, ⨅ a, f a (g a)) i
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ s ⊆ SuccChain r s

Tactic:
by
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then exact (succChain_spec h).2.1
  else
    simp [SuccChain, h]

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

Goal state before:
pp: case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < n

Tactic:
← one_lt_factorial,

Goal state after:
case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < n !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
← one_lt_factorial,

Goal state after:
case inr.inr
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m < n
⊢ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)

Tactic:
by
    rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]
    refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)
    refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_
    rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ ↑|q.num| / ↑q.den = ↑q.num / ↑q.den

Tactic:
abs_of_nonneg (by simpa)

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Algebra.Order.Round

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

Tactic:
← floor_add_fract x,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round (↑⌊x⌋ + fract x) = (⌊2 * (↑⌊x⌋ + fract x)⌋ + 1) / 2
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m

Tactic:
rcases h with ⟨_, rfl⟩
    apply dvd_mul_right

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n

Tactic:
exact one_le_zpow (one_le_div'.2 hab) hn

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
inst✝ : IsOrderedRing R
a b : R
⊢ fract (a + b) ≤ fract a + fract b

Tactic:
rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ← Int.cast_add, Int.cast_le]
  exact le_floor_add _ _

Goal state after:
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
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ 0 ≤ m₁

Tactic:
simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _

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

Goal state before:
pp: 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
⊢ (fract q⁻¹).num < q.num

Tactic:
have q_inv_eq : q⁻¹ = q_inv := by rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]

Goal state after:
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
⊢ (fract q⁻¹).num < q.num
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ : List α
m₁ : ¬a ∈ ↑l₁
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ ↑(r₁ ++ a :: r₂)
⊢ a ::ₘ ↑l₁ ≤ ↑(r₁ ++ a :: r₂)

Tactic:
exact
    perm_middle.subperm_left.2
      ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) s t ↔ s = t

Tactic:
by
  constructor
  · intro h
    induction h <;> simp [*]
  · rintro rfl
    exact rel_eq_refl

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List β
ihl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → l ∈ range (map f)
hl : a :: l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: l ∈ range (map f)

Tactic:
rcases ihl fun x hx => hl x <| subset_cons_self _ _ hx with ⟨l, rfl⟩
    rcases hl a mem_cons_self with ⟨a, rfl⟩
    exact ⟨a :: l, map_cons⟩

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

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a : α
x✝ : a ∈ l₁
b b' : σ a
h : ⟨a, b⟩ = ⟨a, b'⟩
⊢ b = b'

Tactic:
by injection h with _ h

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

Goal state before:
pp: α : Type u
l : List α
r : α → α → Prop
hl : l.Nodup
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l

Tactic:
by
  grind [List.pairwise_iff_forall_sublist]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f (a ::ₘ u) = f a ::ₘ t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1, a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t

Tactic:
rw [map_cons, cons_inj_right] at h

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1, a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ (a :: l').tail = l'

Tactic:
tail_cons

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ l' = l'
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
by_cases hx : x ∈ xs

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : ¬x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
· simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
n : l.Nodup
⊢ (↑l).Nodup

Tactic:
Multiset.coe_nodup

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
n : l.Nodup
⊢ l.Nodup
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t

Tactic:
exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
⊢ bidirectionalRec nil singleton cons_append [] = nil

Tactic:
grind [bidirectionalRec]

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a : α
⊢ bidirectionalRec nil singleton cons_append [a] = singleton a

Tactic:
grind [bidirectionalRec]

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
⊢ [x] <:+: xs ↔ x ∈ xs

Tactic:
rw [List.mem_iff_append, List.IsInfix]
  congr! 4
  simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
⊢ s ∪ {x} = insert x s

Tactic:
rw [Finset.union_comm, singleton_union]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ s.erase a ⊆ t ↔ s ⊆ t

Tactic:
by
  rw [← subset_insert_iff, insert_eq_of_mem h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

Tactic:
refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x ↦ x ∈ t₁) s ∪ filter (fun x ↦ x ∉ t₁) s = s

case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁

case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (range (k + 1))

Tactic:
range_add_one

Goal state after:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (insert k (range k))
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : Set.InjOn f ↑s
⊢ #(image f s) = #s

Tactic:
by
  simp only [card, image_val_of_injOn H, card_map]

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

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

Tactic:
succ_le_castSucc_iff

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

Goal state before:
pp: n m : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero (OfNat.ofNat m)
this : m % (n + m) = m
⊢ NeZero (OfNat.ofNat m)

Tactic:
by simpa [neZero_iff, Fin.ext_iff, OfNat.ofNat, this] using! NeZero.ne m

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

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

Tactic:
succ_le_castSucc_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a < b ↔ a < b