harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coeff_coe (i : ℤ) :
    ((f : R⟦X⟧) : R⸨X⸩).coeff i =
      if i < 0 then 0 else PowerSeries.coeff R i.natAbs f

Proof state:
case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff R (Int.negSucc a✝).natAbs) f

Tactic:
rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)]

Result:
case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ Int.negSucc a✝ ∉ ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } '' (HahnSeries.toPowerSeries.symm f).support

Proof state:
case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ Int.negSucc a✝ ∉ ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } '' (HahnSeries.toPowerSeries.symm f).support

Tactic:
simp only [not_exists, RelEmbedding.coe_mk, Set.mem_image, not_and, Function.Embedding.coeFn_mk,
  Ne, toPowerSeries_symm_apply_coeff, mem_support, imp_true_iff,
  not_false_iff, reduceCtorEq]

Result:
no goals

Proof state:
case ofNat
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.ofNat a✝) = if Int.ofNat a✝ < 0 then 0 else (coeff R (Int.ofNat a✝).natAbs) f

Tactic:
rw [Int.ofNat_eq_coe, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_lt,
  Int.natAbs_ofNat]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
i : ℤ
⊢ ((ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (coeff R i.natAbs) f

Tactic:
cases i

Result:
case ofNat
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.ofNat a✝) = if Int.ofNat a✝ < 0 then 0 else (coeff R (Int.ofNat a✝).natAbs) f

case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff R (Int.negSucc a✝).natAbs) f
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma natAbs_valMinAbs_add_le (a b : ZMod n) :
    (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Proof state:
case zero
a b : ZMod 0
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
rfl

Result:
no goals

Proof state:
case succ.hl
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ n.succ / 2

Tactic:
apply natAbs_valMinAbs_le

Result:
no goals

Proof state:
case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
apply natAbs_min_of_le_div_two n.succ

Result:
case succ.he
n : ℕ
a b : ZMod (n + 1)
⊢ ↑(a + b).valMinAbs = ↑(a.valMinAbs + b.valMinAbs)

case succ.hl
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ n.succ / 2

Proof state:
n : ℕ
a b : ZMod n
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
rcases n with - | n

Result:
case zero
a b : ZMod 0
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Proof state:
case succ.he
n : ℕ
a b : ZMod (n + 1)
⊢ ↑(a + b).valMinAbs = ↑(a.valMinAbs + b.valMinAbs)

Tactic:
simp_rw [Int.cast_add, coe_valMinAbs]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma RightHomologyData.exact_iff [S.HasHomology]
    (h : S.RightHomologyData) :
    S.Exact ↔ IsZero h.H

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ IsZero S.homology ↔ IsZero h.H

Tactic:
exact Iso.isZero_iff h.homologyIso

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact ↔ IsZero h.H

Tactic:
rw [S.exact_iff_isZero_homology]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ IsZero S.homology ↔ IsZero h.H
-- Mathlib/RingTheory/PolynomialAlgebra.lean
lemma evalRingHom_mapMatrix_comp_compRingEquiv {m} [Fintype m] [DecidableEq m] :
    (evalRingHom 0).mapMatrix.comp (compRingEquiv m n R[X]) =
      (compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
⊢ (evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X]) =
    (compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix

Tactic:
ext

Result:
case a.a
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x✝ : Matrix m m (Matrix n n R[X])
i✝ j✝ : m × n
⊢ ((evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X])) x✝ i✝ j✝ =
    ((compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix) x✝ i✝ j✝

Proof state:
case a.a
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x✝ : Matrix m m (Matrix n n R[X])
i✝ j✝ : m × n
⊢ ((evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X])) x✝ i✝ j✝ =
    ((compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix) x✝ i✝ j✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem _root_.tendsto_card_div_pow_atTop_volume (hs₁ : IsBounded s)
    (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) :
    Tendsto (fun n : ℕ ↦ (Nat.card ↑(s ∩ (n : ℝ)⁻¹ • L) : ℝ) / n ^ card ι)
      atTop (nhds (volume s).toReal)

Proof state:
case h.e'_5.h.e'_3
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ (volume s).toReal = ∫ (x : ι → ℝ) in s, 1

Tactic:
rw [setIntegral_const, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑n ^ card ι) atTop
    (nhds (volume s).toReal)

Tactic:
convert tendsto_tsum_div_pow_atTop_integral s (fun _ ↦ 1) continuous_const hs₁ hs₂ hs₃

Result:
case h.e'_3.h.h.e'_5
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
x✝ : ℕ
⊢ ↑(Nat.card ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) =
    ∑' (x : ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), 1

case h.e'_5.h.e'_3
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ (volume s).toReal = ∫ (x : ι → ℝ) in s, 1

Proof state:
case h.e'_3.h.h.e'_5
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
x✝ : ℕ
⊢ ↑(Nat.card ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) =
    ∑' (x : ↑(s ∩ (↑x✝)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), 1

Tactic:
rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
lemma of_dvd_two [IsDomain R] [NeZero (2 : R)] (hx : B x x ∣ 2) :
    IsReflective B x where
  regular := isRegular_of_ne_zero <| fun contra ↦ by simp [contra, two_ne_zero (α := R)] at hx
  dvd_two_mul y := hx.mul_right (B x y)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
inst✝¹ : IsDomain R
inst✝ : NeZero 2
hx : (B x) x ∣ 2
contra : (B x) x = 0
⊢ False

Tactic:
simp [contra, two_ne_zero (α := R)] at hx

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_multiset_prod (m : Multiset R[X]) : (0 : R[X]) ∉ m → m.prod.roots = m.bind roots

Proof state:
case mk
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : Multiset R[X]
L : List R[X]
⊢ 0 ∉ Quot.mk (⇑(List.isSetoid R[X])) L →
    (prod (Quot.mk (⇑(List.isSetoid R[X])) L)).roots = Multiset.bind (Quot.mk (⇑(List.isSetoid R[X])) L) roots

Tactic:
simpa only [Multiset.prod_coe, quot_mk_to_coe''] using roots_list_prod L

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : Multiset R[X]
⊢ 0 ∉ m → m.prod.roots = m.bind roots

Tactic:
rcases m with ⟨L⟩

Result:
case mk
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : Multiset R[X]
L : List R[X]
⊢ 0 ∉ Quot.mk (⇑(List.isSetoid R[X])) L →
    (prod (Quot.mk (⇑(List.isSetoid R[X])) L)).roots = Multiset.bind (Quot.mk (⇑(List.isSetoid R[X])) L) roots
-- Mathlib/Data/List/Sublists.lean
theorem sublistsAux_eq_array_foldl :
    sublistsAux = fun (a : α) (r : List (List α)) =>
      (r.toArray.foldl (init := #[])
        fun r l => (r.push l).push (a :: l)).toList

Proof state:
α : Type u
a : α
r : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α),
    (fun r l => r ++ [l, a :: l]) x.toList y = ((fun r l => (r.push l).push (a :: l)) x y).toList

Tactic:
simp

Result:
no goals

Proof state:
case h.h
α : Type u
a : α
r : List (List α)
⊢ sublistsAux a r = (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
simp only [sublistsAux, Array.foldl_toList, Array.mkEmpty]

Result:
case h.h
α : Type u
a : α
r : List (List α)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r = (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList

Proof state:
α : Type u
⊢ sublistsAux = fun a r => (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
funext a r

Result:
case h.h
α : Type u
a : α
r : List (List α)
⊢ sublistsAux a r = (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList

Proof state:
case h.h
α : Type u
a : α
r : List (List α)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r = (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
have := foldl_hom Array.toList (fun r l => (r.push l).push (a :: l))
  (fun (r : List (List α)) l => r ++ [l, a :: l]) r #[]
  (by simp)

Result:
case h.h
α : Type u
a : α
r : List (List α)
this : foldl (fun r l => r ++ [l, a :: l]) #[].toList r = (foldl (fun r l => (r.push l).push (a :: l)) #[] r).toList
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r = (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList

Proof state:
case h.h
α : Type u
a : α
r : List (List α)
this : foldl (fun r l => r ++ [l, a :: l]) #[].toList r = (foldl (fun r l => (r.push l).push (a :: l)) #[] r).toList
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r = (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
simpa using this

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_one_snd_of_isTwoCocycle {f : G × G → A} (hf : IsTwoCocycle f) (g : G) :
    f (g, 1) = g • f (1, 1)

Proof state:
G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsTwoCocycle f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
simpa only [mul_one, add_left_inj] using hf g 1 1

Result:
no goals
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem finset_image_add {F α β : Type*} [AddCommGroup α] [FunLike F α ℝ]
    [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean f)
    (g : β → α) (t : Finset β) :
    ∃ b : β, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
⊢ ∃ b, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Tactic:
let _ := AddGroupSeminormClass.toSeminormedAddCommGroup f

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
⊢ ∃ b, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Tactic:
simp only [← AddGroupSeminormClass.toSeminormedAddCommGroup_norm_eq]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (t.Nonempty → b ∈ t) ∧ ‖t.sum g‖ ≤ ‖g b‖

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
⊢ ∃ b, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Tactic:
have := AddGroupSeminormClass.isUltrametricDist hna

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (t.Nonempty → b ∈ t) ∧ ‖t.sum g‖ ≤ ‖g b‖

Tactic:
apply exists_norm_finset_sum_le

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem mul_inverse_cancel (x : M₀) (h : IsUnit x) : x * inverse x = 1

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x * inverse x = 1

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑u * inverse ↑u = 1

Proof state:
case intro
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑u * inverse ↑u = 1

Tactic:
rw [inverse_unit, Units.mul_inv]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_filter_of_ne {p : α → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) :
    ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x :=
  (prod_subset (filter_subset _ _)) fun x => by
    classical
      rw [not_imp_comm, mem_filter]
      exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : α
⊢ x ∈ s → x ∉ filter (fun x => p x) s → f x = 1

Tactic:
classical
  rw [not_imp_comm, mem_filter]
  exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : α
⊢ x ∈ s → ¬f x = 1 → x ∈ s ∧ p x

Tactic:
exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : α
h₁ : x ∈ s
h₂ : ¬f x = 1
⊢ p x

Tactic:
simpa using hp _ h₁ h₂

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : α
⊢ x ∈ s → x ∉ filter (fun x => p x) s → f x = 1

Tactic:
rw [not_imp_comm, mem_filter]

Result:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : α
⊢ x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem sum_pow (x : α → R) (n : ℕ) :
    s.sum x ^ n = ∑ k ∈ s.sym n, k.val.multinomial * (k.val.map x).prod

Proof state:
case h.e'_3.a.h.e'_6
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
x✝ : { x // x ∈ s.sym n }
a✝ : x✝ ∈ univ
⊢ (Multiset.map x ↑↑x✝).prod = (Multiset.map x ↑↑x✝).noncommProd ⋯

Tactic:
rw [Multiset.noncommProd_eq_prod]

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
⊢ s.sum x ^ n = ∑ i : { x // x ∈ s.sym n }, ↑(↑↑i).multinomial * (Multiset.map x ↑↑i).prod

Tactic:
convert sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n

Result:
case h.e'_3.a.h.e'_6
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
x✝ : { x // x ∈ s.sym n }
a✝ : x✝ ∈ univ
⊢ (Multiset.map x ↑↑x✝).prod = (Multiset.map x ↑↑x✝).noncommProd ⋯

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
⊢ s.sum x ^ n = ∑ k ∈ s.sym n, ↑(↑k).multinomial * (Multiset.map x ↑k).prod

Tactic:
conv_rhs => rw [← sum_coe_sort]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
⊢ s.sum x ^ n = ∑ i : { x // x ∈ s.sym n }, ↑(↑↑i).multinomial * (Multiset.map x ↑↑i).prod
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_modifyKey [BEq α] [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')]
    {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getValueCast! k' (modifyKey k f l) =
      if heq : k == k' then
        getValueCast? k l |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!
      else
        getValueCast! k' l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
hi : Inhabited (β k')
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getValueCast! k' (modifyKey k f l) =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (getValueCast? k l))).get! else getValueCast! k' l

Tactic:
simp only [modifyKey_eq_alterKey, getValueCast!_alterKey, hl]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_image_Iio (s : Set α) : IsPiSystem (Iio '' s)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iio a ∩ Iio b ∈ Iio '' s

Tactic:
exact ⟨a ⊓ b, inf_ind a b ha hb, Iio_inter_Iio.symm⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iio '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iio a ∩ Iio b ∈ Iio '' s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_cons (a : α) (l) : countP p (a :: l) = countP p l + if p a then 1 else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ countP p (a :: l) = countP p l + if p a = true then 1 else 0

Tactic:
by_cases h : p a <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem Multiset.untrop_sum [LinearOrder R] [OrderTop R] (s : Multiset (Tropical R)) :
    untrop s.sum = Multiset.inf (s.map untrop)

Proof state:
case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ untrop (sum 0) = (map untrop 0).inf

Tactic:
simp

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop x.sum = (map untrop x).inf
⊢ untrop (s ::ₘ x).sum = (map untrop (s ::ₘ x)).inf

Tactic:
simp only [sum_cons, untrop_add, untrop_le_iff, map_cons, inf_cons, ← IH]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset (Tropical R)
⊢ untrop s.sum = (map untrop s).inf

Tactic:
induction' s using Multiset.induction with s x IH

Result:
case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ untrop (sum 0) = (map untrop 0).inf

case cons
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop x.sum = (map untrop x).inf
⊢ untrop (s ::ₘ x).sum = (map untrop (s ::ₘ x)).inf
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem mem_adjoin_range_iff {ι : Type*} (i : ι → E) (x : E) :
    x ∈ adjoin F (Set.range i) ↔ ∃ r s : MvPolynomial ι F,
      x = MvPolynomial.aeval i r / MvPolynomial.aeval i s

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
i : ι → E
x : E
⊢ x ∈ adjoin F (Set.range i) ↔ ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

Tactic:
simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
  Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring,
  Algebra.adjoin_range_eq_range_aeval, AlgHom.mem_range, exists_exists_eq_and]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
i : ι → E
x : E
⊢ (∃ a a_1, (MvPolynomial.aeval i) a / (MvPolynomial.aeval i) a_1 = x) ↔
    ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
i : ι → E
x : E
⊢ (∃ a a_1, (MvPolynomial.aeval i) a / (MvPolynomial.aeval i) a_1 = x) ↔
    ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

Tactic:
tauto

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_neg (f_neg : ∀ x : R, f (-x) = f x) (x : R) :
    seminormFromBounded' f (-x) = seminormFromBounded' f x

Proof state:
case e_s.h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x y : R
⊢ f (-x * y) / f y = f (x * y) / f y

Tactic:
rw [neg_mul, f_neg]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ ⨆ y, f (-x * y) / f y = ⨆ y, f (x * y) / f y

Tactic:
congr

Result:
case e_s
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ (fun y => f (-x * y) / f y) = fun y => f (x * y) / f y

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ seminormFromBounded' f (-x) = seminormFromBounded' f x

Tactic:
suffices ⨆ y, f (-x * y) / f y = ⨆ y, f (x * y) / f y by simpa only [seminormFromBounded']

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ ⨆ y, f (-x * y) / f y = ⨆ y, f (x * y) / f y

Proof state:
case e_s
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ (fun y => f (-x * y) / f y) = fun y => f (x * y) / f y

Tactic:
ext y

Result:
case e_s.h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x y : R
⊢ f (-x * y) / f y = f (x * y) / f y

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
this : ⨆ y, f (-x * y) / f y = ⨆ y, f (x * y) / f y
⊢ seminormFromBounded' f (-x) = seminormFromBounded' f x

Tactic:
simpa only [seminormFromBounded']

Result:
no goals