awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
convert_3 :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) a : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) b : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
⊢ HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max
      (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) a : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
      (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) b : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
convert_3 :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) (max ((v : (a : A) → Γ) a) ((v : (a : A) → Γ) b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ)
convert_3₁ convert_3₂ :
  HMul.hMul (α := Γ) (β := Γ) (max ((v : (a : A) → Γ) a) ((v : (a : A) → Γ) b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) (max ((v : (a : A) → Γ) a) ((v : (a : A) → Γ) b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) a : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) b : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))

Tactic:
grw [max_mul_mul_right, v.map_add a b]

Premises used: Valuation.map_add, max_mul_mul_right
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
x : A
y : ↥S
⊢ HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) x : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) ⋯ : (a : ↥S) → Γˣ) y)⁻¹ : Γ) : Γ) =
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) x : Γ) (((v : (a : A) → Γ) (↑y : A))⁻¹ : Γ)

Tactic:
simp [IsUnit.coe_liftRight]

Premises used: IsUnit.coe_liftRight
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
a : A
⊢ Eq.{u_2 + 1} (α := Γ) ((v.extendToLocalization hS B : (a : B) → Γ) ((algebraMap A B : (a : A) → B) a : B) : Γ)
    ((v : (a : A) → Γ) a : Γ)

Tactic:
Submonoid.LocalizationMap.lift_eq _ _ a

Premises used: Submonoid.LocalizationMap.lift_eq
-- Module: Mathlib.Tactic.CategoryTheory.CancelIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
rw : f ≫ inv f = 𝟙 x
⊢ f ≫ g = 𝟙 x

Tactic:
rw [← h]
-- Module: Mathlib.Tactic.CategoryTheory.CancelIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ inv f = 𝟙 x

Tactic:
IsIso.hom_inv_id f

Premises used: CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.Tactic.CategoryTheory.CancelIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ inv f = 𝟙 x

Tactic:
exact IsIso.hom_inv_id f

Premises used: CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.Tactic.CategoryTheory.CancelIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
rw : f ≫ inv f ≫ k = k
⊢ f ≫ g ≫ k = k

Tactic:
rw [← h]
-- Module: Mathlib.Tactic.CategoryTheory.CancelIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ inv f ≫ k = k

Tactic:
IsIso.hom_inv_id_assoc f k

Premises used: CategoryTheory.IsIso.hom_inv_id_assoc
-- Module: Mathlib.Tactic.CategoryTheory.CancelIso
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ inv f ≫ k = k

Tactic:
exact IsIso.hom_inv_id_assoc f k

Premises used: CategoryTheory.IsIso.hom_inv_id_assoc
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 0 < a
hb : 0 < b
pos : p → 0 < if p then a else b
neg : ¬p → 0 < if p then a else b
⊢ 0 < if p then a else b

Tactic:
by_cases p
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 0 < a
hb : 0 < b
h : p
⊢ 0 < if p then a else b

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 0 < a
hb : 0 < b
h : ¬p
⊢ 0 < if p then a else b

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 0 ≤ a
hb : 0 ≤ b
pos : p → 0 ≤ if p then a else b
neg : ¬p → 0 ≤ if p then a else b
⊢ 0 ≤ if p then a else b

Tactic:
by_cases p
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h : p
⊢ 0 ≤ if p then a else b

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h : ¬p
⊢ 0 ≤ if p then a else b

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : Preorder α
ha : 0 < a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b

Tactic:
ite_nonneg _ ha.le hb

Premises used: Mathlib.Meta.Positivity.ite_nonneg, LT.lt.le
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : Preorder α
ha : 0 ≤ a
hb : 0 < b
⊢ 0 ≤ if p then a else b

Tactic:
ite_nonneg _ ha hb.le

Premises used: Mathlib.Meta.Positivity.ite_nonneg, LT.lt.le
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
pos : p → (if p then a else b) ≠ 0
neg : ¬p → (if p then a else b) ≠ 0
⊢ (if p then a else b) ≠ 0

Tactic:
by_cases p
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : p
⊢ (if p then a else b) ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : ¬p
⊢ (if p then a else b) ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : Preorder α
ha : 0 < a
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0

Tactic:
ite_ne_zero _ ha.ne' hb

Premises used: LT.lt.ne', Mathlib.Meta.Positivity.ite_ne_zero
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : Preorder α
ha : a ≠ 0
hb : 0 < b
⊢ (if p then a else b) ≠ 0

Tactic:
ite_ne_zero _ ha hb.ne'

Premises used: LT.lt.ne', Mathlib.Meta.Positivity.ite_ne_zero
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
R : Type u_2
inst : LinearOrder R
a b c : R
ha : a < b
hb : a ≤ c
⊢ a ≤ min b c

Tactic:
le_min ha.le hb

Premises used: LT.lt.le, le_min
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
R : Type u_2
inst : LinearOrder R
a b c : R
ha : a ≤ b
hb : a < c
⊢ a ≤ min b c

Tactic:
le_min ha hb.le

Premises used: LT.lt.le, le_min
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
R : Type u_2
inst : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ min a b ≠ c

Tactic:
grind
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
R : Type u_2
inst : LinearOrder R
a b c : R
ha : a ≠ c
hb : c < b
⊢ min a b ≠ c

Tactic:
min_ne ha hb.ne'

Premises used: LT.lt.ne', Mathlib.Meta.Positivity.min_ne
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
R : Type u_2
inst : LinearOrder R
a b c : R
ha : c < a
hb : b ≠ c
⊢ min a b ≠ c

Tactic:
min_ne ha.ne' hb

Premises used: LT.lt.ne', Mathlib.Meta.Positivity.min_ne
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
R : Type u_2
inst : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ max a b ≠ c

Tactic:
grind
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
a : ℤ
ha : 0 < a
rw : LT.lt (α := ℤ) 0 1
⊢ 0 < a / a

Tactic:
rw [Int.ediv_self ha.ne']

Premises used: Int.ediv_self, LT.lt.ne'
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
a : ℤ
ha : 0 < a
⊢ LT.lt (α := ℤ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
a : ℤ
ha : 0 < a
⊢ LT.lt (α := ℤ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
a b : ℤ
ha : 0 < a
hb : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
Int.ediv_nonneg ha.le hb

Premises used: LT.lt.le, Int.ediv_nonneg
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
a b : ℤ
ha : 0 ≤ a
hb : 0 < b
⊢ 0 ≤ a / b

Tactic:
Int.ediv_nonneg ha hb.le

Premises used: LT.lt.le, Int.ediv_nonneg
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
a b : ℤ
ha : 0 < a
hb : 0 < b
⊢ 0 ≤ a / b

Tactic:
Int.ediv_nonneg ha.le hb.le

Premises used: LT.lt.le, Int.ediv_nonneg
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Nontrivial α
a : α
⊢ 0 < HPow.hPow (β := ℕ) a 0

Tactic:
zero_lt_one.trans_le (pow_zero a).ge

Premises used: Eq.ge, pow_zero, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_2
inst : AddGroup α
inst_1 : LinearOrder α
inst_2 : AddLeftMono α
a : α
⊢ a ≠ 0 → 0 < |a|

Tactic:
abs_pos.mpr

Premises used: Iff.mpr, abs_pos
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
n : ℤ
hn : 0 < n
⊢ 0 < n.natAbs

Tactic:
Int.natAbs_pos.mpr hn.ne'

Premises used: Iff.mpr, Int.natAbs_pos, LT.lt.ne'
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
q : ℚ≥0
hq : 0 < q
⊢ 0 < q.num

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
q : ℚ≥0
hq : q ≠ 0
⊢ q.num ≠ 0

Tactic:
positivity
-- Module: Mathlib.Tactic.Positivity.Basic
Goal:
α : Type u_1
q : ℚ≥0
⊢ 0 < q.den

Tactic:
positivity
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
⊢ HasProd (fun (b' : β) ↦ if b' = b then a else 1) a

Tactic:
hasProd_ite_eq (L := .unconditional β) b a

Premises used: hasProd_ite_eq, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
h : ∀ (x : β), Pi.mulSingle (M := fun (a : β) ↦ α) b a x = if x = b then a else 1
⊢ HasProd (Pi.mulSingle (M := fun (a : β) ↦ α) b a) a

Tactic:
convert! hasProd_ite_eq (L := .unconditional β) b a

Premises used: hasProd_ite_eq, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
x : β
⊢ Pi.mulSingle (M := fun (a : β) ↦ α) b a x = if x = b then a else 1

Tactic:
simp [Pi.mulSingle_apply]

Premises used: Pi.mulSingle_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
rw : Pi.mulSingle (M := fun (a : β) ↦ α) b a b = a
rw₁ : ∀ (b' : β), b' ≠ b → Eq.{u_1 + 1} (α := α) (Pi.mulSingle (M := fun (a : β) ↦ α) b a b' : α) (1 : α)
⊢ ∏' (b' : β), Pi.mulSingle (M := fun (a : β) ↦ α) b a b' = a

Tactic:
rw [tprod_eq_mulSingle b]

Premises used: tprod_eq_mulSingle
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
⊢ Pi.mulSingle (M := fun (a : β) ↦ α) b a b = a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Eq.{u_1 + 1} (α := α) (Pi.mulSingle (M := fun (a : β) ↦ α) b a b' : α) (1 : α)

Tactic:
simp [hb']
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
b : β
t : Set γ
f : β × γ → α
rw :
  Eq.{u_1 + 1} (α := α) (∏' (x : (↑(Prod.mk b '' t) : Type (max u_3 u_2))), f (↑x : β × γ))
    (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (∏' (x : (↑t : Type u_3)), f (b, (↑x : γ))) (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(SProd.sprod (α := Set β) {b} t) : Type (max u_3 u_2))), f (↑x : β × γ))
    (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))

Tactic:
rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ (Prod.mk_right_injective b).injOn]

Premises used: tprod_image, Function.Injective.injOn, Set.singleton_prod, Prod.mk_right_injective, tprod_congr_set_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
c : γ
f : β × γ → α
rw :
  Eq.{u_1 + 1} (α := α) (∏' (x : (↑((fun (a : β) ↦ (a, c)) '' s) : Type (max u_3 u_2))), f (↑x : β × γ))
    (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (∏' (x : (↑s : Type u_2)), f ((↑x : β), c)) (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(SProd.sprod (β := Set γ) s {c}) : Type (max u_2 u_3))), f (↑x : β × γ))
    (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))

Tactic:
rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ (Prod.mk_left_injective c).injOn]

Premises used: tprod_image, Function.Injective.injOn, Set.prod_singleton, Prod.mk_left_injective, tprod_congr_set_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β × γ → α
hf : Multipliable f
⊢ Multipliable (α := α) fun (p : γ × β) ↦ f p.swap

Tactic:
(Equiv.prodComm γ β).multipliable_iff.2 hf

Premises used: Iff.mpr, Equiv.prodComm, Prod.swap, Equiv.multipliable_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
f : β → α
g : β → γ
a : α
b : γ
hf : HasProd f a L
hg : HasProd g b L
⊢ HasProd (fun (x : β) ↦ (f x, g x)) (a, b) L

Tactic:
simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prodMk_nhds hf hg]

Premises used: HasProd, prod_mk_prod, SummationFilter.unconditional, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
rw :
  Tendsto
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    (SProd.sprod (α := Filter (Finset α)) (β := Filter (Finset β)) atTop atTop) (𝓝 (a * b))
⊢ Tendsto (α := Prod.{u_4, u_5} (Finset α) (Finset β))
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    (Filter.map (α := Finset (α ⊕ β)) (⇑sumEquiv : (a : Finset (α ⊕ β)) → Finset α × Finset β) atTop) (𝓝 (a * b))

Tactic:
rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]

Premises used: Finset.sumEquiv, Filter.prod_atTop_atTop_eq, OrderIso.map_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto
    ((fun (p : M × M) ↦ p.1 * p.2) ∘
      Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)
    ((SummationFilter.unconditional α).filter ×ˢ (SummationFilter.unconditional β).filter) (𝓝 (a * b))

Tactic:
(tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))

Premises used: tendsto_mul, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
h :
  Eq (α := Prod.{u_4, u_5} (Finset α) (Finset β) → M)
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    ((fun (p : M × M) ↦ p.1 * p.2) ∘
      Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)
⊢ Tendsto
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    (SProd.sprod (α := Filter (Finset α)) (β := Filter (Finset β)) atTop atTop) (𝓝 (a * b))

Tactic:
convert! (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))

Premises used: tendsto_mul, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
h :
  ∀ (s : Prod.{u_4, u_5} (Finset α) (Finset β)),
    Eq.{u_6 + 1} (α := M)
      (((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
          (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
        s)
      (((fun (p : M × M) ↦ p.1 * p.2) ∘
          Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)
        s)
⊢ Eq (α := Prod.{u_4, u_5} (Finset α) (Finset β) → M)
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    ((fun (p : M × M) ↦ p.1 * p.2) ∘
      Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)

Tactic:
ext s
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
s : Prod.{u_4, u_5} (Finset α) (Finset β)
⊢ Eq.{u_6 + 1} (α := M)
    (((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
        (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
      s)
    (((fun (p : M × M) ↦ p.1 * p.2) ∘
        Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)
      s)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto (α := Prod.{u_4, u_5} (Finset α) (Finset β))
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    (Filter.map (α := Finset (α ⊕ β)) (⇑sumEquiv : (a : Finset (α ⊕ β)) → Finset α × Finset β) atTop) (𝓝 (a * b))

Tactic:
have : Tendsto ((∏ b ∈ ·, f b) ∘ sumEquiv.symm) (atTop.map sumEquiv) (nhds (a * b)) := by
    rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]
    convert! (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))
    ext s
    simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
this :
  Tendsto (α := Prod.{u_4, u_5} (Finset α) (Finset β))
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    (Filter.map (α := Finset (α ⊕ β)) (⇑sumEquiv : (a : Finset (α ⊕ β)) → Finset α × Finset β) atTop) (𝓝 (a * b))
⊢ HasProd f (a * b)

Tactic:
simpa [Tendsto, ← Filter.map_map] using this

Premises used: Filter.map_map, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : T2Space M
f : α ⊕ β → M
h₁ : Multipliable (f ∘ Sum.inl)
h₂ : Multipliable (f ∘ Sum.inr)
⊢ ∏' (i : α ⊕ β), f i = HMul.hMul (α := M) (∏' (i : α), f (Sum.inl i)) (∏' (i : β), f (Sum.inr i))

Tactic:
(h₁.hasProd.sum h₂.hasProd).tprod_eq

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
h₁ : Multipliable (f ∘ Sum.inl)
h₂ : Multipliable (f ∘ Sum.inr)
⊢ Multipliable f

Tactic:
⟨_, .sum h₁.hasProd h₂.hasProd⟩

Premises used: Multipliable, Multipliable.hasProd, Exists.intro, HasProd.sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
⊢ HasProd g a

Tactic:
(atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_

Premises used: Iff.mpr, Filter.atTop_basis, iInf, Filter.HasBasis.tendsto_iff, closed_nhds_basis, HasProd, Filter.atTop