mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mp.cons
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
p : α × Bool
s' : List (α × Bool)
hL : (a, b) :: L₁ = p :: s' ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)

Tactic:
simp_all

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∀ a ∈ s₁ \ s₂, a ∉ s₁ ∩ s₂ → f a = 1

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝

Tactic:
simp_all

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∀ a ∈ s₂ \ s₁, a ∉ s₂ ∩ s₁ → g a = 1

Tactic:
simp_all

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
this : ∏ x ∈ map (Embedding.subtype p) (Finset.subtype p s), f x = ∏ x ∈ Finset.subtype p s, f ((Embedding.subtype p) x)
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s with p x, f x

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
N : Submonoid M
⊢ FG ↥N ↔ N.FG

Tactic:
conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]
  exact ⟨fun h ↦ h.fg_top.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a✝ b✝ : { N // N.Normal }
x : G
h : 1⁻¹ * x ∈ ↑a✝ → 1⁻¹ * x ∈ ↑b✝
x✝ : x ∈ ↑a✝
⊢ x ∈ ↑b✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG

Tactic:
Subgroup.fg_iff_submonoid_fg

Goal state after:
H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
hx' : g x hx = x
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
| inl hx' =>

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : WellQuasiOrderedLE M
inst✝³ : IsOrderedCancelMonoid M
inst✝² : CanonicallyOrderedMul M
inst✝¹ : Monoid N
inst✝ : IsCancelMul N
f g : M →* N
⊢ ∀ x ∈ f.eqLocusM g, ∀ (y : M), x * y ∈ f.eqLocusM g → y ∈ f.eqLocusM g

Tactic:
simp_all

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
⊢ ∏ j, ∏ i, f ↑i = ∏ i, f i

Tactic:
by
  rw [← Finset.prod_fiberwise _ g f]
  congr with j
  exact (prod_subtype _ (by simp) _).symm

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
inst✝ : Mul α
x y : α
⊢ (lift fun x₁ ↦ of (x₁ * y)) (of x) = of (x * y)

Tactic:
lift_apply_of

Goal state after:
α : Type u
inst✝ : Mul α
x y : α
⊢ of (x * y) = of (x * y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = ∑ x ∈ s.toFinset, k • (count x s / k) • {x}

Tactic:
h₂,

Goal state after:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = ∑ x ∈ s.toFinset, count x s • {x}
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ normalizer ↑K ↔ ⁅H, K⁆ ≤ K

Tactic:
refine le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
⊢ ⁅H, K⁆ ≤ K

case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆

Tactic:
le_antisymm_iff,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ ≤ ⁅map f H₁, map f H₂⁆ ∧ ⁅map f H₁, map f H₂⁆ ≤ map f ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) (of 1)) x = x

Tactic:
lift_apply_of

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ of (1 * x₂)) x = x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (x₁ * x₂)) x) (of 1) = x

Tactic:
lift_apply_of

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₁ ↦ of (x₁ * 1)) x = x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥

Tactic:
rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆

Tactic:
apply congr_arg₂ <;>
  · rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ (lift ⇑f) (of (L1 * L2)) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)

Tactic:
lift_apply_of

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ f (L1 * L2) = f L1 * f L2
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
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = ↑s₃ * r₂ * ↑s'

Tactic:
h₂,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = r₃ * ↑u * ↑s'
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of s)) (of t) =
    (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of t)) (of s)

Tactic:
lift_apply_of

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ (lift fun x₁ ↦ of (Mul.mul x₁ t)) (of s) = (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of t)) (of s)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ (lift fun x₁ ↦ of (Mul.mul x₁ t)) (of s) = (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of t)) (of s)

Tactic:
lift_apply_of

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of (Mul.mul s t) = (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of t)) (of s)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of (Mul.mul s t) = (lift fun x₂ ↦ (lift fun x₁ ↦ of (Mul.mul x₁ x₂)) (of t)) (of s)

Tactic:
lift_apply_of

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of (Mul.mul s t) = (lift fun x₁ ↦ of (Mul.mul x₁ s)) (of t)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of (Mul.mul s t) = (lift fun x₁ ↦ of (Mul.mul x₁ s)) (of t)

Tactic:
lift_apply_of

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of (Mul.mul s t) = of (Mul.mul t s)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ n • (lift fun x ↦ 1) (of default) = n

Tactic:
lift_apply_of

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ n • 1 = n
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S) x y ↔ (OreLocalization.oreEqv S M) x y

Tactic:
by
  simp +instances only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv,
    smul_eq_mul, Submonoid.mk_smul]
  constructor
  · rintro ⟨u, hu, e⟩
    exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩
  · rintro ⟨u, hu, v, e₁, e₂⟩
    exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply']

Goal state after:
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Tactic:
rw [iterate_succ_apply']

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Tactic:
rw [iterate_succ_apply']

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : WithBot α
h : a ≠ 0
⊢ a * ⊥ = ⊥

Tactic:
rw [mul_bot', if_neg h]

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

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

Tactic:
lift x to α using x0.ne_bot

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

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

Tactic:
lift x to α using x0.ne_bot

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : x * a ≤ x * b
⊢ a ≤ b

Tactic:
lift x to α using x0.ne_bot

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a * x ≤ b * x
⊢ a ≤ b

Tactic:
lift x to α using x0.ne_bot

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
a b : WithBot α
x : α
x0 : 0 < ↑x
h : a * ↑x ≤ b * ↑x
⊢ a ≤ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b

Tactic:
· rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
    refine ⟨ha, fun hab => ?_⟩
    subst hab
    exact (h hb.isMax).elim

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:
by
  rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]

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

Goal state before:
pp: case h.zero
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[0] c = b
⊢ pred^[0] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
simp_all

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

Goal state before:
pp: case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ^[n + 1] a ∈ s
⊢ f a ≤ f (succ^[n + 1] a)

Tactic:
rw [Function.iterate_succ_apply'] at hb ⊢

Goal state after:
case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
⊢ f a ≤ f (succ (succ^[n] a))
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ^[n + 1 + 1] a ∈ s
⊢ f a < f (succ^[n + 1 + 1] a)

Tactic:
rw [Function.iterate_succ_apply'] at hb ⊢

Goal state after:
case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : succ^[n + 1] a ∈ s → f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
⊢ f a < f (succ (succ^[n + 1] a))
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: case neg
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : ¬Nonempty β
⊢ Small.{u, w} β

Tactic:
simp only [not_nonempty_iff] at hβ
    infer_instance

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

Goal state before:
pp: case top
n : ℕ
⊢ ⊤.toNat = ⊤.toNat - (↑n).toNat

Tactic:
toNat_top,

Goal state after:
case top
n : ℕ
⊢ 0 = 0 - (↑n).toNat
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∈ s
h : ⟨x, hx⟩ ≤ ⟨pred x, h'⟩
⊢ IsMin ⟨x, hx⟩

pp: case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h : ⟨x, hx⟩ ≤ ⟨x, hx⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
· simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h
      rintro ⟨y, _⟩ hy
      simp [h hy]

Goal state after:
case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h : ⟨x, hx⟩ ≤ ⟨x, hx⟩
⊢ IsMin ⟨x, hx⟩
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 : ℕ
hi : i < v.toList.length
⊢ i < n

Tactic:
simp_all

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
⊢ i ∉ s → f i = 1

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (f a ::ᵥ map f v').tail = map f (a ::ᵥ v').tail

Tactic:
tail_cons,

Goal state after:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ map f v' = map f (a ::ᵥ v').tail
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ eraseIdx (⟨j, hj⟩.succAbove ⟨i, hi⟩) (insertIdx a ⟨j, hj⟩ v) =
    insertIdx a (⟨i, hi⟩.predAbove ⟨j, hj⟩) (eraseIdx ⟨i, hi⟩ v)

Tactic:
dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ⟨((↑v).insertIdx j a).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩), ⋯⟩ =
    ⟨(↑(match v with
            | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
        (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a,
      ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ ((List.take (↑i) v.toList).prod * if ↑i < v.toList.length then a else 1) * (List.drop (↑i + 1) v.toList).prod =
    (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

Tactic:
simp_all

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i : Fin n✝.succ
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i = f ((a✝ ::ᵥ x✝).get i) ((b✝ ::ᵥ y✝).get i)

Tactic:
cases i using Fin.cases

Goal state after:
case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get 0 = f ((a✝ ::ᵥ x✝).get 0) ((b✝ ::ᵥ y✝).get 0)

case cons.succ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
i✝ : Fin n✝
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get i✝.succ = f ((a✝ ::ᵥ x✝).get i✝.succ) ((b✝ ::ᵥ y✝).get i✝.succ)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
      · rintro (⟨hba⟩ | ⟨hba⟩ | ⟨b, a⟩)
        · exact hba.not_gt (inl_lt_inl_iff.1 hab)
        · exact hba.not_gt (inr_lt_inr_iff.1 hab)
        · exact not_inr_lt_inl hab
      · rintro ⟨⟨hab⟩ | ⟨hab⟩ | ⟨a, b⟩, hba⟩
        · exact Lex.inl (hab.lt_of_not_ge fun h => hba <| Lex.inl h)
        · exact Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)
        · exact Lex.sep _ _

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

Goal state before:
pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝¹, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝¹ ≤ ↑a✝

Tactic:
· simp only [elim_inl, elim_inr, lex_inr_inl, false_iff]
      exact not_coe_le_bot _

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝¹, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ o.toOption ↔ a ∈ o

Tactic:
unfold toOption

Goal state after:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ (a ∈ if h : o.Dom then Option.some (o.get h) else Option.none) ↔ a ∈ o
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : p
a✝ : α
⊢ a✝ ∈ assert p f ↔ a✝ ∈ f h

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : ¬p
a✝ : α
⊢ a✝ ∈ assert p f ↔ a✝ ∈ none

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o

Tactic:
by
  rw [show f = id from funext H]; exact id_map o

Goal state after: