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

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}

Tactic:
simp only [le_def, or_imp, ← forall_and]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c : Con M
⊢ c.toSetoid = ⊤ ↔ c = ⊤

Tactic:
rw [← toSetoid_top, toSetoid_inj]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' mk '' s = s * ↑N

Tactic:
by
  rw [preimage_image_mk_eq_iUnion_image, iUnion_subtype, ← image2_mul, ← iUnion_image_right]
  simp only [SetLike.mem_coe]

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

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective ⇑(map f)

Tactic:
rw [Function.injective_iff_hasLeftInverse]
    use map (Function.invFun f)
    simp [Function.LeftInverse, map.comp, Function.invFun_comp hf]

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ (lift N φ HN).ker = Subgroup.map (mk' N) ((lift N φ HN).comp (mk' N)).ker

Tactic:
← MonoidHom.comap_ker,

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ (lift N φ HN).ker = Subgroup.map (mk' N) (Subgroup.comap (mk' N) (lift N φ HN).ker)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_5
inst✝¹ : Finite ι
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi Set.univ P).FG

Tactic:
by
  simp_rw [fg_iff_submonoid_fg] at *
  exact .pi hP

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeGroup.lift Subtype.val, ?_⟩, ?_⟩

Goal state after:
case refine_1
G : Type u_3
inst✝ : Group G
x✝ : FG G
S : Finset G
hS : Subgroup.closure ↑S = ⊤
⊢ Function.Surjective ⇑(FreeGroup.lift Subtype.val)

case refine_2
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG G
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
s : ↥⊥
h : x✝¹ * ↑s = x✝ * ↑s
⊢ ↑s * x✝¹ = ↑s * x✝

Tactic:
rcases s with ⟨s, hs⟩
      rw [Submonoid.mem_bot] at hs
      subst hs
      rw [mul_one, mul_one] at h
      subst h
      rfl

Goal state after:
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 = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}

Tactic:
← Finset.sum_nsmul,

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, k • (count x s / k) • {x}
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ g * ⁅g₁, g₂⁆ * g⁻¹ ∈ closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}

Tactic:
apply (mul_mem_cancel_right <| commutator_mem_commutator hg hg₂).mp

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ g * ⁅g₁, g₂⁆ * g⁻¹ * ⁅g, g₂⁆ ∈ ⁅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 α
⊢ 1 * x = x

Tactic:
simp_rw [mul_def, one_def, 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.Commutator.Basic

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

Tactic:
refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this

Goal state after:
G : Type u_1
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), ⊤⁆, centralizer ↑(commutator G)⁆ = ⊥
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

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)
⊢ (f.lift hg).comp f.toMonoidHom = g

Tactic:
ext; exact f.lift_eq hg _

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑y * p) = ↑t * (↑q * x)
⊢ (↑t * (↑q * x), t * (y * q)) = (↑t * (↑q * x), t * (q * y))

Tactic:
mul_comm y q

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: case inl
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')
surj : Set.SurjOn ⇑g ↑S ↑T
⊢ z = w

Tactic:
have ⟨⟨c, hc'⟩, eq⟩ := k.exists_of_eq this

Goal state after:
case inl
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')
surj : Set.SurjOn ⇑g ↑S ↑T
c : P
hc' : c ∈ T
eq : ↑⟨c, hc'⟩ * g z' = ↑⟨c, hc'⟩ * g w'
⊢ z = w
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ f (g₁ a) = f (g₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁵ : Mul R
inst✝⁴ : Add R
inst✝³ : Mul S
inst✝² : Add S
inst✝¹ : Preorder R
inst✝ : Preorder S
e : R ≃+*o S
x : R
y : S
⊢ e.symm y < x ↔ y < e x

Tactic:
by
  simpa using! e.toOrderIso.symm_apply_lt

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ (match a, n + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a

Tactic:
cases n

Goal state after:
case zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match a, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a

case succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
n✝ : ℕ
⊢ (match a, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0

Tactic:
cases n

Goal state after:
case top.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊤ ^ 0 = ⊤ ↔ ⊤ = ⊤ ∧ 0 ≠ 0

case top.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n✝ : ℕ
⊢ ⊤ ^ (n✝ + 1) = ⊤ ↔ ⊤ = ⊤ ∧ n✝ + 1 ≠ 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
a✝ : α
⊢ ↑a✝ ^ n = ⊤ ↔ ↑a✝ = ⊤ ∧ n ≠ 0

Tactic:
cases n

Goal state after:
case coe.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
⊢ ↑a✝ ^ 0 = ⊤ ↔ ↑a✝ = ⊤ ∧ 0 ≠ 0

case coe.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
n✝ : ℕ
⊢ ↑a✝ ^ (n✝ + 1) = ⊤ ↔ ↑a✝ = ⊤ ∧ n✝ + 1 ≠ 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

Tactic:
by_cases hc : c = 0; · simp [hc]
      simp only [mul_coe_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (add_mul _ _ _)

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n

Tactic:
cases n

Goal state after:
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
n✝ : ℕ
hx : ∀ (k : ℕ), k < n✝ + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n✝ + 1 → f (y k) ≤ y (k + 1)
⊢ x (n✝ + 1) < y (n✝ + 1)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥

Tactic:
rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥

Tactic:
rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

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

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

Tactic:
rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

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

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

Tactic:
rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
Or.comm

Goal state after:
case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ succ a ≤ succ b

Tactic:
by_cases hb : IsMax b
  · by_cases hba : b ≤ a
    · exact (hb <| hba.trans <| le_succ _).trans (le_succ _)
    · exact succ_le_of_lt ((h.lt_of_not_ge hba).trans_le <| le_succ b)
  · rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]
    apply lt_succ_of_le_of_not_isMax h hb

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
⊢ IsMax a

Tactic:
by_contra H

Goal state after:
α : Type u_1
a : α
inst✝¹ : Preorder α
inst✝ : SuccOrder α
h : IsSuccPrelimit (succ a)
H : ¬IsMax a
⊢ False
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ b)
⊢ False

Tactic:
exact not_isMax _ h.isMax

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)

Tactic:
· rw [h_eq]
    exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ (succ^[n] x) = x + ↑(n + 1)

Tactic:
IH,

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ (x + ↑n) = x + ↑(n + 1)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred (pred^[n] x) = x - ↑(n + 1)

Tactic:
IH,

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred (x - ↑n) = x - ↑(n + 1)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
· have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a b : WithTop α
h : a < b
⊢ (match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    b

Tactic:
by
    cases b
    · exact le_top
    cases a
    · exact (not_top_lt h).elim
    rw [coe_lt_coe] at h
    change ite _ _ _ ≤ _
    split_ifs with ha
    · rw [succ_eq_iff_isMax] at ha
      exact (ha.not_lt h).elim
    · exact coe_le_coe.2 (succ_le_of_lt h)

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

Goal state before:
pp: x : ℕ∞
hx : x < ⊤
⊢ x.lift hx = x.toNat

Tactic:
rcases x with ⟨⟩ | x

Goal state after:
case none
hx : none < ⊤
⊢ lift none hx = toNat none

case some
x : ℕ
hx : some x < ⊤
⊢ lift (some x) hx = toNat (some x)
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
m : ℕ
inst✝ : NeZero m
⊢ n.toNat = m ↔ n = ↑m

Tactic:
cases n

Goal state after:
case top
m : ℕ
inst✝ : NeZero m
⊢ ⊤.toNat = m ↔ ⊤ = ↑m

case coe
m : ℕ
inst✝ : NeZero m
a✝ : ℕ
⊢ (↑a✝).toNat = m ↔ ↑a✝ = ↑m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
⊢ x = default

Tactic:
have := x.val_inv

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
⊢ x = default
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ 0 ≤ map Nat.cast n

Tactic:
cases n

Goal state after:
case top
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ 0 ≤ map Nat.cast ⊤

case coe
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
a✝ : ℕ
⊢ 0 ≤ map Nat.cast ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : WithBot ℕ∞
m : ℕ
⊢ n < ↑↑(m + 1) ↔ n ≤ ↑m

Tactic:
cases n

Goal state after:
case bot
m : ℕ
⊢ ⊥ < ↑↑(m + 1) ↔ ⊥ ≤ ↑m

case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ (univ.erase i).piecewise f g = update f i (g i)

Tactic:
rw [← compl_singleton, piecewise_compl, piecewise_singleton]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x

Tactic:
by
  classical calc
      ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
        (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
      _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
      _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

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✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (∏ j, if h : j = i then f j h else 1) = f i ⋯

Tactic:
Finset.prod_dite_eq',

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (if i ∈ univ then f i ⋯ else 1) = f i ⋯
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ↑s = ↑(replicate n a) ↔ ∀ b ∈ s, b = a

Tactic:
val_replicate,

Goal state after:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ↑s = Multiset.replicate n a ↔ ∀ b ∈ s, b = a
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α n✝
a b : α
inst✝ : Subsingleton α
n : ℕ
⊢ ∀ (a b : Sym α n), a = b

Tactic:
cases n

Goal state after:
case zero
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
⊢ ∀ (a b : Sym α 0), a = b

case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (n✝ + 1)), a = b
Module: Mathlib.Data.Vector.Basic

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

Tactic:
cases n

Goal state after:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ (scanl f b v).head = b

case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m

Tactic:
count_add,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ ¬a = x) ↑m) + count b ↑(replicate (count a ↑m) a) = count b ↑m
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
suffices x ∉ Multiset.replicate i a by simp [coe_fill, coe_replicate, this]
  simp [Multiset.mem_replicate, hx]

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
⊢ t = t'

Tactic:
by_contra H

Goal state after:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
A : (f t ∩ f t').Nonempty
H : ¬t = t'
⊢ False
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
⊢ (match Sum.inr f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]

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

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

Tactic:
simp only [lex_inr_inl, false_iff]
      exact not_top_le_coe _

Goal state after: