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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))

Tactic:
[

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹² : Max α
inst✝¹¹ : Min α
inst✝¹⁰ : LE α
inst✝⁹ : LT α
inst✝⁸ : SupSet α
inst✝⁷ : InfSet α
inst✝⁶ : Top α
inst✝⁵ : Bot α
inst✝⁴ : Compl α
inst✝³ : HImp α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))

Tactic:
[

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹² : Max α
inst✝¹¹ : Min α
inst✝¹⁰ : LE α
inst✝⁹ : LT α
inst✝⁸ : SupSet α
inst✝⁷ : InfSet α
inst✝⁶ : Top α
inst✝⁵ : Bot α
inst✝⁴ : Compl α
inst✝³ : HImp α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b

Tactic:
exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
this : Icc a b = Icc (toDual b) (toDual a)
⊢ sInf (f '' Icc a b) = f b

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc (toDual b) (toDual a))
this : Icc a b = Icc (toDual b) (toDual a)
⊢ sInf (f '' Icc (toDual b) (toDual a)) = f b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

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

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Lattice α
a b : α
⊢ [[a, b]] = [[b, a]]
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.1 = y.1
⊢ (fun p ↦ f p.1 p.2) y = f x.1 y.2

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.1 = y.1
⊢ (fun p ↦ f p.1 p.2) y = f y.1 y.2
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Tactic:
by simp [uIcc_eq_union]

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

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
[

Goal state after:
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
[

Goal state after:
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.2 = y.2
⊢ (fun p ↦ f p.1 p.2) y = (fun a ↦ f a x.2) y.1

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.2 = y.2
⊢ (fun p ↦ f p.1 p.2) y = (fun a ↦ f a y.2) y.1
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = uIoo b a

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = uIoo b a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (Ι a b).Nonempty ↔ a ≠ b

Tactic:
by
  simp [uIoc, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
⊢ (range ⇑e).OrdConnected

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
⊢ (range ⇑e).OrdConnected
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f a * f c ≤ f b * f c

Tactic:
grw [le.2 ab]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : Nonempty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
[

Goal state after:
case inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
h✝ : Nonempty ι
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s

Tactic:
[

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = max 1 a

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = max 1 a
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

Tactic:
[

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = max 1 a⁻¹

Tactic:
[

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = max 1 a⁻¹
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ (-↑n)) = ↑q ^ (-↑n)

Tactic:
[

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ (-↑n)) = ↑q ^ (-↑n)
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = (2 * ⌊x⌋ + (⌊↑2 * fract x⌋ + 1)) / 2

Tactic:
Int.mul_add_ediv_left _ _ two_ne_zero,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊↑2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| = min (fract x) (1 - fract x)

Tactic:
[

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| = min (fract x) (1 - fract x)
Module: Mathlib.Algebra.Order.Round

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

Tactic:
[

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Tactic:
[

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
⊢ 0 < k ∧ k < 1

Tactic:
[

Goal state after:
case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : 1 < (fun x ↦ a ^ x) k
hba : (fun x ↦ a ^ x) k < a
⊢ 0 < k ∧ k < 1
Module: Mathlib.Data.Rat.Floor

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

Tactic:
this

Goal state after:
q : ℚ
this✝ : ↑q.num < (q - fract q + 1) * ↑q.den
this : ↑⌊q⌋ = q - fract q
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
Module: Mathlib.Data.Rat.Floor

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

Tactic:
this

Goal state after:
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
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
q_inv_eq : q⁻¹ = q_inv
this✝ : ↑q.den - q.num * ⌊q_inv⌋ < q.num
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num

Tactic:
this

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
this✝ : ↑q.den - q.num * ⌊q_inv⌋ < q.num
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ R (f (l + k • a)) (f (l + (k + 1) • a))

Tactic:
[

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ R (f (l + k • a)) (f (l + (k + 1) • a))
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ fract (f a) = f (fract a)

Tactic:
[

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ fract (f a) = f (fract a)
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a ↑l = List.count a l

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a ↑l = List.count a l
Module: Mathlib.Algebra.Torsor.Basic

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

Tactic:
vsub_eq_zero_iff_eq,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ x = y ↔ y = x
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = a ::ₘ b ::ₘ cs

Tactic:
cons_swap

Goal state after:
α : Type u_1
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} = {b} ↔ a = b

Tactic:
[

Goal state after:
α : Type u_1
a b : α
⊢ {a} = {b} ↔ a = b
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk (⇑(isSetoid α)) _l) ↔ replicate n a ≤ Quot.mk (⇑(isSetoid α)) _l

Tactic:
simp only [quot_mk_to_coe'', coe_count]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ ↑_l
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
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:
rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ Surjective (map f)

Tactic:
by
  intro s
  induction s using Multiset.induction_on with
  | empty => exact ⟨0, map_zero _⟩
  | cons x s ih =>
    obtain ⟨y, rfl⟩ := hf x
    obtain ⟨t, rfl⟩ := ih
    exact ⟨y ::ₘ t, map_cons _ _ _⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a l.dedup = if a ∈ l then 1 else 0

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a l.dedup = if a ∈ l then 1 else 0
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ filter p s + filter (fun a ↦ ¬p a) s = s

Tactic:
filter_add_filter,

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ filter (fun a ↦ p a ∨ ¬p a) s + filter (fun a ↦ p a ∧ ¬p a) s = s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard fun b ↦ decide (p b)) l = List.filter (fun b ↦ decide (p b)) l

Tactic:
by
      rw [← List.filterMap_eq_filter]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ countP p (filter q s) = countP (fun a ↦ p a ∧ q a) s

Tactic:
simp [countP_eq_card_filter]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.dedup.toFinset = m.toFinset

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.dedup.toFinset = m.toFinset
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = replicate (count b s) b

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = replicate (count b s) b
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t

Tactic:
exact
      show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
        ⟨fun o =>
          match s, t, o with
          | _, t, Or.inl rfl => suffix_rfl
          | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
          fun e =>
          match s, t, e with
          | _, t, ⟨[], rfl⟩ => Or.inl rfl
          | s, t, ⟨b :: l, he⟩ =>
            List.noConfusion rfl (heq_of_eq he) fun _ lt => Or.inr ⟨l, eq_of_heq lt⟩⟩

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}

Tactic:
by
  rw [← val_inj]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ RightInverse (fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩

Tactic:
rintro (_ | y) <;> grind

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ s.Finite ↔ t.Finite

Tactic:
[

Goal state after:
α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ s.Finite ↔ t.Finite