mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊥
⊢ False

Tactic:
exact (bot_lt_coe <| Classical.arbitrary _).not_ge <| h <| by simp

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
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ b < ⌈a + ↑n⌉₊ ↔ b < ⌈a⌉₊ + n

Tactic:
rw [lt_ceil]

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ c * a = b ↔ a = ⅟c * b

Tactic:
← mul_right_inj_of_invertible (c := ⅟c),

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ ⅟c * (c * a) = ⅟c * b ↔ a = ⅟c * b
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ 1 = 1 + ⅟b * a + (1 + ⅟a * b) ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b

Tactic:
rw [← add_assoc, add_comm _ 1, ← add_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a : α
⊢ |a| ^ 2 = a ^ 2

Tactic:
by simpa only [sq] using abs_mul_abs_self a

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ RightInverse (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)) (Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯)

Tactic:
by rintro ⟨⟨_⟩, ⟨_⟩⟩; rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
u s : Set α
⊢ (fun x ↦ ↑((Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' f '' u

Tactic:
by
  ext ⟨b, a, has, rfl⟩
  simp [hf.eq_iff]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
· refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
    · rw [← Icc_sdiff_right]
      exact subset_sdiff_singleton hc hb
    · rwa [← Ico_sdiff_left, sdiff_singleton_subset_iff, insert_eq_of_mem ha] at ho

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ m = m'

Tactic:
funext α β f x

Goal state after:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
f : α → β
x : F α
⊢ m f x = m' f x
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < b' * a

Tactic:
exact exists_lt_mul_left_of_nonneg hb.le hc h

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

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

Tactic:
by
  simp_rw [mul_comm a] at hc ⊢; exact exists_mul_left_lt₀ hc

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl : l ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

Tactic:
by
  match l, hl with | x :: xs, hl => induction xs generalizing x <;> simp_all

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
by_cases ha : a = 0
  · simp [ha]
  by_cases hb : b = 0
  · simp [hb]
  simpa [zpow', ha, hb] using mul_zpow a b n

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

Goal state before:
pp: α : Type u
x a : α
l : List α
h : a = x
⊢ a :: l = x :: (a :: l).tail

Tactic:
exact h ▸ rfl

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

Goal state before:
pp: case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
rintro rfl
    exact ⟨rfl, fun _ _ _ ↦ rfl⟩

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

Goal state before:
pp: case inr
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
· simp only [map, erase_cons_tail (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
        mul_left_comm (f a) (f b)]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a b : G
l : List G
⊢ a * b⁻¹ * l.alternatingProd = a * (b⁻¹ * l.alternatingProd⁻¹⁻¹)

Tactic:
inv_inv,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a b : G
l : List G
⊢ a * b⁻¹ * l.alternatingProd = a * (b⁻¹ * l.alternatingProd)
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a * b⁻¹ * (d⁻¹⁻¹ * c⁻¹) = a * c⁻¹ * (d⁻¹⁻¹ * b⁻¹)

Tactic:
inv_inv,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (d * b⁻¹)
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)

Tactic:
by
  rw [sq, sq, mul_self_tsub_mul_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Type u_8
ι' : Type u_9
g : ι' → α
e : ι ≃ ι'
s : Set ι'
⊢ ⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i

Tactic:
simpa only [iSup_subtype'] using! (image e.symm s).symm.iSup_comp (g := g ∘ (↑))

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

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

Tactic:
apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

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

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

Tactic:
apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ a ⊓ sSup s =
    ⨅ i,
      ⨆ j,
        match i, j with
        | { down := true }, j => a
        | { down := false }, j => ↑j

Tactic:
by simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]

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

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

Tactic:
by_cases hab : a = b
    · simp [hab]
    · rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
      · simp [h₁]
      · simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

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

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

Tactic:
by_cases hab : a = b
    · simp [hab]
    · rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
      · simp [h₁]
      · simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (sInf s)

Tactic:
rw [sInf_eq_argmin_on hs]

Goal state after:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a✝ : WithTop β
⊢ a✝ ∈ s → a✝ ≤ ⊤

Tactic:
_

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
_

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a✝ : WithTop β
⊢ a✝ ∈ lowerBounds s → a✝ ≤ ⊤

Tactic:
_

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a✝¹ : WithTop β
a✝ : a✝¹ ∈ lowerBounds s
⊢ a✝¹ ≤ ⊤
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 α)
haS : a ∈ S
⊢ (if S ⊆ {⊤} then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' S))) ≤ a

Tactic:
split_ifs with h₁

Goal state after:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : S ⊆ {⊤}
⊢ ⊤ ≤ a

case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : ¬S ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
b : WithBot α
⊢ b ∈ (fun a ↦ ↑a) ⁻¹' S → ⊥ ≤ b

Tactic:
_

Goal state after:
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝¹ : WithBot α
haS : ↑a✝¹ ∈ S
b : WithBot α
a✝ : b ∈ (fun a ↦ ↑a) ⁻¹' S
⊢ ⊥ ≤ b
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : ι), x ∈ s → r (f x) z

Tactic:
constructor
  · rcases hs with ⟨y, hy⟩
    refine fun H => ⟨f y, fun x hx => ?_⟩
    rcases eq_or_ne x y with (rfl | hne)
    · apply Std.Refl.refl
    · exact H hx hy hne
  · rintro ⟨z, hz⟩ x hx y hy _
    exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (symm <| hz _ hy)

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
rintro (hf | hf) a b c

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]]

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.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : a < b
⊢ b = c

Tactic:
· refine
      eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)
    simpa [ha, ha.not_ge, mem_uIoc] using h b

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

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

Tactic:
by
  rcases lt_or_ge a b with h | h
  · simp [uIoo_of_lt, h, Ioo_eq_empty_of_le h.le]
  · simp [uIoo_of_ge, h]

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:
_

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✝ : α
⊢ y✝ ∈ f ⁻¹' c → x✝ ≠ y✝ → (fun x y ↦ r x y ∨ r y x) x✝ y✝
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)

Tactic:
obtain ⟨t, ht, hst⟩ := hs₂ hs₁

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : s.OrdConnected
a b : ↑s
⊢ Subtype.val '' Ι a b = Ι ↑a ↑b

Tactic:
by
  simp [uIoc, (Subtype.mono_coe (· ∈ s)).map_inf, (Subtype.mono_coe (· ∈ s)).map_sup]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

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

Tactic:
cases isEmpty_or_nonempty ι

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

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.Tactic.NormNum.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat |↑na| na

Tactic:
Nat.abs_cast

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat (↑na) na
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a : ℤ
b : ℕ
h : IsInt a (Int.negOfNat b)
⊢ -a = ↑b

Tactic:
simp [h.out]

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 : α
⊢ a⁻¹⁻¹ ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹

Tactic:
inv_inv,

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

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

Tactic:
inv_inv,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊓ 1⁻¹ = a ⊓ 1
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:
simp_rw [← one_le_inv']

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1
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:
rw [← one_lt_factorial, h, one_lt_factorial] at hn

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

Goal state before:
pp: i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + n + 1)!

Tactic:
factorial_succ (1 + n),

Goal state after:
i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + n + 1) * (1 + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1).descFactorial (0 + 1) = (n + 1) * n.descFactorial 0

Tactic:
by rw [descFactorial_zero, descFactorial_one, Nat.mul_one]

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

Goal state before:
pp: F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x⁻¹⁻¹ / y) = f (x * y⁻¹)

Tactic:
inv_inv,

Goal state after:
F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x / y) = f (x * y⁻¹)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m

Tactic:
rw [factorial_mul_descFactorial hmn, show n - m = (n - k) - (m - k) by lia, ← Nat.mul_assoc,
      factorial_mul_descFactorial (show m - k ≤ n - k by lia),
      factorial_mul_descFactorial (le_trans hkm hmn)]

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ f (a / a) ≤ f a + f a

Tactic:
exact map_div_le_add _ _ _

Goal state after:
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:
simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]
    congr
    rw [cast_inv_of_ne_zero hq]

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

Goal state before:
pp: k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * (q + 1).pred = 0 + ↑k * (q + 1)

Tactic:
rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
| -(x - ↑z)

Tactic:
rw [← fract_add_floor x]

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
| -(fract x + ↑⌊x⌋ - ↑z)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = c * q.num / (c * ↑q.den)

Tactic:
refine (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left ?_ <| Int.natCast_nonneg q.den).symm

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < c * ↑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
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
⊢ b⁻¹ < a⁻¹ * c

Tactic:
lt_inv_mul_iff₀' ha,

Goal state after:
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
⊢ b⁻¹ * a < c
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : Group G
inst✝ : Torsor G P
⊢ Subsingleton G ↔ Subsingleton P

Tactic:
inhabit P
  exact (Equiv.smulConst default).subsingleton_congr

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ⌈a⌉

Tactic:
by
  rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg ha)]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
⊢ ∀ {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H =
      ↑(List.pmap f l₁ H₁)

Tactic:
_

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
H✝ : ∀ (a : α), a ∈ s₂ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H✝ =
    ↑(List.pmap f l₁ H₁)
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
simp_rw [← cons_zero]
  exact cons_inj_left _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t ≤ s

Tactic:
Multiset.sub_le_iff_le_add

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ≤ s + t