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

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha : ⊤ ≠ ⊤
⊢ pred ⊤ ≠ ⊤

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha : ↑a✝ ≠ ⊤
⊢ pred ↑a✝ ≠ ⊤

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha : ⊤ ≠ ⊤
⊢ pred ⊤ ≠ ⊤

case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha : ↑a✝ ≠ ⊤
⊢ pred ↑a✝ ≠ ⊤
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case top
a b c d m n : ℕ∞
⊢ SuccOrder.succ ⊤ = ⊤ + 1

pp: case coe
a b c d m n : ℕ∞
a✝ : ℕ
⊢ SuccOrder.succ ↑a✝ = ↑a✝ + 1

Tactic:
<;>

Goal state after:
case top
a b c d m n : ℕ∞
⊢ SuccOrder.succ ⊤ = ⊤ + 1

case coe
a b c d m n : ℕ∞
a✝ : ℕ
⊢ SuccOrder.succ ↑a✝ = ↑a✝ + 1
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case top
b : ℕ∞
⊢ (⊤ * b).toNat = ⊤.toNat * b.toNat

pp: case coe
b : ℕ∞
a✝ : ℕ
⊢ (↑a✝ * b).toNat = (↑a✝).toNat * b.toNat

Tactic:
<;>

Goal state after:
case top
b : ℕ∞
⊢ (⊤ * b).toNat = ⊤.toNat * b.toNat

case coe
b : ℕ∞
a✝ : ℕ
⊢ (↑a✝ * b).toNat = (↑a✝).toNat * b.toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case top.coe.zero
⊢ (⊤ * ↑0).toNat = ⊤.toNat * (↑0).toNat

pp: case top.coe.succ
n✝ : ℕ
⊢ (⊤ * ↑(n✝ + 1)).toNat = ⊤.toNat * (↑(n✝ + 1)).toNat

Tactic:
<;>

Goal state after:
case top.coe.zero
⊢ (⊤ * ↑0).toNat = ⊤.toNat * (↑0).toNat

case top.coe.succ
n✝ : ℕ
⊢ (⊤ * ↑(n✝ + 1)).toNat = ⊤.toNat * (↑(n✝ + 1)).toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe.top.zero
⊢ (↑0 * ⊤).toNat = (↑0).toNat * ⊤.toNat

pp: case coe.top.succ
n✝ : ℕ
⊢ (↑(n✝ + 1) * ⊤).toNat = (↑(n✝ + 1)).toNat * ⊤.toNat

Tactic:
<;>

Goal state after:
case coe.top.zero
⊢ (↑0 * ⊤).toNat = (↑0).toNat * ⊤.toNat

case coe.top.succ
n✝ : ℕ
⊢ (↑(n✝ + 1) * ⊤).toNat = (↑(n✝ + 1)).toNat * ⊤.toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case top
n : ℕ
hn : n ≠ 0
⊢ ⊤.toNat = n ↔ ⊤ = ↑n

pp: case coe
n : ℕ
hn : n ≠ 0
a✝ : ℕ
⊢ (↑a✝).toNat = n ↔ ↑a✝ = ↑n

Tactic:
<;>

Goal state after:
case top
n : ℕ
hn : n ≠ 0
⊢ ⊤.toNat = n ↔ ⊤ = ↑n

case coe
n : ℕ
hn : n ≠ 0
a✝ : ℕ
⊢ (↑a✝).toNat = n ↔ ↑a✝ = ↑n
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✝ : ↑s
x : α
hx : x ∈ s
h✝ : pred x ∈ s
⊢ ⟨pred x, h✝⟩ ≤ ⟨x, hx⟩

pp: case isFalse
α✝ : 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
⊢ ⟨x, hx⟩ ≤ ⟨x, hx⟩

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✝ : ↑s
x : α
hx : x ∈ s
h✝ : pred x ∈ s
⊢ ⟨pred x, h✝⟩ ≤ ⟨x, hx⟩

case isFalse
α✝ : 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
⊢ ⟨x, hx⟩ ≤ ⟨x, hx⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ a * c

Tactic:
by
  obtain rfl | hne := eq_or_ne a ⊤
  · simp [top_mul hc]
  obtain rfl | h0 := eq_or_ne a 0
  · simp
  nth_rewrite 1 [← mul_one a, ENat.mul_le_mul_left_iff h0 hne, Order.one_le_iff_ne_zero]
  assumption

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

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

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

Tactic:
<;>

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

Goal state before:
pp: case pos
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
h✝ : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s
⊢ ↑⟨pred ↑(ofDual a), h✝⟩ = succ ↑a

pp: case neg
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
h✝ : pred ↑(ofDual a) ∉ ⇑ofDual ⁻¹' s
⊢ ↑(ofDual a) = succ ↑a

Tactic:
<;>

Goal state after:
case pos
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
h✝ : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s
⊢ ↑⟨pred ↑(ofDual a), h✝⟩ = succ ↑a

case neg
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
h✝ : pred ↑(ofDual a) ∉ ⇑ofDual ⁻¹' s
⊢ ↑(ofDual a) = succ ↑a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
h✝ : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s
⊢ ⟨pred ↑(ofDual a), h✝⟩ = a

pp: case neg
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
h✝ : pred ↑(ofDual a) ∉ ⇑ofDual ⁻¹' s
⊢ ofDual a = a

Tactic:
<;>

Goal state after:
case pos
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
h✝ : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s
⊢ ⟨pred ↑(ofDual a), h✝⟩ = a

case neg
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
h✝ : pred ↑(ofDual a) ∉ ⇑ofDual ⁻¹' s
⊢ ofDual a = a
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inr.coe.top
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
this : ↑(f x) ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤

Tactic:
simp [mul_top hx, WithTop.mul_top this]

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

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∈ s
⊢ p (s.piecewise f g i)

pp: case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∉ s
⊢ p (s.piecewise f g i)

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∈ s
⊢ p (s.piecewise f g i)

case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∉ s
⊢ p (s.piecewise f g i)
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: case inl
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

pp: case inr
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

case inr
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
hs : j ∈ s
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

pp: case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
hs : j ∉ s
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

pp: case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∈ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

pp: case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∉ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
hs : j ∈ s
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
hs : j ∉ s
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∈ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∉ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
h : i ∈ s
⊢ s.piecewise f f i = f i

pp: case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
h : i ∉ s
⊢ s.piecewise f f i = f i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
h : i ∈ s
⊢ s.piecewise f f i = f i

case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
h : i ∉ s
⊢ s.piecewise f f i = f i
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∈ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

pp: case neg
ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∉ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∈ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

case neg
ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∉ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: case hst
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ (i : γ × α), i ∈ r ↔ (Equiv.sigmaEquivProd γ α).symm i ∈ s.sigma t

pp: case hfg
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ i ∈ r, f i = f (((Equiv.sigmaEquivProd γ α).symm i).fst, ((Equiv.sigmaEquivProd γ α).symm i).snd)

Tactic:
<;>

Goal state after:
case hst
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ (i : γ × α), i ∈ r ↔ (Equiv.sigmaEquivProd γ α).symm i ∈ s.sigma t

case hfg
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∀ i ∈ r, f i = f (((Equiv.sigmaEquivProd γ α).symm i).fst, ((Equiv.sigmaEquivProd γ α).symm i).snd)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: case hst
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ (i : α × γ), i ∈ r ↔ ((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i ∈ s.sigma t

pp: case hfg
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ i ∈ r,
    f i =
      f
        ((((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i).snd,
          (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i).fst)

Tactic:
<;>

Goal state after:
case hst
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ (i : α × γ), i ∈ r ↔ ((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i ∈ s.sigma t

case hfg
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∀ i ∈ r,
    f i =
      f
        ((((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i).snd,
          (((Equiv.prodComm α γ).trans (Equiv.sigmaEquivProd γ α).symm) i).fst)
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 ∈ map Embedding.some (eraseNone s), Option.elim' 1 f x = ∏ x ∈ s.erase none, Option.elim' 1 f x

Tactic:
map_some_eraseNone

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ s.erase none, Option.elim' 1 f x = ∏ x ∈ s.erase none, Option.elim' 1 f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z

Tactic:
by
  simp_rw [prod_comm (s := t), prod_comm (s := s)]

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

Goal state before:
pp: case refine_1
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

pp: case refine_2
ι : 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
⊢ ∀ a ∈ univ, ↑a ∈ s

pp: case refine_3
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

pp: case refine_4
ι : 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
⊢ ∀ (a : ↥s) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

pp: case refine_5
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = g ↑⟨a, ha⟩ ⋯

Tactic:
<;>

Goal state after:
case refine_1
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

case refine_2
ι : 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
⊢ ∀ a ∈ univ, ↑a ∈ s

case refine_3
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

case refine_4
ι : 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
⊢ ∀ (a : ↥s) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

case refine_5
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = g ↑⟨a, ha⟩ ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case refine_1
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

pp: case refine_2
ι : 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
⊢ ∀ a ∈ univ, ↑a ∈ s

pp: case refine_3
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

pp: case refine_4
ι : 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
⊢ ∀ (a : ↥s) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

pp: case refine_5
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = f ↑⟨a, ha⟩ ⋯

Tactic:
<;>

Goal state after:
case refine_1
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

case refine_2
ι : 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
⊢ ∀ a ∈ univ, ↑a ∈ s

case refine_3
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

case refine_4
ι : 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
⊢ ∀ (a : ↥s) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

case refine_5
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = f ↑⟨a, ha⟩ ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case e_5.hα
ι : 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.h
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (a : ↥s) (a' : ↥{x | x ∈ s}), a ≍ a' → f a ≍ f ⟨↑a', ⋯⟩

Tactic:
<;>

Goal state after:
case e_5.hα
ι : 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}

case e_5.h
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (a : ↥s) (a' : ↥{x | x ∈ s}), a ≍ a' → f a ≍ f ⟨↑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
i : Fin n
l : List α
p : l.length = n
⊢ l.length - 1 = n - 1

pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < l.length

Tactic:
<;>

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ l.length - 1 = n - 1

α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < l.length
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : α
⊢ Sum.inl val✝ ∈ univ.disjSum univ

pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : β
⊢ Sum.inr val✝ ∈ univ.disjSum univ

Tactic:
<;>

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : α
⊢ Sum.inl val✝ ∈ univ.disjSum univ

case inr
α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
val✝ : β
⊢ Sum.inr val✝ ∈ univ.disjSum univ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

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

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

Tactic:
<;>

Goal state after:
case neg.h
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ s = s \ {i}

case neg.a
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ ∀ x ∈ s \ {i}, f x = f x
Module: Mathlib.Control.Applicative

Goal state before:
pp: case e_a.e_a
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ (fun a x ↦ Prod.mk <$> x <*> a) = fun a x2 ↦ (fun b a ↦ (a, b)) <$> a <*> x2

Tactic:
funext x y

Goal state after:
case e_a.e_a
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
x : g β✝
y : g α✝
⊢ Prod.mk <$> y <*> x = (fun b a ↦ (a, b)) <$> x <*> y