awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Ring.Nat
Goal:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, Set.Finite.{u_1} (α := ι) {a : ι | f a = b}
s₁ s₂ s₃ : Nat.card.{u_1} (↑(f ⁻¹' (↑s : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
s₄ :
  let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯;
  Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }
s₅ :
  let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯;
  Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1)
s₆ :
  let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯;
  ∀ (ht : (f ⁻¹' (↑t : Set M)).Finite),
    Nat.card.{u_1} (↑(f ⁻¹' (↑t : Set M)) : Type u_1) = ∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1)
s₇ :
  let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯;
  ∀ (ht : (f ⁻¹' (↑t : Set M)).Finite),
    Eq (α := ℕ)
      (∑ b ∈ image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))), #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = b}))
      (∑ b ∈ t, Nat.card.{u_1} (↑{a : ι | f a = b} : Type u_1))
refine_1 :
  let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯;
  ∀ (ht : (f ⁻¹' (↑t : Set M)).Finite), image f (ht.toFinset (s := f ⁻¹' (↑t : Set M))) = t
refine_2 refine_2₁ :
  let t := Set.Finite.toFinset (s := (↑s : Set M) ∩ Set.range f) ⋯;
  ∀ (ht : (f ⁻¹' (↑t : Set M)).Finite) (m : M) (hm : m ∈ t),
    #({a ∈ ht.toFinset (s := f ⁻¹' (↑t : Set M)) | f a = m}) = Nat.card.{u_1} (↑{a : ι | f a = m} : Type u_1)
⊢ Nat.card.{u_1} (↑(f ⁻¹' (↑s : Set M)) : Type u_1) = ∑ b ∈ s, Nat.card.{u_1} { a : ι // f a = b }

Tactic:
classical
  -- `t = s ∩ Set.range f` as a `Finset`
  let t := (Set.finite_coe_iff.mp (Finite.Set.finite_inter_of_left ↑s (Set.range f))).toFinset
  rw [show Nat.card (f ⁻¹' s) = Nat.card (f ⁻¹' t) by simp [t]]
  rw [show ∑ b ∈ s, Nat.card {a //f a = b} = ∑ b ∈ t, Nat.card {a | f a = b} by
    exact (Finset.sum_subset (by simp [t]) (by aesop)).symm]
  have ht : Set.Finite (f ⁻¹' t) := Set.Finite.preimage' (finite_toSet t) (by aesop)
  rw [Nat.card_eq_card_finite_toFinset ht, Finset.card_eq_sum_card_image (f := f)]
  refine Finset.sum_congr ?_ fun m hm ↦ ?_
  · simpa [← Finset.coe_inj, t] using Set.image_preimage_eq_inter_range
  · rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]
    suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)
    intro _ h
    simp_all

Premises used: Finset.coe_inj, Set.image_preimage_eq_inter_range, Finset.sum_congr, Nat.card_eq_card_finite_toFinset
-- Module: Mathlib.Algebra.BigOperators.RingEquiv
Goal:
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
l : List R
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) l.prod : S) (List.prod (List.map (⇑f : (a : R) → S) l) : S)

Tactic:
map_list_prod f l

Premises used: map_list_prod
-- Module: Mathlib.Algebra.BigOperators.RingEquiv
Goal:
R : Type u_2
S : Type u_3
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
l : List R
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) l.sum : S) (List.sum (List.map (⇑f : (a : R) → S) l) : S)

Tactic:
map_list_sum f l

Premises used: map_list_sum
-- Module: Mathlib.Algebra.BigOperators.RingEquiv
Goal:
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : RingEquiv.{u_2, u_3} R Sᵐᵒᵖ
l : List R
⊢ Eq.{u_3 + 1} (α := S) (MulOpposite.unop ((f : (a : R) → Sᵐᵒᵖ) l.prod))
    (List.prod (List.reverse (List.map (MulOpposite.unop ∘ (⇑f : (a : R) → Sᵐᵒᵖ)) l)))

Tactic:
unop_map_list_prod f l

Premises used: unop_map_list_prod
-- Module: Mathlib.Algebra.BigOperators.RingEquiv
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
f : R ≃+* S
s : Multiset R
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) s.prod : S) (Multiset.prod (Multiset.map (⇑f : (a : R) → S) s) : S)

Tactic:
map_multiset_prod f s

Premises used: map_multiset_prod
-- Module: Mathlib.Algebra.BigOperators.RingEquiv
Goal:
R : Type u_2
S : Type u_3
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
s : Multiset R
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) s.sum : S) (Multiset.sum (Multiset.map (⇑f : (a : R) → S) s) : S)

Tactic:
map_multiset_sum f s

Premises used: map_multiset_sum
-- Module: Mathlib.Algebra.BigOperators.RingEquiv
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
g : R ≃+* S
f : α → R
s : Finset α
⊢ Eq.{u_3 + 1} (α := S) ((g : (a : R) → S) (∏ x ∈ s, f x) : S) (∏ x ∈ s, (g : (a : R) → S) (f x) : S)

Tactic:
map_prod g f s

Premises used: map_prod
-- Module: Mathlib.Algebra.BigOperators.RingEquiv
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
g : R ≃+* S
f : α → R
s : Finset α
⊢ Eq.{u_3 + 1} (α := S) ((g : (a : R) → S) (∑ x ∈ s, f x) : S) (∑ x ∈ s, (g : (a : R) → S) (f x) : S)

Tactic:
map_sum g f s

Premises used: map_sum
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
ι : Type u_1
M : Type u_2
inst : LinearOrder ι
inst_1 : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
rw : Eq.{u_2 + 1} (α := M) (∑ i ∈ s.sym2 with ¬i.IsDiag, p i) (∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2))
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ s.sym2 with ¬i.IsDiag, p i) (∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2))

Tactic:
rw [Finset.offDiag_filter_lt_eq_filter_le]

Premises used: Finset.offDiag_filter_lt_eq_filter_le
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
ι : Type u_1
M : Type u_2
inst : LinearOrder ι
inst_1 : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
rw : ∑ x ∈ Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag, p s((↑x : ι × ι).1, (↑x : ι × ι).2)
| ∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2)

Tactic:
rw [← Finset.sum_subtype_eq_sum_filter]

Premises used: Finset.sum_subtype_eq_sum_filter
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
ι : Type u_1
M : Type u_2
inst : LinearOrder ι
inst_1 : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
conv_rhs :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ s.sym2 with ¬i.IsDiag, p i)
    (∑ x ∈ Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag, p s((↑x : ι × ι).1, (↑x : ι × ι).2))
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ s.sym2 with ¬i.IsDiag, p i) (∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2))

Tactic:
conv_rhs => rw [← Finset.sum_subtype_eq_sum_filter]

Premises used: Finset.sum_subtype_eq_sum_filter
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
ι : Type u_1
M : Type u_2
inst : LinearOrder ι
inst_1 : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ s.sym2 with ¬i.IsDiag, p i)
    (∑ x ∈ Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag, p s((↑x : ι × ι).1, (↑x : ι × ι).2))

Tactic:
(Finset.sum_equiv Sym2.sortEquiv.symm ?_ ?_).symm

Premises used: Sym2.sortEquiv, Equiv.symm, Eq.symm, Finset.sum_equiv
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
ι : Type u_1
M : Type u_2
inst : LinearOrder ι
inst_1 : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
refine_1 :
  ∀ (i : { p : ι × ι // p.1 ≤ p.2 }),
    Membership.mem (γ := Finset { p : ι × ι // p.1 ≤ p.2 }) (Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag) i ↔
      Membership.mem (α := Sym2 ι) ({i ∈ s.sym2 | ¬i.IsDiag})
        ((Equiv.symm Sym2.sortEquiv : (a : { p : ι × ι // p.1 ≤ p.2 }) → Sym2 ι) i : Sym2 ι)
refine_2 :
  ∀ (i : { p : ι × ι // p.1 ≤ p.2 }),
    Membership.mem (γ := Finset { p : ι × ι // p.1 ≤ p.2 }) (Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag) i →
      p s((↑i : ι × ι).1, (↑i : ι × ι).2) =
        p ((Equiv.symm Sym2.sortEquiv : (a : { p : ι × ι // p.1 ≤ p.2 }) → Sym2 ι) i)
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ s.sym2 with ¬i.IsDiag, p i)
    (∑ x ∈ Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag, p s((↑x : ι × ι).1, (↑x : ι × ι).2))

Tactic:
refine (Finset.sum_equiv Sym2.sortEquiv.symm ?_ ?_).symm

Premises used: Sym2.sortEquiv, Equiv.symm, Eq.symm, Finset.sum_equiv
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
ι : Type u_1
M : Type u_2
inst : LinearOrder ι
inst_1 : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∀ (i : { p : ι × ι // p.1 ≤ p.2 }),
    Membership.mem (γ := Finset { p : ι × ι // p.1 ≤ p.2 }) (Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag) i ↔
      Membership.mem (α := Sym2 ι) ({i ∈ s.sym2 | ¬i.IsDiag})
        ((Equiv.symm Sym2.sortEquiv : (a : { p : ι × ι // p.1 ≤ p.2 }) → Sym2 ι) i : Sym2 ι)

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
ι : Type u_1
M : Type u_2
inst : LinearOrder ι
inst_1 : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∀ (i : { p : ι × ι // p.1 ≤ p.2 }),
    Membership.mem (γ := Finset { p : ι × ι // p.1 ≤ p.2 }) (Finset.subtype (fun (i : ι × ι) ↦ i.1 ≤ i.2) s.offDiag) i →
      p s((↑i : ι × ι).1, (↑i : ι × ι).2) =
        p ((Equiv.symm Sym2.sortEquiv : (a : { p : ι × ι // p.1 ≤ p.2 }) → Sym2 ι) i)

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Sym
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
k : Sym α m
s : Finset α
hk : k ∈ s.sym m
⊢ ∑ i ∈ s, count i (↑k : Multiset α) = m

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_2 + 1} (α := WithTop M) (↑(∑ i ∈ s, f i) : WithTop M) (∑ i ∈ s, (↑(f i) : WithTop M))

Tactic:
map_sum addHom f s

Premises used: map_sum, WithTop.some, WithTop.addHom
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
empty : Eq.{u_2 + 1} (α := WithTop M) (∑ i ∈ ∅, f i) ⊤ ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = ⊤
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (Eq.{u_2 + 1} (α := WithTop M) (∑ i ∈ s, f i) ⊤ ↔ ∃ i ∈ s, f i = ⊤) →
      (Eq.{u_2 + 1} (α := WithTop M) (∑ i ∈ Finset.cons a s h, f i) ⊤ ↔ ∃ i ∈ Finset.cons a s h, f i = ⊤)
⊢ Eq.{u_2 + 1} (α := WithTop M) (∑ i ∈ s, f i) ⊤ ↔ ∃ i ∈ s, f i = ⊤

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ Eq.{u_2 + 1} (α := WithTop M) (∑ i ∈ ∅, f i) ⊤ ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = ⊤

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
a : ι
s_1 : Finset ι
h : a ∉ s_1
h_1 : Eq.{u_2 + 1} (α := WithTop M) (∑ i ∈ s_1, f i) ⊤ ↔ ∃ i ∈ s_1, f i = ⊤
⊢ Eq.{u_2 + 1} (α := WithTop M) (∑ i ∈ cons a s_1 h, f i) ⊤ ↔ ∃ i ∈ cons a s_1 h, f i = ⊤

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ Ne.{u_2 + 1} (α := WithTop M) (∑ i ∈ s, f i) ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
inst_1 : LT M
⊢ LT.lt.{u_2} (α := WithTop M) (∑ i ∈ s, f i) ⊤ ↔ ∀ i ∈ s, f i < ⊤

Tactic:
simp [WithTop.lt_top_iff_ne_top]

Premises used: WithTop.lt_top_iff_ne_top
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
h : ∀ i ∈ s, f i ≠ ⊤
⊢ Ne.{u_3 + 1} (α := WithTop M₀) (∏ i ∈ s, f i) ⊤

Tactic:
prod_induction f (· ≠ ⊤) (fun _ _ ↦ mul_ne_top) coe_ne_top h

Premises used: WithTop.mul_ne_top, Ne, Finset.prod_induction, WithTop.coe_ne_top, Top.top
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
inst_4 : LT M₀
h : ∀ i ∈ s, f i < ⊤
⊢ LT.lt.{u_3} (α := WithTop M₀) (∏ i ∈ s, f i) ⊤

Tactic:
prod_induction f (· < ⊤) (fun _ _ ↦ mul_lt_top) (coe_lt_top _) h

Premises used: WithTop.coe_lt_top, Finset.prod_induction, LT.lt, WithTop.mul_lt_top, Top.top
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
rw : (∏ x ∈ s.erase i, f x) * f i = ⊤
⊢ Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤

Tactic:
rw [← prod_erase_mul _ _ hi]

Premises used: Finset.prod_erase_mul
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
classical : (∏ x ∈ s.erase i, f x) * f i = ⊤
⊢ Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤

Tactic:
classical rw [← prod_erase_mul _ _ hi]
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ (∏ x ∈ s.erase i, f x) * f i = ⊤

Tactic:
WithTop.mul_eq_top_iff.mpr (Or.inl ⟨?_, hi'⟩)

Premises used: Iff.mpr, And.intro, Or.inl, WithTop.mul_eq_top_iff
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
refine : Ne.{u_3 + 1} (α := WithTop M₀) (∏ x ∈ s.erase i, f x) 0
⊢ (∏ x ∈ s.erase i, f x) * f i = ⊤

Tactic:
refine WithTop.mul_eq_top_iff.mpr (Or.inl ⟨?_, hi'⟩)

Premises used: Iff.mpr, And.intro, Or.inl, WithTop.mul_eq_top_iff
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ Ne.{u_3 + 1} (α := WithTop M₀) (∏ x ∈ s.erase i, f x) 0

Tactic:
prod_ne_zero_iff.mpr ?_

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
refine : ∀ a ∈ s.erase i, f a ≠ 0
⊢ Ne.{u_3 + 1} (α := WithTop M₀) (∏ x ∈ s.erase i, f x) 0

Tactic:
refine prod_ne_zero_iff.mpr ?_

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
a : ι
h_1 : a ∈ s.erase i
⊢ f a ≠ 0

Tactic:
simp_all only [ne_eq, mem_erase, not_false_eq_true]

Premises used: ne_eq, Finset.mem_erase, not_false_eq_true
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
h : Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
by_contra! : ∀ (h0 : f i = 0), False
⊢ f i ≠ 0

Tactic:
by_contra! h0
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
h : Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
h0 : f i = 0
apply : Eq.{u_3 + 1} (α := WithTop M₀) ⊤ 0
⊢ False

Tactic:
apply WithTop.top_ne_zero (α := M₀)

Premises used: WithTop.top_ne_zero
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
h : Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
h0 : f i = 0
⊢ Eq.{u_3 + 1} (α := WithTop M₀) ⊤ (∏ j ∈ s, f j)

Tactic:
Eq.symm h

Premises used: Eq.symm
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
h : Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
h0 : f i = 0
⊢ Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) 0

Tactic:
prod_eq_zero hi h0

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
h : Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
h0 : f i = 0
⊢ Eq.{u_3 + 1} (α := WithTop M₀) ⊤ 0

Tactic:
calc
    ⊤ = ∏ j ∈ s, f j := Eq.symm h
    _ = 0 := prod_eq_zero hi h0

Premises used: Finset.prod_eq_zero, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
h : Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
contrapose! : ∀ (h : ∀ (i : ι) (_ : i ∈ s), f i ≠ ⊤), Ne.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
⊢ ∃ i ∈ s, f i = ⊤

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
h : ∀ (i : ι) (_ : i ∈ s), f i ≠ ⊤
⊢ Ne.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤

Tactic:
WithTop.prod_ne_top h

Premises used: WithTop.prod_ne_top
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
h : ∀ (i : ι) (_ : i ∈ s), f i ≠ ⊤
⊢ Ne.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤

Tactic:
exact WithTop.prod_ne_top h

Premises used: WithTop.prod_ne_top
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
mp : Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤ → (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0
mpr : ((∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0) → Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤
⊢ Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤ ↔ (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

Tactic:
constructor
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤ → (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

Tactic:
fun h ↦ ⟨prod_eq_top_ex_top h, fun _ ih ↦ prod_eq_top_ne_zero ih h⟩

Premises used: WithTop.prod_eq_top_ne_zero, And.intro, WithTop.prod_eq_top_ex_top
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤ → (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

Tactic:
exact fun h ↦ ⟨prod_eq_top_ex_top h, fun _ ih ↦ prod_eq_top_ne_zero ih h⟩
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ((∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0) → Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤

Tactic:
fun ⟨h, h'⟩ ↦ prod_eq_top (Exists.choose_spec h).1 (Exists.choose_spec h).2 h'

Premises used: Exists.choose_spec, _private.0.WithTop.prod_eq_top_iff.match_1, WithTop.prod_eq_top, Finset.prod, And.right, And.left, Top.top, Eq
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ((∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0) → Eq.{u_3 + 1} (α := WithTop M₀) (∏ j ∈ s, f j) ⊤

Tactic:
exact fun ⟨h, h'⟩ ↦ prod_eq_top (Exists.choose_spec h).1 (Exists.choose_spec h).2 h'
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → M
⊢ Eq.{u_2 + 1} (α := WithBot M) (↑(∑ i ∈ s, f i) : WithBot M) (∑ i ∈ s, (↑(f i) : WithBot M))

Tactic:
map_sum addHom f s

Premises used: WithBot.some, map_sum, WithTop.some, WithBot.addHom
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
empty : Eq.{u_2 + 1} (α := WithBot M) (∑ i ∈ ∅, f i) ⊥ ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = ⊥
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (Eq.{u_2 + 1} (α := WithBot M) (∑ i ∈ s, f i) ⊥ ↔ ∃ i ∈ s, f i = ⊥) →
      (Eq.{u_2 + 1} (α := WithBot M) (∑ i ∈ Finset.cons a s h, f i) ⊥ ↔ ∃ i ∈ Finset.cons a s h, f i = ⊥)
⊢ Eq.{u_2 + 1} (α := WithBot M) (∑ i ∈ s, f i) ⊥ ↔ ∃ i ∈ s, f i = ⊥

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ Eq.{u_2 + 1} (α := WithBot M) (∑ i ∈ ∅, f i) ⊥ ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ f i = ⊥

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
a : ι
s_1 : Finset ι
h : a ∉ s_1
h_1 : Eq.{u_2 + 1} (α := WithBot M) (∑ i ∈ s_1, f i) ⊥ ↔ ∃ i ∈ s_1, f i = ⊥
⊢ Eq.{u_2 + 1} (α := WithBot M) (∑ i ∈ cons a s_1 h, f i) ⊥ ↔ ∃ i ∈ cons a s_1 h, f i = ⊥

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
inst_1 : LT M
⊢ LT.lt.{u_2} (α := WithBot M) ⊥ (∑ i ∈ s, f i) ↔ ∀ i ∈ s, ⊥ < f i

Tactic:
simp only [WithBot.bot_lt_iff_ne_bot, ne_eq, sum_eq_bot_iff, not_exists, not_and]

Premises used: WithBot.sum_eq_bot_iff, not_exists, ne_eq, WithBot.bot_lt_iff_ne_bot, not_and
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
inst_1 : LT M
h : ∀ i ∈ s, f i ≠ ⊥
⊢ LT.lt.{u_2} (α := WithBot M) ⊥ (∑ i ∈ s, f i)

Tactic:
bot_lt_sum_iff.2 fun i hi ↦ WithBot.bot_lt_iff_ne_bot.2 (h i hi)

Premises used: Iff.mpr, WithBot.bot_lt_iff_ne_bot, WithBot.bot_lt_sum_iff
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithBot M₀
h : ∀ i ∈ s, f i ≠ ⊥
⊢ Ne.{u_3 + 1} (α := WithBot M₀) (∏ i ∈ s, f i) ⊥

Tactic:
prod_induction f (· ≠ ⊥) (fun _ _ ↦ mul_ne_bot) coe_ne_bot h

Premises used: Ne, Bot.bot, Finset.prod_induction, WithBot.mul_ne_bot, WithBot.coe_ne_bot
-- Module: Mathlib.Algebra.BigOperators.WithTop
Goal:
ι : Type u_1
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
inst_2 : Nontrivial M₀
inst_3 : DecidableEq M₀
s : Finset ι
f : ι → WithBot M₀
inst_4 : LT M₀
h : ∀ i ∈ s, ⊥ < f i
⊢ LT.lt.{u_3} (α := WithBot M₀) ⊥ (∏ i ∈ s, f i)

Tactic:
prod_induction f (⊥ < ·) (fun _ _ ↦ bot_lt_mul) (bot_lt_coe _) h

Premises used: WithBot.bot_lt_mul, Bot.bot, Finset.prod_induction, LT.lt, WithBot.bot_lt_coe
-- Module: Mathlib.Algebra.BrauerGroup.Defs
Goal:
K : Type u
inst : Field K
A : CSA.{u, u_1} K
⊢ IsBrauerEquivalent A A

Tactic:
⟨1, 1, one_ne_zero, one_ne_zero, ⟨AlgEquiv.refl⟩⟩

Premises used: Nonempty.intro, And.intro, Exists.intro, one_ne_zero, AlgEquiv.refl, OfNat.ofNat
-- Module: Mathlib.Algebra.BrauerGroup.Defs
Goal:
K : Type u
inst : Field K
A : CSA.{u, u_1} K
B : CSA.{u, u_2} K
h : IsBrauerEquivalent A B
⊢ IsBrauerEquivalent B A

Tactic:
let ⟨n, m, hn, hm, ⟨iso⟩⟩ := h
  ⟨m, n, hm, hn, ⟨iso.symm⟩⟩

Premises used: AlgEquiv.symm, Nonempty.intro, And.intro, Exists.intro, IsBrauerEquivalent, _private.0.IsBrauerEquivalent.symm.match_1