mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
ih : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
e : Option (ULift.{?u.79, 0} (Fin n)) ≃ ULift.{?u.82, 0} (Fin n.succ)
⊢ P (ULift.{u, 0} (Fin n)) → P (ULift.{u, 0} (Fin (n + 1)))

Tactic:
intro ih

Goal state after:
α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
ih✝ : Trunc (P (ULift.{u, 0} (Fin n)))
this : card (Option (ULift.{?u.79, 0} (Fin n))) = card (ULift.{?u.82, 0} (Fin n.succ))
e : Option (ULift.{?u.79, 0} (Fin n)) ≃ ULift.{?u.82, 0} (Fin n.succ)
ih : P (ULift.{u, 0} (Fin n))
⊢ P (ULift.{u, 0} (Fin (n + 1)))
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (⨆ i, f ↑i)

Tactic:
← sSup_image'

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
rw [he i hi, mem_empty_iff_false] at hx
    contradiction

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (⨆ i, f ↑i)

Tactic:
← sSup_image'

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f ≤ a ↔ sSup (f '' ↑s) ≤ a

Tactic:
by
    simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
this : Nonempty ι
⊢ a ⋖ b

Tactic:
refine covBy_iff_wcovBy_and_lt.2 ⟨wcovBy_iff_antisymmRel.2 ⟨i, hi.wcovBy, h⟩, ?_⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
this : Nonempty ι
⊢ a < b
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ (x ∈ if h : ⟨i, a⟩.fst = ⟨j, b⟩.fst then map (Embedding.sigmaMk ⟨j, b⟩.fst) (f (h ▸ ⟨i, a⟩.snd) ⟨j, b⟩.snd) else ∅) ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Tactic:
dif_neg h

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ ∅ ↔ ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ t, t.Subsingleton ∧ IsCofinal t

Tactic:
obtain ⟨a, ha⟩ := hs.exists_maximal hn
    use {a}
    suffices IsTop a by simpa [IsCofinal]
    intro b
    obtain ⟨c, hc, hbc⟩ := hs' b
    exact hbc.trans (ha.le hc)

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x ↦ x ∈ s) x
y : α
hy : y ∈ s
⊢ y ≤ x → x ≤ y

Tactic:
exact hx.le_of_le hy

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hca : c ≤ a
⊢ {x ∈ Finset.Ico a b | x < c}.val = ∅

Tactic:
Finset.Ico_filter_lt_of_le_left hca

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hca : c ≤ a
⊢ ∅.val = ∅
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
· rcases ht with ⟨m, mt⟩
    exact ⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 : ∀ m < n, f m = Classical.choose ⋯ m
h2 : IsBadSeq r s (Classical.choose ⋯)
h3 : rk (Classical.choose ⋯ n) = Nat.find h
⊢ IsBadSeq r s (Classical.choose ⋯)

Tactic:
by convert! h2

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g = g * h

Tactic:
← mul_inv_eq_iff_eq_mul

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ = g
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, hmul _ _ _ _ Cx Cy⟩

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | x ∈ map (⇑f) s}.Pairwise Commute

Tactic:
simp only [Multiset.mem_map]
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _
  exact (comm.of_refl hx hy).map f

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Normal
⊢ (sSup Hs).Normal

Tactic:
by
  rw [sSup_eq_iSup]
  exact biSup_normal Hs id h

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

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
⊢ Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b

Tactic:
simpa only [disjoint_comm (a := a)] using disjoint_sum_left

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

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ ⊤ ≤ s ↔ ∀ (x y : α), s x y

Tactic:
Setoid.le_def,

Goal state after:
α : Type u_1
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → s x y) ↔ ∀ (x y : α), s x y
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ f (of x) = 0

Tactic:
rw [h, map_zero]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ g (↑c * y) * ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ = g y

Tactic:
mul_inv_left hg,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ g (↑c * y) = g ↑c * g y
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec (x * y)).2)⁻¹ =
    g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹ *
      (g (f.sec y).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec y).2)⁻¹)

Tactic:
mul_inv_left hg,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 =
    g ↑(f.sec (x * y)).2 *
      (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹ *
        (g (f.sec y).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec y).2)⁻¹))
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ w * g (f.sec z).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec z).2)⁻¹ = v ↔
    g (f.sec z).1 * w = g ↑(f.sec z).2 * v

Tactic:
mul_inv_left hg,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ w * g (f.sec z).1 = g ↑(f.sec z).2 * v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * ↑s₂ ∈ S
⊢ P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩

Tactic:
have := hP r₁ 1 s₁ (by simp) r₂ t₂ s₂ ht₂
      simp [this]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ (f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1

Tactic:
by
  rw [lift_apply, mul_assoc, ← g.domRestrict_apply, IsUnit.liftRight_inv_mul, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ Surjective ⇑(f.lift hg) → ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1

Tactic:
intro H v
    obtain ⟨z, hz⟩ := H v
    obtain ⟨x, hx⟩ := f.surj z
    use x
    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.domRestrict_apply, IsUnit.mul_liftRight_inv (g.domRestrict S) hg, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ g x.1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) x.2)⁻¹ = v

Tactic:
mul_inv_left hg,

Goal state after:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1
v : P
x : M × ↥S
hx : v * g ↑x.2 = g x.1
⊢ g x.1 = g ↑x.2 * v
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
r✝ : X
s✝ : ↥S
⊢ (r • 1) • (r✝ /ₒ s✝) = r • (r✝ /ₒ s✝)

Tactic:
simp only [smul_oreDiv, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
rcases le_total_of_codirected h₁ h₂ with h | h

Goal state after:
case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
h : IsSuccPrelimit a
x✝ : ↑(Iio a)
b : α
hb : b ∈ Iio a
c : α
hbc : b < c
hca : c < a
⊢ ∃ b_1, ⟨b, hb⟩ < b_1

Tactic:
exact ⟨⟨c, hca⟩, hbc⟩

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case zero
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ^[0] b)
hb : b ≤ succ^[0] b
⊢ succ^[0] b ≤ b

Tactic:
exact le_rfl

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
⊢ ¬IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a

Tactic:
by
  rw [not_isSuccPrelimit_iff]
  refine exists_congr fun b ↦ ⟨fun hba ↦ ⟨hba.lt.not_isMax, hba.succ_eq⟩, ?_⟩
  rintro ⟨h, rfl⟩
  exact covBy_succ_of_not_isMax h

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ (if h : IsSuccPrelimit (Order.succ b) then
      isSuccPrelimit (Order.succ b) h fun y x ↦
        ⋯.fix
          (fun a IH ↦
            if h : IsSuccPrelimit a then isSuccPrelimit a h IH
            else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
          y
    else
      cast ⋯
        (succ (Classical.choose ⋯) ⋯
          ((fun y x ↦
              ⋯.fix
                (fun a IH ↦
                  if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                  else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
                y)
            (Classical.choose ⋯) ⋯))) =
    succ b hb (prelimitRecOn b succ isSuccPrelimit)

Tactic:
dif_neg h

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ cast ⋯
      (succ (Classical.choose ⋯) ⋯
        ((fun y x ↦
            ⋯.fix
              (fun a IH ↦
                if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
              y)
          (Classical.choose ⋯) ⋯)) =
    succ b hb (prelimitRecOn b succ isSuccPrelimit)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : ⟨b, hb⟩ < ⟨c, hc⟩
⊢ ⟨b, hb⟩ ≤ if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩

Tactic:
rw [Subtype.mk_lt_mk] at h

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
⊢ ⟨b, hb⟩ ≤ if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

Tactic:
simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ min n i + min (n - i) n = n

Tactic:
by omega

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Tactic:
← cons_head_tail v

Goal state after:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b

Tactic:
← cons_head_tail v

Goal state after:
case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b (v.head ::ᵥ v.tail)).head = b
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
x : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ (fun x ↦ toLex (x, default)) ((fun x ↦ (ofLex x).1) (toLex (a, b))) = toLex (a, b)

Tactic:
simpa using Unique.default_eq b

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
x : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ (fun x ↦ toLex (default, x)) ((fun x ↦ (ofLex x).2) (toLex (a, b))) = toLex (a, b)

Tactic:
by simpa using Unique.default_eq a

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: a : Cardinal.{u}
⊢ Nonempty (Quotient.out (lift.{v, u} a) ≃ Quotient.out a)

Tactic:
by
  rw [← mk_out a, ← mk_uLift, mk_out]
  exact ⟨outMkEquiv.trans Equiv.ulift⟩

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst✝ : IsWellOrder β s
f✝ : r ≼i s
f : r ≃r s
⊢ ∃ γ t, IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
exact ⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuous Prod.fst

Tactic:
by
  simp_rw [← scottContinuousOn_univ, ScottContinuousOn.fst]

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r

Tactic:
rw [maxChain_spec.right this (subset_insert _ _)]
      exact mem_insert _ _

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
⊢ ψ (φ x) = χ x

Tactic:
rw [← h.comp_eq, Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ (n + 1))

Tactic:
rw [pow_succ']
    exact (ra.smul_iff (a ^ n)).mpr hn

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c

Tactic:
apply exists_congr

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ ∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (r s : R) (x : A), (r + s) • x = r • x + s • x

Tactic:
by simp [smul_def', add_mul]

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ ((s + s') • f) m = (s • f + s' • f) m

Tactic:
by
    simp_rw [AddMonoidHom.add_apply, DomMulAct.smul_addMonoidHom_apply, ← map_add, ← add_smul]; rfl

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
x✝¹ : M →+ M₂
x✝ : M
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
DomMulAct.smul_addMonoidHom_apply

Goal state after:
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
x✝¹ : M →+ M₂
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm 0 • x✝) = 0 x✝
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ f (a ⊔ b) = f a ⊔ f b

Tactic:
← sSup_pair,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ f (sSup {a, b}) = f a ⊔ f b