Theorem: Finsupp.prod_congr' (FltRegular/NumberTheory/Hilbert92.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ f₁.prod g1 = f₂.prod g2
Tactic:
classical
rw [f₁.prod_of_support_subset Finset.subset_union_left _ (fun i _ ↦ hg1 i),
  f₂.prod_of_support_subset Finset.subset_union_right _ (fun i _ ↦ hg2 i)]
exact Finset.prod_congr rfl (fun x _ ↦ h x)
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ f₁.prod g1 = f₂.prod g2
Tactic:
rw [f₁.prod_of_support_subset Finset.subset_union_left _ (fun i _ ↦ hg1 i),
  f₂.prod_of_support_subset Finset.subset_union_right _ (fun i _ ↦ hg2 i)]
State after:
p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ ∏ x ∈ f₁.support ∪ ?m.76044, g1 x (f₁ x) = ∏ x ∈ ?m.76647 ∪ f₂.support, g2 x (f₂ x)

p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α

p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α

p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α

State before:
p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ ∏ x ∈ f₁.support ∪ ?m.76044, g1 x (f₁ x) = ∏ x ∈ ?m.76647 ∪ f₂.support, g2 x (f₂ x)

p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α

p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α

p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
k : Type u_2
inst✝⁹ : Field k
inst✝⁸ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : CommGroup H
inst✝⁵ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝⁴ : DistribMulAction H G
inst✝³ : Module.Free ℤ G
inst✝² : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
α : Type u_5
M : Type u_6
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α
Tactic:
exact Finset.prod_congr rfl (fun x _ ↦ h x)
State after:
no goals