mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = r.mapOfSurjective f h hf

Tactic:
by
  rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]; rfl

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ sSup S = conGen fun x y ↦ ∃ c ∈ S, c x y

Tactic:
rw [sSup_def]

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ conGen (sSup (DFunLike.coe '' S)) = conGen fun x y ↦ ∃ c ∈ S, c x y
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ (↑x * ↑y = 1) = (↑x' * ↑y' = 1)

Tactic:
c.eq.2 hx,

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ (↑x' * ↑y = 1) = (↑x' * ↑y' = 1)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2.refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y * ↑x = 1) = (↑y' * ↑x' = 1)

Tactic:
c.eq.2 hx,

Goal state after:
case refine_2.refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y * ↑x' = 1) = (↑y' * ↑x' = 1)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x✝¹
snd_eq✝¹ : x✝² = x✝
tail_eq✝ : x✝⁵ = x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : (!x✝²) = !x✝
⊢ [] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
subst_vars

Goal state after:
α : Type u
x✝² : List (α × Bool)
x✝¹ : α
x✝ : Bool
fst_eq✝ : x✝¹ = x✝¹
snd_eq✝ : (!x✝) = !x✝
⊢ [] ++ x✝² = [] ++ x✝² ∨ ∃ L₅, Step ([] ++ x✝²) L₅ ∧ Step ([] ++ x✝²) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x3
snd_eq✝¹ : x✝² = b3
tail_eq✝ : x✝⁵ = (x✝¹, !x✝) :: x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : (!x✝²) = x✝
⊢ [] ++ x✝⁵ = [(x3, b3)] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([(x3, b3)] ++ x✝⁴) L₅

Tactic:
subst_vars

Goal state after:
α : Type u
x✝² : List (α × Bool)
x✝¹ : Bool
x✝ : α
⊢ [] ++ (x✝, !!x✝¹) :: x✝² = [(x✝, x✝¹)] ++ x✝² ∨
    ∃ L₅, Step ([] ++ (x✝, !!x✝¹) :: x✝²) L₅ ∧ Step ([(x✝, x✝¹)] ++ x✝²) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x3 = x✝¹
snd_eq✝¹ : b3 = x✝
tail_eq✝ : (x✝³, !x✝²) :: x✝⁵ = x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : x✝² = !x✝
⊢ [(x3, b3)] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([(x3, b3)] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
subst_vars

Goal state after:
α : Type u
x✝² : List (α × Bool)
x✝¹ : α
x✝ : Bool
⊢ [(x✝¹, x✝)] ++ x✝² = [] ++ (x✝¹, !!x✝) :: x✝² ∨
    ∃ L₅, Step ([(x✝¹, x✝)] ++ x✝²) L₅ ∧ Step ([] ++ (x✝¹, !!x✝) :: x✝²) L₅
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
a b : ι
h : a ≠ b
⊢ ∏ x ∈ {a, b}, f x = f a * f b

Tactic:
prod_insert (notMem_singleton.2 h),

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
a b : ι
h : a ≠ b
⊢ f a * ∏ x ∈ {b}, f x = f a * f b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x3
snd_eq✝¹ : x✝² = b3
tail_eq✝ : x✝⁵ = tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
fst_eq✝ : x✝³ = x4
snd_eq✝ : (!x✝²) = b4
⊢ [] ++ x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁴) L₅

Tactic:
subst_vars

Goal state after:
α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ [] ++ tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴) = (x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)) L₅ ∧ Step ((x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x3 = x✝¹
snd_eq✝¹ : b3 = x✝
tail_eq✝ : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = x✝⁴
fst_eq✝ : x4 = x✝¹
snd_eq✝ : b4 = !x✝
⊢ (x3, b3) :: (x4, b4) :: tl ++ x✝⁵ = [] ++ x✝⁴ ∨
    ∃ L₅, Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
subst_vars

Goal state after:
α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ (x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴ = [] ++ tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴) ∨
    ∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴) L₅ ∧ Step ([] ++ tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴)) L₅
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
⊢ (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x

Tactic:
prod_filter_mul_prod_filter_not

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refl
α : Type u
p : α × Bool
LL₁ LL₂ L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

Tactic:
subst_vars

Goal state after:
case refl
α : Type u
p : α × Bool
LL₁ L₁ L₂ : List (α × Bool)
eq₂ : p :: L₂ = p :: L₁
⊢ Red L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case head
α : Type u
p : α × Bool
LL₁ LL₂ a✝ c✝ : List (α × Bool)
h₁₂ : Step a✝ c✝
h : ReflTransGen Step c✝ LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = c✝ → p :: L₂ = LL₂ → Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = a✝
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

Tactic:
subst_vars

Goal state after:
case head
α : Type u
p : α × Bool
LL₁ c✝ L₁ L₂ : List (α × Bool)
h : ReflTransGen Step c✝ (p :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, p :: L₁ = c✝ → p :: L₂_1 = p :: L₂ → Red L₁ L₂_1
h₁₂ : Step (p :: L₁) c✝
⊢ Red L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < sizeOf ((x, b) :: (x, !b) :: L2)

Tactic:
cons.sizeOf_spec,

Goal state after:
case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + sizeOf (x, b) + sizeOf ((x, !b) :: L2)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
P : Submonoid M
Q : Submonoid N
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
obtain ⟨bM, hbM⟩ := hP

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
P : Submonoid M
Q : Submonoid N
hQ : Q.FG
bM : Finset M
hbM : closure ↑bM = P
⊢ (P.prod Q).FG
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG G

Tactic:
rintro ⟨S, hfin : Finite S, φ, hφ⟩
    exact Group.fg_of_surjective hφ

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : FreeAbelianGroup α
⊢ (map id) x = x

Tactic:
by
  rw [map_id]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
ih : of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
⊢ -of L1 * of L2 * of L3 = -of L1 * (of L2 * of L3)

Tactic:
rw [neg_mul, neg_mul, neg_mul, ih]

Goal state after:
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 → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P r₁ s₁ = P r₂ s₂

Tactic:
rw [hP r₁ v s₁ s₁vS, hP r₂ u s₂ (by norm_cast; rwa [hs₂]), ← hr₂]

Goal state after:
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 → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P (u • r₂) ⟨v * ↑s₁, s₁vS⟩ = P (↑u • r₂) ⟨↑u * ↑s₂, ⋯⟩
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * ↑x.2 * y.1 = u * ↑y.2 * x.1

Tactic:
by rw [mul_assoc, mul_assoc, ← e]

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

Goal state before:
pp: case inr
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
inj : Injective ⇑k
⊢ z = w

Tactic:
· apply (f.map_units x).mul_right_cancel
    rw [hxz, hxw, hg (inj this)]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : Mul α
inst✝⁷ : Add α
inst✝⁶ : LE α
inst✝⁵ : Mul β
inst✝⁴ : Add β
inst✝³ : LE β
inst✝² : Mul γ
inst✝¹ : Add γ
inst✝ : LE γ
f g : α ≃+*o β
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
    congr

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S'✝ : Type u_6
inst✝⁶ : NonUnitalNonAssocSemiring R✝
inst✝⁵ : NonUnitalNonAssocSemiring S✝
f✝ : R✝ ≃+* S✝
x : R✝
inst✝⁴ : FunLike F R✝ S✝
R : Type u_7
R' : Type u_8
S : Type u_9
S' : Type u_10
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring R'
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
f : R ≃+* R'
g : S ≃+* S'
x✝¹ x✝ : R × S
⊢ ((↑f).prodCongr ↑g).toFun (x✝¹ * x✝) = ((↑f).prodCongr ↑g).toFun x✝¹ * ((↑f).prodCongr ↑g).toFun x✝

Tactic:
by
    simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, map_mul, Prod.mk_mul_mk]

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

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ ↑x * a < ↑x * ⊥

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ ↑x * a < ↑x * ↑a✝

Tactic:
· exact absurd h not_lt_bot

Goal state after:
case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ ↑x * a < ↑x * ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ a * ↑x < ⊥ * ↑x

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ a * ↑x < ↑a✝ * ↑x

Tactic:
· exact absurd h not_lt_bot

Goal state after:
case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ a * ↑x < ↑a✝ * ↑x
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
succ_le_iff_of_not_isMax ha,

Goal state after:
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ a < b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f (succ a) = succ (f a)

Tactic:
rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a = b → a ⋖ b

Tactic:
by rintro rfl; exact covBy_succ _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ b < succ a ↔ b ≤ a

Tactic:
contrapose!
  exact succ_le_iff_of_not_isMax ha

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
succ_le_iff_of_not_isMax ha,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ a < succ b ↔ a ≤ b
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
n a✝ : ℕ
⊢ (↑a✝ - ↑n).toNat = (↑a✝).toNat - (↑n).toNat

Tactic:
rw [← natCast_sub, toNat_natCast, toNat_natCast, toNat_natCast]

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

Goal state before:
pp: c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ c * a

Tactic:
by
  rw [mul_comm]
  exact ENat.self_le_mul_right a hc

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | p x})
_hx : x ∈ univ
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝² : CommMonoid M
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred fun x ↦ ¬p x
f : (x : ι) → p x → γ
g : (x : ι) → ¬p x → γ
h : γ → M
x : ↥({x ∈ s | ¬p x})
_hx : x ∈ univ
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s✝ : Finset ι
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | p x})
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s✝ : Finset ι
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Goal state after:
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
⊢ (fun {α} ↦ η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α} ↦ η.app α

Tactic:
ext y

Goal state after:
F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
y : F α
⊢ ((fun {α} ↦ η.app α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} ↦ η.app α) y
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b a : α
s : Sym α n
⊢ (a ::ₘ ↑s).card = n.succ

Tactic:
rw [Multiset.card_cons, s.2]

Goal state after:
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:
rw [← cons_head_tail v]
    simp [← get_zero, get_eq_get_toList]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #({x ∈ T | x.length = s}) ≤ #(image List.ofFn univ)

Tactic:
apply Finset.card_le_card
          intro a ha
          let hlen := Finset.mem_filter.mp ha
          exact Finset.mem_image.mpr ⟨
              (fun j : Fin s => a.get ⟨j.val, by simp [hlen]⟩),
              by simp,
              List.ext_get (by simp [hlen]) (by simp)⟩

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

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u1} ↑t
⊢ Small.{u, u1} ↑(s ∪ t)

Tactic:
rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]
  infer_instance

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

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
s : ℕ → ↑S
hs : Surjective s
⊢ ⨆ n, (fun n ↦ ↑(s n)) n = ⊤

Tactic:
hs.iSup_comp,

Goal state after:
case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
s : ℕ → ↑S
hs : Surjective s
⊢ ⨆ y, ↑y = ⊤
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hs : s.Countable
⊢ {t | t.Finite ∧ t ⊆ s}.Countable

Tactic:
by
  have := hs.to_subtype
  refine (countable_range fun t : Finset s => Subtype.val '' (t : Set s)).mono ?_
  rintro t ⟨ht, hts⟩
  lift t to Set s using hts
  lift t to Finset s using ht.of_finite_image Subtype.val_injective.injOn
  exact mem_range_self _

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
by
        obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)
        · exact (not_inl_lt_inr hb).elim
        · exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t (f.trans g).top g.top

Tactic:
apply PrincipalSeg.lt_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ⇑(⨅ i, f i) = ⨅ i, ⇑(f i)

Tactic:
by
  funext x; simp [iInf_apply]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ lowerBounds {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, o.get ⋯ = a) → p ∧ ∃ h, o.get h = a

pp: case mpr
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ h, o.get h = a) → ∃ h_1, o.get ⋯ = a

Tactic:
· rintro ⟨h₀, h₁⟩
    exact ⟨h₀, ⟨_, h₁⟩⟩

Goal state after:
case mpr
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ h, o.get h = a) → ∃ h_1, o.get ⋯ = a
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h : c₀ ≤ c₁
i : ℕ
⊢ c₀ i ≤ ωSup c₁

Tactic:
obtain ⟨_, h⟩ := h i
    exact le_trans h (le_ωSup _ _)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}

Tactic:
exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ z ∈ c, f z ≤ y
⊢ False

Tactic:
apply lt_irrefl y (lt_of_lt_of_le hy' ?_)

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
h : ∀ z ∈ c, f z ≤ y
⊢ cSup c ≤ y