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

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

pp: case neg
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : ¬a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
· exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha

Goal state after:
case neg
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : ¬a ≤ b
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a + (b - a) / 2 < b

Tactic:
by
  rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]

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

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

Tactic:
hb

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
b : α
hb : b ∈ l.insertIdx n a
⊢ b ∈ a :: l
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
⊢ Perm ∘r Perm = Perm

Tactic:
funext a c; apply propext
  constructor
  · exact fun ⟨b, hab, hba⟩ => Perm.trans hab hba
  · exact fun h => ⟨a, Perm.refl a, h⟩

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

Goal state before:
pp: α : Type u
x y : α
x✝ : x ∈ [].getLast?
⊢ x ∈ [y].getLast?

Tactic:
by contradiction

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

Goal state before:
pp: α : Type u
l₁ : List α
hl₂ : [] ≠ []
⊢ (l₁ ++ []).getLast? = [].getLast?

Tactic:
by contradiction

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

Goal state before:
pp: α : Type u
a : α
h : a ∈ [].head?
⊢ a :: [].tail = []

Tactic:
by contradiction

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
h : [] ≠ []
⊢ [].head! ∈ [].head?

Tactic:
by contradiction

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

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

Tactic:
by rw [foldl_cons, hf b, foldl_fixed' hf l]

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

Goal state before:
pp: case nil
α : Type u
f : α → α
hl : ∀ (f : α → α), f ∈ [] → Injective f
hf : Injective f
⊢ Injective (foldl comp f [])

Tactic:
exact hf

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

Goal state before:
pp: q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ q.num ∣ n

Tactic:
rw [qdf]

Goal state after:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ (n /. d).num ∣ n
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₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₂ = ↑n₁ * ↑d₂ / ↑d₁
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
eq_div_iff_mul_eq d₁a,

Goal state after:
α : 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₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₂ * ↑d₁ = ↑n₁ * ↑d₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ q.num ≠ 0

Tactic:
rw [qdf]

Goal state after:
case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
⊢ (q - r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q - r).den

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]

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

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a)⁻¹.num = 1

Tactic:
have : 2 ≤ a := Nat.AtLeastTwo.prop

Goal state after:
a : ℕ
inst✝ : a.AtLeastTwo
this : 2 ≤ a
⊢ (OfNat.ofNat a)⁻¹.num = 1
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
⊢ a * c < b * d

Tactic:
obtain rfl | hc := eq_zero_or_pos c

Goal state after:
case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ a * 0 < b * d

case inr
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
x✝ : Set β
⊢ IsGLB x✝ (gi.choice (sInf (u '' x✝)) ⋯)

Tactic:
gi.choice_eq

Goal state after:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : PartialOrder β
inst✝ : CompleteLattice α
gi : GaloisInsertion l u
x✝ : Set β
⊢ IsGLB x✝ (l (sInf (u '' x✝)))
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ (⋂ i, t i) ∪ {x} = ⋂ i, t i ∪ {x}

Tactic:
iInter_union

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≤ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
simp only [le_refl, iSup_pos, iSup_and', lt_iff_le_and_ne, and_comm, sup_comm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t

Tactic:
iInter_union

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
⊢ sSup ∅ = sSup t

Tactic:
have : t = ∅ := eq_empty_of_forall_notMem (fun y yt ↦ by simpa using ht y yt)

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x
this : t = ∅
⊢ sSup ∅ = sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
⊢ b ∈ s → b ∈ {⊤}

Tactic:
hb

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
hb : b ∈ s
⊢ b ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
⊢ b ∈ (fun a ↦ ↑a) ⁻¹' s → a ≤ b

Tactic:
hb

Goal state after:
case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : b ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
⊢ sSup S ≤ a

Tactic:
rcases S.eq_empty_or_nonempty with h | h
    · change ite _ _ _ ≤ a
      simp [h]
    · exact (WithTop.isLUB_sSup' h).2 ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
⊢ y✝ ∈ f ⁻¹' c → x✝ ≠ y✝ → (fun x y ↦ r x y ∨ r y x) x✝ y✝

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
x✝ : α
ha : x✝ ∈ f ⁻¹' c
y✝ : α
hb : y✝ ∈ f ⁻¹' c
⊢ x✝ ≠ y✝ → (fun x y ↦ r x y ∨ r y x) x✝ y✝
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ {a}.OrdConnected

Tactic:
by
  rw [← Icc_self]
  exact ordConnected_Icc

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:
← e.coe_fn_toEquiv,

Goal state after:
α : 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.toEquiv '' c = t
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
⊢ b ∈ ⇑φ '' s → ∀ ⦃y : β⦄, y ∈ ⇑φ '' s → b ≠ y → r'ᶜ b y

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
⊢ ∀ ⦃y : β⦄, y ∈ ⇑φ '' s → b ≠ y → r'ᶜ b y
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
⊢ IsChain r (SuccChain r s)

Tactic:
if h : ∃ t, IsChain r s ∧ SuperChain r s t then exact (succChain_spec h).1
  else
    rw [exists_and_left] at h
    simpa [SuccChain, dif_neg, h] using hs

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsAntichain (fun x1 x2 ↦ r ↑x1 ↑x2) (s ↓∩ t) ↔ IsAntichain r (s ∩ t)

Tactic:
simp [IsAntichain, Set.Pairwise]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, [[x, y]] ⊆ s
y : α
hy : y ∈ s
z : α
hz : z ∈ s
⊢ [[y, x]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]

Tactic:
rw [uIcc_comm]

Goal state after:
Module: Mathlib.Order.Antichain

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

Tactic:
← e.coe_fn_toEquiv,

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e.toEquiv '' c = t
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩) = ↑1

Tactic:
simp [r.2.ne']

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ↑(⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩) = ↑1

Tactic:
simp [r.2.ne']

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ⊔ a ⊔ (a⁻¹ ⊔ 1) = |a|ₘ

Tactic:
sup_assoc,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ⊔ (a ⊔ (a⁻¹ ⊔ 1)) = |a|ₘ
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a⁺ᵐ
⊢ a⁺ᵐ = a

Tactic:
rw [oneLePart_def, right_lt_sup, not_le] at ha; exact oneLePart_eq_self.2 ha.le

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

Goal state before:
pp: n k : ℕ
⊢ n * n ^ k ≤ (n + k) * n.ascFactorial k

Tactic:
← succ_ascFactorial

Goal state after:
n k : ℕ
⊢ n * n ^ k ≤ n * n.succ.ascFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k * (n + 1 + k) ≤ (n + k + 1) ^ k * (n + k + 1)

Tactic:
Nat.add_right_comm n 1 k

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)
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✝ : GroupNormClass F α β
f : F
x : α
⊢ x = 1 → f x = 0

Tactic:
by
    rintro rfl
    exact map_one_eq_zero _

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

Goal state before:
pp: a b : ℕ+
⊢ a - b ≤ a

Tactic:
by
  rw [← coe_le_coe, sub_coe]
  split_ifs with h
  · exact Nat.sub_le a b
  · exact a.2

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

Goal state before:
pp: a b : ℕ+
h : a < b
⊢ (↑a + if a < b then ↑b - ↑a else 1) = ↑b

Tactic:
if_pos h

Goal state after:
a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) = ↑k

Tactic:
if_pos h

Goal state after:
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k = ↑k
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x ↦ 1 ^ x
b : α
hb : b ≠ 1
⊢ False

Tactic:
simpa [hb.symm] using ha b

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

Goal state before:
pp: n : ℤ
d : ℕ
⊢ ⌊↑n / ↑d⌋ = n / ↑d

Tactic:
rw [Rat.floor_def']

Goal state after:
n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d

Tactic:
obtain rfl | hd := eq_zero_or_pos (a := d)

Goal state after:
case inl
n : ℤ
⊢ (↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0

case inr
n : ℤ
d : ℕ
hd : 0 < d
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ↑(fract x) = fract ↑x

Tactic:
simp only [fract, cast_sub, cast_intCast, floor_cast]

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

Goal state before:
pp: q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

Tactic:
rw [← sub_lt_iff_lt_add']

Goal state after:
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
refine ⟨n, ?_, ?_⟩

Goal state after:
case refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ y ^ (n + 1) < x

case refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inr.refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ a < c ^ (-↑n)

Tactic:
lt_inv_comm₀ (pow_pos hc₀ n) ha,

Goal state after:
case inr.inr.inr.refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : a < (c ^ n)⁻¹
⊢ a < c ^ (-↑n)
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
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |↑m * δ - q| ≤ δ

Tactic:
← Nat.succ_pred_eq_of_pos m_pos,

Goal state after:
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
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |↑m.pred.succ * δ - q| ≤ δ
Module: Mathlib.Algebra.Torsor.Basic

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

Tactic:
sdiv_smul_eq_sdiv_div

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) * ((p₃ /ₛ p₁) / (p₃ /ₛ p₂)) = 1
Module: Mathlib.Algebra.Torsor.Basic

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

Tactic:
sdiv_smul_eq_sdiv_div

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ p₄ : P
⊢ (p₁ /ₛ p₃) / (p₂ /ₛ p₄) = (p₁ /ₛ p₃) / (p₂ /ₛ p₄)
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
⊢ Rel p s t

Tactic:
induction hst with

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n ?convert_1)

pp: case e'_3.h₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (?convert_1 == a) = true

pp: case convert_1
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ α

Tactic:
· rw [← coe_count, coe_replicate]

Goal state after:
case e'_3.h₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
⊢ s + t - u = s + (t - u)

Tactic:
by
  ext a; simp [Nat.add_sub_assoc <| count_le_of_le _ hut]

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)

Tactic:
induction hst with

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

Goal state before:
pp: case cons.inr.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

pp: case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
· apply (d.1 _ h₁ h₃).elim

Goal state after:
case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
· exact count_filter_of_pos h

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → ¬a ∈ t

Tactic:
refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
s t : Multiset α
h : _root_.Disjoint s t
a : α
hs : a ∈ s
ht : a ∈ t
⊢ False

case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ u ≤ ⊥
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = b :: s

Tactic:
by rw [eq_of_heq ba]; exact ⟨_, (mem_inits _ _).2 ⟨_, eq_of_heq st⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)

Tactic:
by
  simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]
  apply Perm.refl

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a t) s ↔ a ∉ s ∧ Disjoint s t

Tactic:
disjoint_insert_left,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∉ s ∧ Disjoint t s ↔ a ∉ s ∧ Disjoint s t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (s.erase a).Nonempty ↔ s.Nontrivial

Tactic:
simp only [Finset.Nonempty, mem_erase, and_comm (b := _ ∈ _)]
  refine ⟨?_, fun hs ↦ hs.exists_ne a⟩
  rintro ⟨b, hb, hba⟩
  exact ⟨_, hb, _, ha, hba⟩

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ s.toFinset = t.toFinset

Tactic:
subst h; congr!

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

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p.toFinset ↔ x ∈ s

Tactic:
by rw [@mem_toFinset _ _ (id _), H]

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

Goal state before:
pp: n : ℕ
⊢ 0 = ⊥

Tactic:
bot_eq_zero

Goal state after:
n : ℕ
⊢ 0 = 0
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [coe_int_sub_eq_ite]

Goal state after:
n : ℕ
u v : Fin n
⊢ (if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n) = (↑↑u - ↑↑v) % ↑n