Theorem: Finset.prod_erase_attach (ForML/FDerivProd.lean)

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in erase (attach s) i, f ↑j = ∏ j in erase s ↑i, f j
Tactic:
simp only [erase_eq]
State after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ x in attach s \ {i}, f ↑x = ∏ x in s \ {↑i}, f x

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ x in attach s \ {i}, f ↑x = ∏ x in s \ {↑i}, f x
Tactic:
rw [← prod_update_one_of_mem i.prop, ← prod_update_one_of_mem (mem_attach s i)]
State after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j = ∏ j in s, Function.update (fun x => f x) (↑i) 1 j

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j = ∏ j in s, Function.update (fun x => f x) (↑i) 1 j
Tactic:
rw [← prod_coe_sort s]
State after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j =
    ∏ i_1 : { x // x ∈ s }, Function.update (fun x => f x) (↑i) 1 ↑i_1

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j =
    ∏ i_1 : { x // x ∈ s }, Function.update (fun x => f x) (↑i) 1 ↑i_1
Tactic:
refine prod_congr rfl ?_
State after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∀ x ∈ univ, Function.update (fun x => f ↑x) i 1 x = Function.update (fun x => f x) (↑i) 1 ↑x

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∀ x ∈ univ, Function.update (fun x => f ↑x) i 1 x = Function.update (fun x => f x) (↑i) 1 ↑x
Tactic:
intro j _
State after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update (fun x => f x) (↑i) 1 ↑j

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update (fun x => f x) (↑i) 1 ↑j
Tactic:
simp only [← Function.comp_apply (g := Subtype.val) (x := j)]
State after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = (Function.update (fun x => f x) (↑i) 1 ∘ Subtype.val) j

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = (Function.update (fun x => f x) (↑i) 1 ∘ Subtype.val) j
Tactic:
rw [Function.update_comp_eq_of_injective _ Subtype.val_injective]
State after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update ((fun x => f x) ∘ Subtype.val) i 1 j

State before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update ((fun x => f x) ∘ Subtype.val) i 1 j
Tactic:
rfl
State after:
no goals