mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, ↑a ∈ m.toFinset

Tactic:
simp [hfg]

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ⟨a, ⋯⟩ ∈ univ

Tactic:
simp [hfg]

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

Goal state before:
pp: case refine_3
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : { x // x ∈ m }) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

Tactic:
simp [hfg]

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

Goal state before:
pp: case refine_4
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ↑⟨a, ⋯⟩ = a

Tactic:
simp [hfg]

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

Goal state before:
pp: case refine_5
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, f a = g ↑a

Tactic:
simp [hfg]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y✝ y

Tactic:
rw [Multiset.mem_map]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ (∃ a ∈ s.val, f a = y) → Commute y✝ y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ S.toFinset.prod id ∣ S.prod

Tactic:
Finset.prod_eq_multiset_prod

Goal state after:
M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ (map id S.toFinset.val).prod ∣ S.prod
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ y ∈ Multiset.map f t.val → y ∈ S

Tactic:
rw [Multiset.mem_map]

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ (∃ a ∈ t.val, f a = y) → y ∈ S
Module: Mathlib.Data.Setoid.Basic

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

Tactic:
rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r) x y ↔ ⟦f x⟧ = ⟦f y⟧

Tactic:
rw [Quotient.eq]; rfl

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:
← toSetoid_bot,

Goal state after:
M : Type u_1
inst✝ : Mul M
c : Con M
⊢ c.toSetoid = ⊥.toSetoid ↔ c = ⊥
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)

Tactic:
by
  rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disjSum, Finset.toLeft_disjSum,
    Finset.toRight_disjSum]

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]

Tactic:
singleton_iff

Goal state after:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]
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:
by 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:
by simp_all

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
⊢ FG M'

Tactic:
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
    use s.image f
    rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Monoid M
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG M

Tactic:
intro ⟨α, _, φ, hφ⟩
    exact Monoid.fg_of_surjective _ hφ

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
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ G ⧸ N →* H ⧸ M

Tactic:
refine QuotientGroup.lift N ((mk' M).comp f) ?_

Goal state after:
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
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ N ≤ ((mk' M).comp f).ker
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f x = 1

pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : ¬x = a
⊢ f x = 1

Tactic:
· rw [h]
      rw [h] at hx
      rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp
      exact hp

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : ¬x = a
⊢ f x = 1
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:
by simp_all

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup α
⊢ (map ⇑f.symm) ((map ⇑f) x) = x

Tactic:
rw [← map_comp_apply, Equiv.symm_comp_self, map_id, AddMonoidHom.id_apply]

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

Goal state before:
pp: case mpr
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)
⊢ (∀ (v : P), ∃ x, v * g ↑x.2 = g x.1) → Surjective ⇑(f.lift hg)

Tactic:
· intro H v
    obtain ⟨x, hx⟩ := H v
    use f.mk' x.1 x.2
    rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ OreLocalization.oreNum (c • 1) b • a /ₒ (OreLocalization.oreDenom (c • 1) b * 1) = c • a /ₒ b

Tactic:
change (c • 1) • a /ₒ (b * 1) = _

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ (c • 1) • a /ₒ (b * 1) = c • a /ₒ b
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 : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ (s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)) = r₂' • r₂ • r₁ /ₒ (s₂' * s)

Tactic:
OreLocalization.expand _ (s₂' * s) _ this

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 : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ (s₄' * s₃') • r₁' • r₁ /ₒ (s₄' * s₃' * (s₁' * s)) = (↑s₄' * r₃') • r₂' • r₂ • r₁ /ₒ ⟨↑s₄' * r₃' * ↑(s₂' * s), this⟩
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑y = f ↑z

Tactic:
rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]
  exact Units.inv_mul (IsUnit.liftRight (f.domRestrict S) hf z)⁻¹

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ * ↑b = Option.bind ⊤ fun a ↦ Option.some (a * b)

Tactic:
simp [top_mul, hb]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ = Option.bind ⊤ fun a ↦ Option.some (a * b)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case inr
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z n : ℕ
hnS : n ∈ S
hn0 : n ≠ 0
key : z < n * (z / n + 1)
⊢ ∃ x, ∃ y ∈ S, -↑z = ↑x - ↑y

Tactic:
exact ⟨(z / n + 1) * n - z, (z / n + 1) * n, nsmul_mem hnS _, by lia⟩

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Tactic:
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a : α
n : ℕ
h : a ≤ succ^[n] a
⊢ p a ↔ p (succ^[n] a)

Tactic:
exact Iterate.rec (fun b => p a ↔ p b) Iff.rfl (fun c hc => hc.trans (hsucc _)) n

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

Goal state before:
pp: case bot
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
⊢ ⊥.succ = 0 ↔ ⊥ = ⊥

Tactic:
simp [bot_eq_zero]

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : LinearOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x + 1 = y + 1 ↔ x = y

Tactic:
by
  simp [← succ_eq_add_one]

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

Goal state before:
pp: case pos
α : 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
this : succ^[n] a ∈ s
hb' : IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))

pp: case neg
α : 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
this : succ^[n] a ∈ s
hb' : ¬IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))

Tactic:
· rw [succ_eq_iff_isMax.2 hb']
      exact hn this

Goal state after:
case neg
α : 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
this : succ^[n] a ∈ s
hb' : ¬IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) < f a) → StrictAnti f

Tactic:
by
  simpa [Order.succ_eq_add_one] using strictAnti_of_succ_lt (f := f)

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

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha : (if succ a✝ = a✝ then ⊤ else ↑(succ a✝)) ≤ ↑a✝
⊢ IsMax ↑a✝

Tactic:
split_ifs at ha with ha'

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : succ a✝ = a✝
ha : ⊤ ≤ ↑a✝
⊢ IsMax ↑a✝

case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : ↑(succ a✝) ≤ ↑a✝
⊢ IsMax ↑a✝
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : 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
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))

pp: case neg
α : 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
this : succ^[n + 1] a ∈ s
hb' : ¬IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))

Tactic:
· rw [succ_eq_iff_isMax.2 hb']
      exact hn this

Goal state after:
case neg
α : 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
this : succ^[n + 1] a ∈ s
hb' : ¬IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))
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:
by 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:
by simp_all

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

Goal state before:
pp: ι : Type u_1
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ #({i ∈ s | p i}) = ∑ i ∈ s, if p i then 1 else 0

Tactic:
by simp [sum_ite]

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 ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (List.scanl f b v.toList).length = n + 1

Tactic:
by rw [List.length_scanl, toList_length]

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

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ ∏ j ∈ univ.erase i, #s = #s ^ (card ι - 1)

Tactic:
by
    rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

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

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then ∏ b ∈ univ.erase i, #s else 0) = if j ∈ s then #s ^ (card ι - 1) else 0

Tactic:
by
    rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
⊢ Encodable α

Tactic:
by
  classical exact (Fintype.truncEncodable α).out

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
⊢ {t | t.Finite ∧ t ⊆ s} ⊆ range fun t ↦ Subtype.val '' ↑t

Tactic:
rintro t ⟨ht, hts⟩

Goal state after:
α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Set α
ht : t.Finite
hts : t ⊆ s
⊢ t ∈ range fun t ↦ Subtype.val '' ↑t
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: f : ℕ → Cardinal.{u}
⊢ sum f = f 0 + sum fun i ↦ f (i + 1)

Tactic:
by
  refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_
  simp only [mk_sum, mk_out, lift_id, mk_sigma]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ioi a ⊆ s

Tactic:
simp [isUpperSet_iff_forall_lt, subset_def, @forall_comm (_ ∈ s)]

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

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, 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)) ↔
    ⊥ ≤ ⊥

pp: case bot.coe
α : 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 ⊥, 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✝

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_inr, lex_inl_inl, bot_le]

Goal state after:
case bot.coe
α : 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 ⊥, 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✝

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✝ ≤ ⊥

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✝