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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds ({a} ∪ s) = Ici a ∩ upperBounds s

Tactic:
upperBounds_union,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds {a} ∩ upperBounds s = Ici a ∩ upperBounds s
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
hs : s.Nonempty
ht : t.Nonempty
ha : IsLUB s a
hb : IsLUB t b
⊢ IsLUB (s ×ˢ t) (a, b)

Tactic:
simp_all +contextual [IsLUB, IsLeast, lowerBounds]

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

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < e

Tactic:
rw [eq]

Goal state after:
A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < ↑n * ⅟↑d
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < e

Tactic:
rw [eq]

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < ↑n * ⅟↑d
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ e ≠ 0

Tactic:
rw [eq]

Goal state after:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ ↑n * ⅟↑d ≠ 0
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a / 2 < a ↔ 0 < a

Tactic:
rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
by
  induction n with
  | zero => rw [pow_zero, replicate_zero, prod_nil]
  | succ n ih => rw [replicate_succ, prod_cons, ih, pow_succ']

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB {0} 0

Tactic:
exact isGLB_singleton

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
simp [division_def, mul_nonpos_iff]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
hn : n ≠ l.length
a : α
⊢ (l.eraseIdx n).insertIdx n a = l.set n a

Tactic:
by
  induction n generalizing l <;> cases l <;> simp_all

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

Goal state before:
pp: case trans
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Tactic:
rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩

Goal state after:
case trans
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
⊢ (Forall₂ r ∘r Perm) l₁✝ v
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n.succ)).prod = f 0 * (map (fun i ↦ f i.succ) (range n)).prod

Tactic:
rw [range_succ_eq_map]
  simp [Function.comp_def]

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

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ ((r, x) ::ᵣ l).eval ≠ 0

Tactic:
unfold eval cons
  apply mul_ne_zero ?_ hl
  simp [zpow'_eq_zero_iff, hx]

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

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ x₁ * x₂ = l.eval

Tactic:
hx₁,

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ l₁.eval * x₂ = l.eval
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ x₁ / x₂ = l.eval

Tactic:
hx₁,

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ l₁.eval / x₂ = l.eval
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
h : l.length = 1
⊢ l.length = [l.get ⟨0, ⋯⟩].length

Tactic:
by convert! h

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

Goal state before:
pp: case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
ext; simp [toNNRat, hp, hq, mul_nonneg]

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

Goal state before:
pp: n : ℤ
hn : 0 < n
⊢ ↑↑n.natAbs.toPNat' = n

Tactic:
Nat.toPNat'_coe,

Goal state after:
n : ℤ
hn : 0 < n
⊢ ↑(if 0 < n.natAbs then n.natAbs else 1) = n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n - q).den = q.den

Tactic:
by
  rw [sub_eq_add_neg, intCast_add_den, neg_den]

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

Goal state before:
pp: case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑q.num / ↑q.den

Tactic:
num_div_den

Goal state after:
case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = q
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
⊢ ↑b = 0

Tactic:
have : Rat.divInt a b = _ := congr_arg NNRat.cast e

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d = 0
this : Rat.divInt ↑a ↑b = ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ ↑b = 0
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
⊢ ⨆ i, f ↑i = ⨆ i, f i

Tactic:
by_cases! htriv : ∀ i, f i = ⊥

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∀ (i : ι), f i = ⊥
⊢ ⨆ i, f ↑i = ⨆ i, f i

case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
⊢ ⨆ i, f ↑i = ⨆ i, f i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
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 ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (f (sSup x✝))

Tactic:
rw [map_sSup]; exact isLUB_biSup

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝ : SemilatticeSup α
x y : ↑(Iic a)
⊢ Codisjoint x y ↔ ↑x ⊔ ↑y = a

Tactic:
simpa only [_root_.codisjoint_iff] using! Iic.eq_top_iff

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ (∀ a_1 ∈ Iic a, ∃ b, Disjoint a_1 ↑b ∧ a_1 ⊔ ↑b = a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
Subtype.exists,

Goal state after:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ (∀ a_1 ∈ Iic a, ∃ a_2, ∃ (_ : a_2 ∈ Iic a), Disjoint a_1 a_2 ∧ a_1 ⊔ a_2 = a) ↔
    ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
⊢ BddAbove s

Tactic:
refine ⟨b, fun x hx ↦ ?_⟩

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
x : α
hx : x ∈ s
⊢ x ≤ b
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False

pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False

Tactic:
· have ab := (h ⟨xa, xb⟩).1.trans xb
      exact lt_irrefl _ (h ⟨h', ab⟩).1

Goal state after:
case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ≤ f a → b' ∈ lowerBounds (f '' Icc a b)

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a

Tactic:
· intro hb'
    rintro _ ⟨x, hx, rfl⟩
    exact hb'.trans <| h' (left_mem_Icc.mpr hab) hx hx.1

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b

Tactic:
by_contra ba

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
⊢ a ≤ b

Tactic:
by_contra ba

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ False
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.coe
α✝ : 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
⊢ ⊤ ≤ ↑a✝

Tactic:
cases h₁ haS

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι c a = Ι a c

pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[c, a]]

Tactic:
uIoc_comm

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι a c = Ι a c

α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[c, a]]
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)

Tactic:
exists_and_left

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsGreatest s a

Tactic:
rintro rfl
    exact ⟨IsAntichain.singleton, isGreatest_singleton⟩

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
⊢ sInf (Subtype.val '' S) ∈ Icc a b

Tactic:
refine ⟨le_csInf (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.1), ?_⟩

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) ≤ b
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S = ∅
⊢ IsGLB S ⟨b, ⋯⟩

Tactic:
subst hS; simp only [isGLB_empty_iff, isTop_iff_eq_top]; rfl

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)
⊢ IsGLB S (if hS : S = ∅ then ⟨b, ⋯⟩ else ⟨sInf (Subtype.val '' S), ⋯⟩)

Tactic:
by
    split_ifs with hS
    · subst hS; simp only [isGLB_empty_iff, isTop_iff_eq_top]; rfl
    · exact .of_image Subtype.coe_le_coe <| isGLB_csInf ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddBelow (OrderBot.bddBelow S))

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)

Tactic:
factorial_mul_descFactorial h

Goal state after:
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
⊢ 1 + (↑n - 1) = ↑n

Tactic:
add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2

Goal state after:
n : ℕ+
⊢ ↑n = ↑n
Module: Mathlib.Data.PNat.Basic

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

Tactic:
change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)

Goal state after:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * (q + 1).pred = 0 + ↑k * (q + 1)
Module: Mathlib.Algebra.Order.Round

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

Tactic:
rw [sub_eq_add_neg]
  norm_cast
  rw [round_add_intCast, sub_eq_add_neg]

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 : ℤ
⊢ |x - ↑(round x)| ≤ |x - ↑z|

Tactic:
by
  rw [abs_sub_round_eq_min, min_le_iff]
  rcases le_or_gt (z : α) x with (hx | hx) <;> [left; right]
  · conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]
    simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx
  · rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]
    conv_rhs => rw [← fract_add_floor x]
    rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
      le_sub_comm]
    norm_cast
    rwa [le_sub_one_iff, floor_lt]

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

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑(n * (m / n))

Tactic:
rw [← Nat.cast_add, Nat.mod_add_div m n]

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

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

Tactic:
by
  change -⌊-q⌋ = _
  rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]

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

Goal state before:
pp: n : ℤ
d : ℕ
| - -⌈↑n / ↑d⌉

Tactic:
← floor_neg

Goal state after:
n : ℤ
d : ℕ
| -⌊-(↑n / ↑d)⌋
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = ↑(-(-↑n / ↑d)).toNat

Tactic:
rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast, Int.cast_natCast,
    Int.natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg))]

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

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

Tactic:
ring

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

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

Tactic:
· rintro (rfl | rfl)
    exacts [nil_subperm, Subperm.refl _]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
⊢ (t + s).erase a = s.erase a + t

Tactic:
erase_add_right_neg s h,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
⊢ t + s.erase a = s.erase a + t
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ ↑l = ↑l'

Tactic:
exact Multiset.Nodup.toFinset_inj hl hl' h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
s : Finset α
hx : x ∈ s
⊢ s.erase x = s.erase y ↔ x = y

Tactic:
by
  grind [eq_of_mem_of_notMem_erase]

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

Goal state before:
pp: α : Type u_2
a b : α
⊢ Disjoint {a} {b} ↔ a ≠ b

Tactic:
rw [disjoint_singleton_left, mem_singleton]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a s ∪ t = s ∪ insert a t

Tactic:
rw [insert_union, union_insert]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Set α
⊢ ↑s.toFinset = s

Tactic:
exact s.coe_toFinset

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

Goal state before:
pp: α : Sort u_1
k l k' l' : ℕ
h : k = l
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin l → Fin l' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
by
  subst h
  subst h'
  simp [funext_iff]

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

Goal state before:
pp: k l : ℕ
h : k = l
i : Fin k
j : Fin l
⊢ i ≍ j ↔ ↑i = ↑j

Tactic:
by
  subst h
  simp [val_eq_val]

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

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
hkb : k ≤ ↑b
⊢ b = a + ⟨k, ⋯⟩

Tactic:
simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ b = a + ⟨k, ⋯⟩ + 1

Tactic:
simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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

Goal state before:
pp: n m : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero (OfNat.ofNat m)
⊢ NeZero (OfNat.ofNat m)

Tactic:
by
  suffices m % (n + m) = m by simpa [neZero_iff, Fin.ext_iff, OfNat.ofNat, this] using! NeZero.ne m
  apply Nat.mod_eq_of_lt
  simpa using! zero_lt_of_ne_zero (NeZero.ne n)

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

Goal state before:
pp: case inr
n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
h' : a < b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1

Tactic:
grind [castPred, val_sub_castLT_of_lt]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
⊢ a.succAbove (last n) = last (n + 1)

Tactic:
succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h),

Goal state after:
n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
⊢ (last n).succ = last (n + 1)
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (f ∘ ⇑σ) ~ ofFn f

Tactic:
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
  exact σ.map_finRange_perm.map f

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, #t = 2 + 1) ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
reduceAdd,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, #t = 3) ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
exists_and_left

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, #t = 3 + 1) ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
reduceAdd,

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ t ⊆ s, #t = 4) ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
exists_and_left

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

Goal state before:
pp: P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst✝ : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α

Tactic:
induction n using Nat.strong_induction_on generalizing α with

Goal state after:
case h
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
⊢ P α