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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a + c - (d + b) = a + c - (b + d)

Tactic:
add_comm d

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a + c - (b + d) = a + c - (b + d)
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
⊢ Nat.find h₁ = Nat.find h₂ + 1

Tactic:
refine (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn ↦ ?_⟩

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find h₂ + 1
⊢ ¬p n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ ⌊1⌋₊ = 1

Tactic:
rw [← Nat.cast_one, floor_natCast]

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
⊢ Nat.cast ⁻¹' Ici a = Ici ⌈a⌉₊

Tactic:
ext
  simp [ceil_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
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_ge <| h₀.not.mp ha.not_ge)]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 1) * (a + b) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) := by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ (a + b) ^ (n + n) ≤ 2 ^ (n + n - 1) * (a ^ (n + n) + b ^ (n + n))

Tactic:
rw [← two_mul, pow_mul]

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ ((a + b) ^ 2) ^ n ≤ 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
n0 : n ≤ 0
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
· obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
    rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]
    exact mabs_pow m _

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

Goal state before:
pp: ι : Sort x
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
F : ι → α × β
⊢ BddAbove (range F) ↔ BddAbove (range (Prod.fst ∘ F)) ∧ BddAbove (range (Prod.snd ∘ F))

Tactic:
simp only [bddAbove_prod, ← range_comp]

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

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t

Tactic:
by rcases le_total a b with h | h <;> simp [h, ha.1, hb.1]

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]
  apply Nat.cast_pos.2
  simpa using! w

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
by
  simpa using inv_lt_inv_of_neg (inv_lt_zero'.2 ha) hb

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
by
  rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab✝ : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab : d < a' * b
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', d_ab⟩ := exists_lt_mul_right_of_nonneg ha'.1 hd d_ab

Goal state after:
case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab✝¹ : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab✝ : d < a' * b
b' : α
hb' : b' ∈ Set.Ico 0 b
d_ab : d < a' * b'
⊢ d ≤ c
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b [] → SublistForall₂ Rₐ a []

Tactic:
rintro _ _ h1 h2
      cases h2
      exact h1

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

Tactic:
· simp [h]

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

Goal state before:
pp: case mp
α : Type u
l : List α
a : α
⊢ l <+ [a] → l = [] ∨ l = [a]

Tactic:
rintro (_ | _)

Goal state after:
case mp.cons
α : Type u
l : List α
a : α
a✝ : l <+ []
⊢ l = [] ∨ l = [a]

case mp.cons_cons
α : Type u
a : α
l₁✝ : List α
a✝ : l₁✝ <+ []
⊢ a :: l₁✝ = [] ∨ a :: l₁✝ = [a]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr
α : Type u
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+ [a]

Tactic:
rintro (_ | _)

Goal state after:
case mpr.inl
α : Type u
l : List α
a : α
h✝ : l = []
⊢ l <+ [a]

case mpr.inr
α : Type u
l : List α
a : α
h✝ : l = [a]
⊢ l <+ [a]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l

Tactic:
revert a b
    induction l <;> intros <;> [rfl; simp only [*, foldl]]

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.den * q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den) * q₁.den.lcm q₂.den

Tactic:
← Nat.gcd_mul_lcm,

Goal state after:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den ∣
    (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den.gcd q₂.den * q₁.den.lcm q₂.den) * q₁.den.lcm q₂.den
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * b + a * c

Tactic:
apply self_le_add_right

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

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ b * a + c * a

Tactic:
apply self_le_add_right

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ max a b = b

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ max a b = a

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ max a b = a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi

Tactic:
by
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind` -/
  simp_all

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Tactic:
by
  rw [← compl_compl (⋂₀ S), compl_sInter]

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
ι : α → Type u_13
s : (a : α) → Set (ι a)
t : (a : α) → ι a → Set (π a)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ x ∈ univ.pi s, univ.pi fun a ↦ t a (x a)) ↔ x✝ ∈ univ.pi fun a ↦ ⋃ j ∈ s a, t a j

Tactic:
simp [Classical.skolem, forall_and]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s))
⊢ ↑(sInf s) = ↑(sInf ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s))

Tactic:
rw [preimage_image_eq]

Goal state after:
case neg.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s))
⊢ Injective fun a ↦ ↑a
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
    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.CompleteBooleanAlgebra

Goal state before:
pp: case pos
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

pp: case neg
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : ¬i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
· exact le_iSup₂_of_le i ⟨his, hij ▸ hjs⟩ inf_le_left

Goal state after:
case neg
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : ¬i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
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
    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.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 : β
hb : b ∈ ⇑φ '' s
b' : β
hb' : b' ∈ ⇑φ '' s
⊢ b ≠ b' → r'ᶜ b b'

Tactic:
h₁

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
b' : β
hb' : b' ∈ ⇑φ '' s
h₁ : b ≠ b'
⊢ r'ᶜ b b'
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B

Tactic:
· exact (Subtype.mono_coe (· ∈ s)).csSup_image_le ⟨c, hct⟩ hB

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬¬S.Nonempty
⊢ sSup (Subtype.val '' S) ∈ Icc a b

Tactic:
not_not

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S.Nonempty
⊢ sSup (Subtype.val '' S) ∈ Icc a b
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬¬S.Nonempty
⊢ sInf (Subtype.val '' S) ∈ Icc a b

Tactic:
not_not

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S.Nonempty
⊢ sInf (Subtype.val '' S) ∈ Icc a b
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
by
  cases hn
  · rw [factorial_one]
    exact lt_factorial_self (succ_le_succ hi)
  exact add_factorial_succ_lt_factorial_add_succ _ hi

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

Goal state before:
pp: case succ
l k n' : ℕ
⊢ (n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k = (n' + 1).ascFactorial (l + k)

Tactic:
apply Nat.mul_left_cancel (factorial_pos n')
    simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
    rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]

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

Goal state before:
pp: n : ℕ
x✝ : 0 ≤ n
⊢ (n - 0)! = n !

Tactic:
Nat.sub_zero

Goal state after:
n : ℕ
x✝ : 0 ≤ n
⊢ n ! = n !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ descFactorial = descFactorialBinary

Tactic:
ext n k
  rw [descFactorialBinary]
  split_ifs with h
  · rw [descFactorial_of_lt h]
  · rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']
    grind

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

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 2 * fract x ∈ Ico 0 1

pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
· simp [h]

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1
Module: Mathlib.Data.Rat.Floor

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

Tactic:
num_neg_eq_neg_num,

Goal state after:
q : ℚ
⊢ -(-q.num / ↑(-q).den) = -(-q.num / ↑q.den)
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
n : ℕ
a : ℤ
⊢ ⌈↑n⌉ ≤ a ↔ ↑n ≤ a

Tactic:
rw [ceil_le, ← cast_natCast, cast_le]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ⌈a - ↑n⌉ = ⌈a⌉ - ↑n

Tactic:
convert ceil_sub_intCast a n

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ ↑n = ↑↑n
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 : R
⊢ ↑⌈a⌉ < a + 1

Tactic:
rw [← lt_ceil, ← Int.cast_one, ceil_add_intCast]
  apply lt_add_one

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case inr.inr
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 : 0 < n
⊢ R (f x) (f y)

Tactic:
trans f (l + (1 : ℤ) • a)

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 : 0 < n
⊢ R (f x) (f (l + 1 • a))

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 : 0 < n
⊢ R (f (l + 1 • a)) (f y)
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
⊢ Int.cast ⁻¹' Ici a = Ici ⌈a⌉

Tactic:
ext
  simp [ceil_le]

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g₁ g₂ : G
p : P
h : g₁ • p = g₂ • p
⊢ g₁ = g₂

Tactic:
← smul_sdiv g₁ p,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g₁ g₂ : G
p : P
h : g₁ • p = g₂ • p
⊢ g₁ • p /ₛ p = g₂
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inr.refine_2
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⁻¹
⊢ c ^ (-↑n) < b

Tactic:
inv_lt_comm₀ hb₀ (pow_pos hc₀ n),

Goal state after:
case inr.inr.inr.refine_2
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₁ : (c ^ n)⁻¹ < b
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
⊢ f (c • 1) = f 1

Tactic:
simp only [smul, f.map_one, smul_one]

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

Goal state before:
pp: case refine_1
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
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q₁ < ↑q ^ n

Tactic:
assumption_mod_cast

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

Goal state before:
pp: case refine_2
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
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q ^ n < ↑q₂

Tactic:
assumption_mod_cast

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

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

Tactic:
← coe_count,

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = count a ↑(List.replicate n a)
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)

Tactic:
← coe_count,

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = count a ↑(List.replicate n ?convert_1)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
IH : l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i
hl : (a :: l).Nodup
i : ℕ
h : i < (a :: l).length
⊢ (a :: l).erase (a :: l)[i] = (a :: l).eraseIdx i

Tactic:
cases i with
    | zero => simp
    | succ i => grind

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

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

Tactic:
obtain ⟨t, rfl⟩ := ih

Goal state after:
case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ a, map f a = f y ::ₘ map f t