mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ Monotone f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ Monotone f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a ≤ f (succ a)

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ ∀ (a x : α), a < x → f a ≤ f (succ a)
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: α : Type v
inst✝ : Small.{w, v} α
x y : Shrink.{w, v} α
w : (equivShrink α).symm x = (equivShrink α).symm y
⊢ x = y

Tactic:
simpa using

Goal state after:
α : Type v
inst✝ : Small.{w, v} α
x y : Shrink.{w, v} α
w : (equivShrink α).symm x = (equivShrink α).symm y
⊢ x = y
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: α : Type u_2
β : α → Type u_1
inst✝¹ : Small.{w, u_2} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink.{w, u_1} (β ((equivShrink α).symm ((equivShrink α) a)))

Tactic:
simpa using

Goal state after:
α : Type u_2
β : α → Type u_1
inst✝¹ : Small.{w, u_2} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink.{w, u_1} (β a)
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × e.symm α)
h₁ : e (Set ((α : S) × e.symm α)) = e (Set ((α : S) × e.symm α))
h₂ : cast ⋯ a = cast ⋯ b
⊢ a = b

Tactic:
simpa using

Goal state after:
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × e.symm α)
h₁ : e (Set ((α : S) × e.symm α)) = e (Set ((α : S) × e.symm α))
h₂ : cast ⋯ a = cast ⋯ b
⊢ a = b
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type u_2
β : α → Type u_1
inst✝¹ : Small.{w, u_2} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink.{w, u_1} (β ((equivShrink α).symm ((equivShrink α) a)))

Tactic:
simpa using

Goal state after:
α : Type u_2
β : α → Type u_1
inst✝¹ : Small.{w, u_2} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink.{w, u_1} (β a)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ Antitone f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ Antitone f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) ≤ f a

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ ∀ (a x : α), a < x → f (succ a) ≤ f a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ StrictMono f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ StrictMono f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a < f (succ a)

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ ∀ (a x : α), a < x → f a < f (succ a)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ StrictAnti f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ StrictAnti f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) < f a

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ ∀ (a x : α), a < x → f (succ a) < f a
Module: Mathlib.Data.ENat.Basic

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

Tactic:
simpa using

Goal state after:
case top
m : ℕ
inst✝ : NeZero m
⊢ ¬0 = m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n m : ℕ
h : ↑m ≤ ↑n
⊢ (↑m).toNat ≤ n

Tactic:
simpa using

Goal state after:
n m : ℕ
h : ↑m ≤ ↑n
⊢ m ≤ n
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ a ≤ a * c

Tactic:
← mul_one a,

Goal state after:
case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ a * 1 ≤ a * c
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg.inl
α✝ : 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⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : y < x
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

Tactic:
have := h.le_pred

Goal state after:
case neg.inl
α✝ : 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⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : y < x
this : y ≤ pred x
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
ha : pred^[0 + 1] b ∈ s
⊢ f (pred^[0 + 1] b) < f b

Tactic:
simpa using

Goal state after:
case succ.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
ha : pred^[0 + 1] b ∈ s
⊢ f (pred b) < f b
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
x : ℕ
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa using

Goal state after:
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
x : ℕ
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ ¬x = 0
Module: Mathlib.Data.Finset.Piecewise

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

Tactic:
by
  rw [← insert_empty_eq, piecewise_insert, piecewise_empty]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ Monotone f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ Monotone f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) ≤ f a

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ ∀ (a x : α), x < a → f (pred a) ≤ f a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ Antitone f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ Antitone f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a ≤ f (pred a)

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ ∀ (a x : α), x < a → f a ≤ f (pred a)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ StrictMono f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ StrictMono f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) < f a

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ ∀ (a x : α), x < a → f (pred a) < f a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ StrictAnti f

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ StrictAnti f
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a < f (pred a)

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ ∀ (a x : α), x < a → f a < f (pred a)
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
m : ℕ
n : ℕ∞
⊢ ↑n + 1 ≤ ↑m ↔ ↑n < ↑m

Tactic:
| coe n =>

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

Goal state after:
ι : 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
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

Goal state after:
ι : 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
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

Goal state after:
ι : 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
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

Goal state after:
ι : 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
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

Goal state after:
ι : 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
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

Goal state after:
ι : 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
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

Goal state after:
ι : 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
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

Goal state after:
ι : 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
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, f ↑i ⋯

Tactic:
refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ Fintype.card α = Fintype.card ↥t

Tactic:
Fintype.card_coe

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ Fintype.card α = #t
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:
simpa using

Goal state after:
ι : 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 j : ι), p i → p j → i = j
Module: Mathlib.Data.Vector.Basic

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

Tactic:
simp only [this, scanl_nil, head_cons]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i, f i = f a * ∏ i, f ↑i

Tactic:
simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none,
    Equiv.optionSubtypeNe_some]

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

Goal state before:
pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j

Tactic:
simpa using

Goal state after:
case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ i ≤ j
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i

Tactic:
simpa using

Goal state after:
case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
this : Countable ↑s
⊢ (⋃ x, t ↑x ⋯).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable

Tactic:
countable_iUnion_iff,

Goal state after:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
this : Countable ↑s
⊢ (∀ (i : ↑s), (t ↑i ⋯).Countable) ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk.mk.mk.h
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ val✝¹ ≠ val✝

Tactic:
simpa using

Goal state after:
case mk.mk.mk.h
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ ¬val✝¹ = val✝
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
inst✝ : Countable α
⊢ {s | s.Finite}.Countable

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : Countable α
⊢ {s | s.Finite}.Countable
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
simpa using

Goal state after:
case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : ¬r b x
⊢ r a b
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

Tactic:
simpa using

Goal state after:
case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ ¬r a b
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
simpa using

Goal state after:
case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r x a
b : α
hb : r x b
⊢ r a b
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : ¬r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

Tactic:
simpa using

Goal state after:
case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : ¬r x b
⊢ ¬r a b