awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
rw : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)
rw₁ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y + -x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
rw₂ : Eq (α := ℝ) ((v : (a : R) → ℝ) (y - x) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
rw₃ : Eq (α := ℝ) ((v : (a : R) → ℝ) (x - y) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
rw₄ rw₅ : Eq (α := ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ) ((v : (a : R) → ℝ) (x + -y) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) ((v : (a : R) → ℝ) (-y + x) : ℝ)

Tactic:
rw [add_comm (-x), add_comm (-y), ← sub_eq_add_neg, v.map_sub, sub_eq_add_neg]

Premises used: sub_eq_add_neg, add_comm, AbsoluteValue.map_sub, Neg.neg
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y z : R
⊢ (v : (a : R) → ℝ) (-x + z) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) ((v : (a : R) → ℝ) (-y + z) : ℝ)

Tactic:
simpa [neg_add_eq_sub, add_comm (v (y - x))] using v.sub_le z y x

Premises used: neg_add_eq_sub, HSub.hSub, add_comm, AbsoluteValue.sub_le, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + y) : ℝ) (0 : ℝ)
⊢ y = x

Tactic:
rw [add_comm, ← sub_eq_add_neg, AbsoluteValue.map_sub_eq_zero_iff] at hxy

Premises used: AbsoluteValue.map_sub_eq_zero_iff, sub_eq_add_neg, add_comm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : y = x
⊢ x = y

Tactic:
hxy.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : y = x
⊢ x = y

Tactic:
exact hxy.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
inl :
  IsEmpty ι →
    ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
inr :
  Nonempty ι →
    ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))

Tactic:
rcases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : IsEmpty ι
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
inr :
  IsEmpty ι' →
    ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
inr₁ :
  Nonempty ι' →
    ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
      HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))

Tactic:
rcases isEmpty_or_nonempty ι'

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
h_1 : IsEmpty ι'
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
h_1 : Nonempty ι'
inr :
  Eq (α := ℝ) (⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2))
    (⨆ (i : ι), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j) : ℝ))
inr₁ :
  Eq (α := ℝ) (⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2))
    (⨆ (i : ι), ⨆ (i_1 : ι'), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) ((v : (a : R) → ℝ) (y i_1) : ℝ))
inr₂ :
  Eq (α := ℝ)
    (⨆ (a : ι × ι'), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x a.1) : ℝ) ((v : (a : R) → ℝ) (y a.2) : ℝ))
    (⨆ (i : ι), ⨆ (i_1 : ι'), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) ((v : (a : R) → ℝ) (y i_1) : ℝ))
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))

Tactic:
simp_rw [Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),
    Real.mul_iSup_of_nonneg (apply_nonneg v _), map_mul, Finite.ciSup_prod]

Premises used: Finite.ciSup_prod, map_mul, Real.iSup_mul_of_nonneg, NonnegHomClass.apply_nonneg, Real.iSup_nonneg, Real.mul_iSup_of_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
inl :
  ∀ (h : IsEmpty ((a : α) → ι a)), Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
inr :
  ∀ (h : Nonempty ((a : α) → ι a)),
    Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)

Tactic:
rcases isEmpty_or_nonempty ((a : α) → ι a) with h | h

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
inl : ∃ (a : α), Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)

Tactic:
rw [iSup_of_isEmpty, eq_comm, Finset.prod_eq_zero_iff]

Premises used: eq_comm, Real.iSup_of_isEmpty, Finset.prod_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
inl :
  ∀ (a : α) (ha : IsEmpty.{u + 1} (ι a)),
    ∃ (a : α), Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0
⊢ ∃ (a : α), Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0

Tactic:
obtain ⟨a, ha⟩ := isEmpty_pi.mp h

Premises used: isEmpty_pi, Iff.mp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
a : α
ha : IsEmpty.{u + 1} (ι a)
⊢ Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
a : α
ha : IsEmpty.{u + 1} (ι a)
⊢ ∃ (a : α), Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0

Tactic:
exact ⟨a, by simp⟩
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
inr : LE.le (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
inr₁ : LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
i : (a : α) → ι a
⊢ ∀ (i_1 : α), Membership.mem (γ := Finset α) Finset.univ i_1 → 0 ≤ f i_1 (i i_1)

Tactic:
simp [hf₀]
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ LE.le (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)

Tactic:
exact ciSup_le fun i ↦ Finset.prod_le_prod (by simp [hf₀])
      fun a ha ↦ Finite.le_ciSup_of_le _ le_rfl

Premises used: le_rfl, Finset.prod_le_prod, Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ ∀ (i : α), Nonempty.{u + 1} (ι i)

Tactic:
rw [Classical.nonempty_pi] at h

Premises used: Classical.nonempty_pi
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
⊢ ∀ (a : α), ∃ (i : ι a), f a i = ⨆ (i : ι a), f a i

Tactic:
have H a : ∃ i : ι a, f a i = ⨆ i, f a i := exists_eq_ciSup_of_finite
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
H : ∀ (a : α), ∃ (i : ι a), f a i = ⨆ (i : ι a), f a i
inr :
  ∀ (i : (a : α) → ι a) (hi : ∀ (a : α), f a (i a) = ⨆ (i : ι a), f a i),
    LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
⊢ LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))

Tactic:
choose i hi using H
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
i : (a : α) → ι a
hi : ∀ (a : α), f a (i a) = ⨆ (i : ι a), f a i
inr : LE.le (α := ℝ) (∏ x : α, f x (i x)) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
⊢ LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))

Tactic:
simp only [← hi]
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
i : (a : α) → ι a
hi : ∀ (a : α), f a (i a) = ⨆ (i : ι a), f a i
⊢ LE.le (α := ℝ) (∏ x : α, f x (i x)) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))

Tactic:
Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
i : (a : α) → ι a
hi : ∀ (a : α), f a (i a) = ⨆ (i : ι a), f a i
⊢ LE.le (α := ℝ) (∏ x : α, f x (i x)) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_5
R : Type u_6
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
F : Type u_7
inst_2 : FunLike F R ℝ
inst_3 : NonnegHomClass F R ℝ
v : F
x : (a : α) → ι a → R
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, (v : (a : R) → ℝ) (x a (i a)))
    (∏ a : α, ⨆ (i : ι a), (v : (a : R) → ℝ) (x a i))

Tactic:
Real.iSup_prod_eq_prod_iSup_of_nonneg (f := fun a i ↦ v (x a i)) (fun _ _ ↦ apply_nonneg v _)

Premises used: Real.iSup_prod_eq_prod_iSup_of_nonneg, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.Finite
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormMulClass α
inst_2 : NormOneClass α
a : α
ha : IsOfFinOrder a
⊢ ‖a‖ = 1

Tactic:
((normHom : α →*₀ ℝ).toMonoidHom.isOfFinOrder ha).eq_one <| norm_nonneg _

Premises used: MonoidHom.isOfFinOrder, IsOfFinOrder.eq_one, MonoidWithZeroHom.toMonoidHom, norm_nonneg, normHom
-- Module: Mathlib.Analysis.Normed.Ring.Finite
Goal:
α : Type u_1
β : Type u_2
inst : NormedRing α
inst_1 : NormMulClass α
inst_2 : NormOneClass α
a : α
inst_3 : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ (↑k : ℕ) = 1
⊢ norm.{u_1} (E := α) ((φ : (a : β) → α) x : α) = 1

Tactic:
(φ.isOfFinOrder <| isOfFinOrder_iff_pow_eq_one.2 ⟨_, k.2, h⟩).norm_eq_one

Premises used: Iff.mpr, MonoidHom.isOfFinOrder, And.intro, IsOfFinOrder.norm_eq_one, Exists.intro, isOfFinOrder_iff_pow_eq_one, Subtype.property
-- Module: Mathlib.Analysis.Normed.Ring.Finite
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormMulClass α
inst_2 : NormOneClass α
G : Type u_3
inst_3 : AddLeftCancelMonoid G
inst_4 : Finite G
ψ : AddChar G α
x : G
⊢ norm.{u_1} (E := α) ((ψ : (a : G) → α) x : α) = 1

Tactic:
(ψ.toMonoidHom.isOfFinOrder <| isOfFinOrder_of_finite _).norm_eq_one

Premises used: MonoidHom.isOfFinOrder, AddChar.toMonoidHom, isOfFinOrder_of_finite, IsOfFinOrder.norm_eq_one
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
inl :
  ∀ (hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) ⊥ (𝓝 (g k)))
    (h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k),
    Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))
inr : 𝓕.NeBot → Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))

Tactic:
rcases eq_or_neBot 𝓕 with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) ⊥ (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
⊢ ∀ (k : β), ‖g k‖ ≤ bound k

Tactic:
have h_bound_g (k) : ‖g k‖ ≤ bound k :=
    le_of_tendsto ((hab k).norm) (h_bound.mono fun n hn ↦ hn k)
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
⊢ Summable (α := ℝ) fun (x : β) ↦ ‖g x‖

Tactic:
have hsum_g : Summable (‖g ·‖) := h_sum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) h_bound_g
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
inr : Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∑' (s : Finset β), ∏ i ∈ s, g i))
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))

Tactic:
rw [show ∏' k, (1 + g k) = ∑' s, ∏ i ∈ s, g i from
    tprod_one_add (summable_finsetProd_of_summable_norm hsum_g)]

Premises used: tprod_one_add, summable_finsetProd_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
n : α
hn : ∀ (k : β), ‖f n k‖ ≤ bound k
s : Finset β
⊢ ∀ i ∈ s, 0 ≤ ‖f n i‖

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
n : α
hn : ∀ (k : β), ‖f n k‖ ≤ bound k
s : Finset β
⊢ ∀ i ∈ s, ‖f n i‖ ≤ bound i

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))

Tactic:
have : Tendsto (∑' k, ∏ c ∈ k, f · c) 𝓕 (𝓝 (∑' k, ∏ c ∈ k, g c)) :=
    tendsto_tsum_of_dominated_convergence (summable_finsetProd_of_summable_nonneg
      (fun i ↦ (norm_nonneg (g i)).trans (h_bound_g i)) h_sum)
      (tendsto_finsetProd · fun i _ ↦ hab i)
      (h_bound.mono fun n hn s ↦ (Finset.norm_prod_le s (f n)).trans
      (Finset.prod_le_prod (by grind) (by grind)))
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
this :
  Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))
apply :
  ∀ (n : α) (hn : ∀ (k : β), ‖f n k‖ ≤ bound k),
    Eq.{u_2 + 1} (α := R) (∑' (k : Finset β), ∏ c ∈ k, f n c) (∏' (k : β), (1 + f n k))
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∑' (s : Finset β), ∏ i ∈ s, g i))

Tactic:
apply this.congr' (h_bound.mono fun n hn ↦ ?_)

Premises used: Filter.Eventually.mono, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
this :
  Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))
n : α
hn : ∀ (k : β), ‖f n k‖ ≤ bound k
rw : Summable.{u_2, u_3} (α := R) fun (x : Finset β) ↦ ∏ i ∈ x, f n i
⊢ Eq.{u_2 + 1} (α := R) (∑' (k : Finset β), ∏ c ∈ k, f n c) (∏' (k : β), (1 + f n k))

Tactic:
rw [tprod_one_add]

Premises used: tprod_one_add
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
this :
  Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))
n : α
hn : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ∀ (b : β), 0 ≤ ‖f n b‖

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteProd
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
this :
  Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))
n : α
hn : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Summable.{u_2, u_3} (α := R) fun (x : Finset β) ↦ ∏ i ∈ x, f n i

Tactic:
exact summable_finsetProd_of_summable_norm <| h_sum.of_nonneg_of_le (by grind) hn

Premises used: Summable.of_nonneg_of_le, summable_finsetProd_of_summable_norm
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
ι : Type u_2
ι' : Type u_3
f : ι → ℝ
g : ι' → ℝ
hf : Summable f
hg : Summable g
hf' : 0 ≤ f
hg' : 0 ≤ g
⊢ Summable (α := ℝ) fun (x : ι) ↦ ∑' (y : ι'), f (x, y).1 * g (x, y).2

Tactic:
simpa only [hg.tsum_mul_left _] using hf.mul_right (∑' x, g x)

Premises used: Summable.mul_right, Summable.tsum_mul_left, tsum, SummationFilter.unconditional