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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - min a b + min a b = a

Tactic:
@tsub_add_cancel_of_le

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a = a

case h
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ min a b ≤ a
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
d y : α
x : WithBot α
⊢ unbotD d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d

Tactic:
induction x

Goal state after:
case bot
α : Type u_1
d y : α
⊢ unbotD d ⊥ = y ↔ ⊥ = ↑y ∨ ⊥ = ⊥ ∧ y = d

case coe
α : Type u_1
d y a✝ : α
⊢ unbotD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = ⊥ ∧ y = d
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
rw [add_zero]

Goal state after:
case coe.zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ ≤ ↑a✝ + c
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
rw [add_zero]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
x : WithBot (WithTop α)
H : ∀ (a : α), ↑↑a ≤ x
⊢ x = ⊤

Tactic:
induction x

Goal state after:
case bot
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
H : ∀ (a : α), ↑↑a ≤ ⊥
⊢ ⊥ = ⊤

case coe
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : Nonempty α
inst✝ : NoTopOrder α
a✝ : WithTop α
H : ∀ (a : α), ↑↑a ≤ ↑a✝
⊢ ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < x ∧ z < y

Tactic:
constructor <;> exact lt_of_lt_of_le hlt ‹z' ≤ _›

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
rw [floor_of_nonpos ha]
    exact Nat.zero_le _

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

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

Tactic:
rw [floor_of_nonpos ha]
    exact Nat.zero_le _

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₂ b

Tactic:
← h hb

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₂ b

Tactic:
← h hb

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → f x b ∈ u

Tactic:
@forall₂_comm α

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ |a| ^ n = a ^ n

Tactic:
rw [← abs_pow, abs_eq_self]; exact hn.pow_nonneg _

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

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

Tactic:
isGreatest_univ.upperBounds_eq,

Goal state after:
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ Ici ⊤ = {⊤}
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddAbove ∅

Tactic:
by
  simp only [BddAbove, upperBounds_empty, univ_nonempty]

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n

Tactic:
apply Nat.cast_pos'.2

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < n
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
by
  rw [prl, prr, prt]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
by
  rw [prl, prr, prt]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
h1 : 0 < a
h2 : a ≤ 1
⊢ 1 ≤ 1 / a

Tactic:
by
  rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]

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:
by
  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.TakeDrop

Goal state before:
pp: α : Type u
x : List α
n : ℕ
⊢ take n x = x ↔ x.length ≤ n

Tactic:
take_eq_self_iff

Goal state after:
α : Type u
x : List α
n : ℕ
⊢ x.length ≤ n ↔ x.length ≤ n
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
⊢ a = b ∨ a ∈ l

Tactic:
by
  cases Nat.lt_or_ge (length l) n with
  | inl hn =>
    rw [insertIdx_of_length_lt hn] at h
    exact .inr h
  | inr hn =>
    rwa [mem_insertIdx hn] at h

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

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

Tactic:
cases huv

Goal state after:
case nil.nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case swap
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
v : List β
huv : Forall₂ r (a₁ :: a₂ :: h₂₃) v
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) v

Tactic:
| swap a₁ a₂ h₂₃ =>

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a : α
as : List α
h : a ∈ as
⊢ lookup a (map (fun x ↦ (x, f x)) as) = some (f a)

Tactic:
induction as with grind

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
y z a b : α
ha : a ∣ y
hb : b ∣ z
H1 : IsRelPrime (a * b) z
H2 : a * b ∣ y * z
h : IsPrimal (a * b)
⊢ a * b ∣ y

Tactic:
exact (H1.of_mul_left_right.isUnit_of_dvd hb).mul_right_dvd.mpr ha

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

Goal state before:
pp: α : Type u
x : BinaryTree α
⊢ x.numLeaves = x.numNodes + 1

Tactic:
induction x

Goal state after:
case nil
α : Type u
⊢ nil.numLeaves = nil.numNodes + 1

case node
α : Type u
value✝ : α
left✝ right✝ : BinaryTree α
left_ih✝ : left✝.numLeaves = left✝.numNodes + 1
right_ih✝ : right✝.numLeaves = right✝.numNodes + 1
⊢ (node value✝ left✝ right✝).numLeaves = (node value✝ left✝ right✝).numNodes + 1
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
e : R
h : (a + 0) ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e

Tactic:
by
  simp [← h]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
e : R
h : a ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e + 0

Tactic:
by
  simp [← h]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, ⨆ (_ : i ≥ n), u i ≤ ⨆ i, u (i + n)

Tactic:
simp only [iSup_le_iff]

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ i ≥ n, u i ≤ ⨆ i, u (i + n)
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ i, u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
simp only [iSup_le_iff]

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
s : Set α
⊢ sSup s = sSup (range fun a ↦ ↑a)

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_1
inst✝ : SupSet α
s : Set α
⊢ sSup s = sSup s
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
g : ((i : ι) → κ i) → ι
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j

Tactic:
have ⟨a, ha⟩ : ∃ a, ∀ b, ∃ f, ∃ h : a = g f, h ▸ b = f (g f) := by
    by_contra! h
    choose h hh using h
    have := hh _ h rfl
    contradiction

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
g : ((i : ι) → κ i) → ι
a : ι
ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)
⊢ ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j
Module: Mathlib.Order.CompleteLattice.Basic

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
e : α ≃ β
inst✝ : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
⊢ CompleteLattice α

Tactic:
apply e.injective.completeLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderTop α
a : α
x y : ↑(Ici a)
⊢ Disjoint x y ∧ Codisjoint x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint ↑x ↑y

Tactic:
Ici.disjoint_iff,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderTop α
a : α
x y : ↑(Ici a)
⊢ ↑x ⊓ ↑y = a ∧ Codisjoint x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint ↑x ↑y
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa only [uIcc_comm] using uIcc_injective_right a

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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsChain r univ ↔ Std.Trichotomous r

Tactic:
by
  refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
  have : a ≠ b → (r a b ∨ r b a) := h trivial trivial
  grind

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y} ↦ ↑y) '' t) ↑(sSup t)

Tactic:
← subset_sSup_of_within s ht h_bdd (h_Sup ht h_bdd)

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y} ↦ ↑y) '' t) (sSup (Subtype.val '' t))
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a : α
ha : 1 < a
⊢ 1 < a⁺ᵐ

Tactic:
oneLePart_eq_self.2 ha.le

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a : α
ha : 1 < a
⊢ 1 < a
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:
rw [div_eq_mul_inv, ← map_inv_eq_map f y]
  exact map_mul_le_add _ _ _

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✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |f x - f y| ≤ f (x / y)

Tactic:
rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']
  exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩

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

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

Tactic:
Nat.pow_one,

Goal state after:
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n.descFactorial 1
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
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑⌊a⌋ + b = a

Tactic:
← eq_sub_iff_add_eq,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑⌊a⌋ = a - b
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✝² : AddZeroClass G
inst✝¹ : Add H
inst✝ : AddConstMapClass F G H a b
f : F
⊢ f a = f 0 + b

Tactic:
by
  simpa using map_add_const f 0

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ {l | ∀ (x : α), x ∈ l → x ∈ range Subtype.val} = {l | ∀ (x : α), x ∈ l → x ∈ s}

Tactic:
Subtype.range_coe

Goal state after:
α : Type u_1
s : Set α
⊢ {l | ∀ (x : α), x ∈ l → x ∈ s} = {l | ∀ (x : α), x ∈ l → x ∈ s}
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ Rel r (a ::ₘ s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r (a ::ₘ s) bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
simp only [ih, cons_add, rel_cons_left]

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') ↔
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
⊢ Pairwise (fun a b ↦ b ≠ a) l ↔ l.Nodup

Tactic:
simp only [Nodup, Ne, eq_comm]

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

Goal state before:
pp: α : Type u
l : List α
u : α
⊢ (l.concat u).Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
rw [← nodup_reverse]

Goal state after:
α : Type u
l : List α
u : α
⊢ (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
u : α
⊢ (l.concat u).Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
rw [← nodup_reverse]
  simp

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u

Tactic:
obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = map f s ↔ s = 0

Tactic:
by
  rw [eq_comm, map_eq_zero]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ s.card

Tactic:
← s.card_map f,

Goal state after:
α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ t.card ≤ (map f s).card
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s

Tactic:
| cons x s ih =>

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
s : Multiset α
f : α → β
x : { x // x ∈ s }
⊢ map (fun j ↦ f ↑j) (s.attach.erase x) = map f (s.erase ↑x)

Tactic:
by
  simp only [← Function.comp_apply (f := f)]
  rw [← map_map, erase_attach_map_val]

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 : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α), b ∈ filter (fun a ↦ f x = f a) s → f x = f b

Tactic:
· simp only [mem_filter, and_imp, @eq_comm _ (f x), imp_self, implies_true]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ filter p s.attach = map (Subtype.map id ⋯) (filter (fun x ↦ ∃ h, p ⟨x, h⟩) s).attach

Tactic:
by
  classical
  refine Multiset.map_injective Subtype.val_injective ?_
  rw [map_filter' _ Subtype.val_injective]
  simp only [Subtype.exists, exists_and_right, exists_eq_right, attach_map_val, Subtype.map, id,
    map_map, comp]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l

Tactic:
simp only [insert_of_mem h, suffix_refl]

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

Goal state before:
pp: a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False

Tactic:
obtain ⟨c, _, rfl⟩ := mem_map.1 hxb

Goal state after:
a : ℕ
m : Multiset ℕ
c : ℕ
left✝ : c ∈ m
hxa : a + c < a
hxb : a + c ∈ map (fun x ↦ a + x) m
⊢ False
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : α
⊢ {a} ≠ univ

Tactic:
by
  apply SetLike.coe_ne_coe.1
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x : Prop), x ∈ { val := {True, False}, nodup := fintype._proof_1 }

Tactic:
by simpa using em

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.18
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : ↥(filter p s)
⊢ p ↑x

Tactic:
by simpa using (Finset.mem_filter.1 x.2).2

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ (i.pred h).succ.rev = i.rev

Tactic:
succ_pred

Goal state after:
n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ i.rev = i.rev
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
by
  rw [← Nat.lt_succ_iff] at han hbn
  simp [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, han, hbn]

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ (i.pred hi).succ < j.succ ↔ i < j.succ

Tactic:
succ_pred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i < j.succ ↔ i < j.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j.succ < (i.pred hi).succ ↔ j.succ < i

Tactic:
succ_pred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j.succ < i ↔ j.succ < i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
⊢ a₂ ∈ ↑s → f' a₁ = f' a₂ → a₁ = a₂

Tactic:
ha₂

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
ha₂ : a₂ ∈ ↑s
⊢ f' a₁ = f' a₂ → a₁ = a₂
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ (i.pred hi).succ ≤ j.succ ↔ i ≤ j.succ

Tactic:
succ_pred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i ≤ j.succ ↔ i ≤ j.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j.succ ≤ (i.pred hi).succ ↔ j.succ ≤ i

Tactic:
succ_pred

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j.succ ≤ i ↔ j.succ ≤ i
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
⊢ ∃ k, k ≤ b ∧ b = a + k

Tactic:
have hkb : k ≤ b := by lia

Goal state after:
n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
hkb : k ≤ ↑b
⊢ ∃ k, k ≤ b ∧ b = a + k
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ (i.pred ⋯).succ = i

Tactic:
succ_pred

Goal state after:
n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ i = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ (a.pred ha).succ.succAbove (b.pred hb).succ = ((a.succAbove b).pred hk).succ

Tactic:
succ_pred

Goal state after: