mathlib-initiative/mathlib-tactics huggingface dataset:
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:
·

Goal state after:
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⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inl
c : ℕ∞
hc : c ≠ 0
⊢ ⊤ ≤ ⊤ * c

pp: case inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
⊢ a ≤ a * c

Tactic:
·

Goal state after:
case inl
c : ℕ∞
hc : c ≠ 0
⊢ ⊤ ≤ ⊤ * c
Module: Mathlib.Data.ENat.Basic

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

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

Tactic:
·

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

Goal state before:
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:
·

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.Order.SuccPred.Archimedean

Goal state before:
pp: case 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
ha : pred^[0] b ∈ s
hab : pred^[0] b < b
⊢ f (pred^[0] b) < f b

pp: case succ
α : 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
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : pred^[n + 1] b < b
⊢ f (pred^[n + 1] b) < f b

Tactic:
·

Goal state after:
case 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
ha : pred^[0] b ∈ s
hab : pred^[0] b < b
⊢ f (pred^[0] b) < f b
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, hy⟩ < ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

pp: case neg.inr
α✝ : 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, hy⟩ = ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

Tactic:
·

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, hy⟩ < ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
·

Goal state after:
case neg.inr
α✝ : 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, hy⟩ = ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case isTrue
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
h✝ : pred c ∈ s
⊢ ⟨b, hb⟩ ≤ ⟨pred c, h✝⟩

pp: case isFalse
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
h✝ : pred c ∉ s
⊢ ⟨b, hb⟩ ≤ ⟨c, hc⟩

Tactic:
·

Goal state after:
case isTrue
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
h✝ : pred c ∈ s
⊢ ⟨b, hb⟩ ≤ ⟨pred c, h✝⟩
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case isFalse
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
h✝ : pred c ∉ s
⊢ ⟨b, hb⟩ ≤ ⟨c, hc⟩

Tactic:
·

Goal state after:
case isFalse
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
h✝ : pred c ∉ s
⊢ ⟨b, hb⟩ ≤ ⟨c, hc⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inl
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
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

pp: case inr
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
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
·

Goal state after:
case inl
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
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : 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
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

pp: case neg
α : 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
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : ¬IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
·

Goal state after:
case pos
α : 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
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inl
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
x : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0

pp: case inr.inr
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
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
·

Goal state after:
case inr.inl
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
x : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg
α : 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
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : ¬IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
·

Goal state after:
case neg
α : 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
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : ¬IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b
Module: Mathlib.Data.ENat.Basic

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

pp: case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m

Tactic:
·

Goal state after:
case bot
m : ℕ
⊢ ⊥ < ↑↑(m + 1) ↔ ⊥ ≤ ↑m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m

Tactic:
·

Goal state after:
case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case bot
n : ℕ
⊢ ↑↑(n + 1) ≤ ⊥ ↔ ↑n < ⊥

pp: case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝

Tactic:
·

Goal state after:
case bot
n : ℕ
⊢ ↑↑(n + 1) ≤ ⊥ ↔ ↑n < ⊥
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝

Tactic:
·

Goal state after:
case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β : Type u
f : α → β
⊢ (fun x ↦ pure f <*> x) = fun x ↦ f <$> x

Tactic:
by
  simp [functor_norm]

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

Goal state before:
pp: case e_1
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun x ↦ x ∈ s) = fun x ↦ x ∈ {x | x ∈ s}

pp: case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}

pp: case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩

Tactic:
·

Goal state after:
case e_1
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun x ↦ x ∈ s) = fun x ↦ x ∈ {x | x ∈ s}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}

pp: case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩

Tactic:
·

Goal state after:
case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩

Tactic:
·

Goal state after:
case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1

Tactic:
·

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : a = b_1 then b b_1 h else 1) = 1

pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
·

Goal state after:
case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : a = b_1 then b b_1 h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
·

Goal state after:
case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = 1

Tactic:
·

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : b_1 = a then b b_1 h else 1) = 1

pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
·

Goal state after:
case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : b_1 = a then b b_1 h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
·

Goal state after:
case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = 1

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
·

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
x✝ : Fintype { b // b ≠ a }
⊢ Function.Bijective (Sum.elim Subtype.val Subtype.val)

Tactic:
classical exact (Equiv.sumCompl (· = a)).bijective

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ ⊆ (image b univ).erase k

pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ (image b univ).erase k ⊆ image (fun i ↦ b ↑i) univ

Tactic:
·

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ ⊆ (image b univ).erase k
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ (image b univ).erase k ⊆ image (fun i ↦ b ↑i) univ

Tactic:
·

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ (image b univ).erase k ⊆ image (fun i ↦ b ↑i) univ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = a

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
·

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1
Module: Mathlib.Control.Applicative

Goal state before:
pp: case e_toSeqRight
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
x : F α
y : Unit → F β
⊢ sr1 x y = sr2 x y

Tactic:
·

Goal state after:
case e_toSeqRight
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
x : F α
y : Unit → F β
⊢ sr1 x y = sr2 x y