harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem self_mem_ae_restrict {s} (hs : MeasurableSet s) : s ∈ ae (μ.restrict s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ s ∈ ae (μ.restrict s)

Tactic:
simp only [ae_restrict_eq hs, exists_prop, mem_principal, mem_inf_iff]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∃ t₁ ∈ ae μ, ∃ t₂, s ⊆ t₂ ∧ s = t₁ ∩ t₂

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ∃ t₁ ∈ ae μ, ∃ t₂, s ⊆ t₂ ∧ s = t₁ ∩ t₂

Tactic:
exact ⟨_, univ_mem, s, Subset.rfl, (univ_inter s).symm⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem succ_sub {m n : Nat} (h : n ≤ m) : succ m - n = succ (m - n)

Proof state:
m n : Nat
h : n ≤ m
⊢ m.succ - n = (m - n).succ

Tactic:
let ⟨k, hk⟩ := Nat.le.dest h

Result:
m n : Nat
h : n ≤ m
k : Nat
hk : n + k = m
⊢ m.succ - n = (m - n).succ

Proof state:
m n : Nat
h : n ≤ m
k : Nat
hk : n + k = m
⊢ m.succ - n = (m - n).succ

Tactic:
rw [← hk, Nat.add_sub_cancel_left, ← add_succ, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem map_inv_hom_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) :
    (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : C
e : X ≅ Y
F : C ⥤ D ⥤ E
Z : D
⊢ (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 ((F.obj Y).obj Z)

Tactic:
simp [← NatTrans.comp_app, ← Functor.map_comp]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_le_of_mem_dist {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r)
    (H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) : hausdorffDist s t ≤ r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ hausdorffDist s t ≤ r

Tactic:
apply hausdorffDist_le_of_infDist hr

Result:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ ∀ x ∈ s, infDist x t ≤ r

case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ ∀ x ∈ t, infDist x s ≤ r

Proof state:
case H1.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : dist x y ≤ r
⊢ infDist x t ≤ r

Tactic:
exact le_trans (infDist_le_dist_of_mem yt) hy

Result:
no goals

Proof state:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
⊢ infDist x t ≤ r

Tactic:
rcases H1 x xs with ⟨y, yt, hy⟩

Result:
case H1.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : dist x y ≤ r
⊢ infDist x t ≤ r

Proof state:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ ∀ x ∈ s, infDist x t ≤ r

Tactic:
intro x xs

Result:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xs : x ∈ s
⊢ infDist x t ≤ r

Proof state:
case H2.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : dist x y ≤ r
⊢ infDist x s ≤ r

Tactic:
exact le_trans (infDist_le_dist_of_mem ys) hy

Result:
no goals

Proof state:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
⊢ infDist x s ≤ r

Tactic:
rcases H2 x xt with ⟨y, ys, hy⟩

Result:
case H2.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : dist x y ≤ r
⊢ infDist x s ≤ r

Proof state:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
⊢ ∀ x ∈ t, infDist x s ≤ r

Tactic:
intro x xt

Result:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
r : ℝ
hr : 0 ≤ r
H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r
x : α
xt : x ∈ t
⊢ infDist x s ≤ r
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem threeAPFree_image_sphere :
    ThreeAPFree ((sphere n d k).image (map (2 * d - 1)) : Set ℕ)

Proof state:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
⊢ (a + b) i < 2 * d - 1

Tactic:
have hbi := mem_box.1 (sphere_subset_box hb) i

Result:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1

Proof state:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1

Tactic:
rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]

Result:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ ((a + b) i + 1).succ ≤ d + d

Proof state:
n d k : ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}

Tactic:
rw [Set.add_subset_iff]

Result:
n d k : ℕ
⊢ ∀ x ∈ ↑(sphere n d k), ∀ y ∈ ↑(sphere n d k), x + y ∈ {x | ∀ (i : Fin n), x i < 2 * d - 1}

Proof state:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ ((a + b) i + 1).succ ≤ d + d

Tactic:
exact (add_add_add_comm _ _ 1 1).trans_le (_root_.add_le_add hai hbi)

Result:
no goals

Proof state:
n d k : ℕ
⊢ ∀ x ∈ ↑(sphere n d k), ∀ y ∈ ↑(sphere n d k), x + y ∈ {x | ∀ (i : Fin n), x i < 2 * d - 1}

Tactic:
rintro a ha b hb i

Result:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
⊢ (a + b) i < 2 * d - 1

Proof state:
n d k : ℕ
⊢ ThreeAPFree ↑(image (⇑(map (2 * d - 1))) (sphere n d k))

Tactic:
rw [coe_image]

Result:
n d k : ℕ
⊢ ThreeAPFree (⇑(map (2 * d - 1)) '' ↑(sphere n d k))

Proof state:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
⊢ (a + b) i < 2 * d - 1

Tactic:
have hai := mem_box.1 (sphere_subset_box ha) i

Result:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
⊢ (a + b) i < 2 * d - 1

Proof state:
n d k : ℕ
⊢ ThreeAPFree (⇑(map (2 * d - 1)) '' ↑(sphere n d k))

Tactic:
apply ThreeAPFree.image' (α := Fin n → ℕ) (β := ℕ) (s := sphere n d k) (map (2 * d - 1))
  (map_injOn.mono _) threeAPFree_sphere

Result:
n d k : ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma antitone_rpow_of_base_le_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b ≤ 1) :
    Antitone (b ^ · : ℝ → ℝ)

Proof state:
case inr
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x => 1 ^ x

Tactic:
case inr => intro _ _ _; simp

Result:
no goals

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁✝ : b ≤ 1
hb₁ : b < 1
⊢ Antitone fun x => b ^ x

Tactic:
exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone

Result:
no goals

Proof state:
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x => 1 ^ x

Tactic:
intro _ _ _

Result:
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x => 1 ^ x) b✝ ≤ (fun x => 1 ^ x) a✝¹

Proof state:
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x => 1 ^ x) b✝ ≤ (fun x => 1 ^ x) a✝¹

Tactic:
simp

Result:
no goals

Proof state:
b : ℝ
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ Antitone fun x => b ^ x

Tactic:
rcases lt_or_eq_of_le hb₁ with hb₁ | rfl

Result:
case inl
b : ℝ
hb₀ : 0 < b
hb₁✝ : b ≤ 1
hb₁ : b < 1
⊢ Antitone fun x => b ^ x

case inr
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x => 1 ^ x

Proof state:
case inl
b : ℝ
hb₀ : 0 < b
hb₁✝ : b ≤ 1
hb₁ : b < 1
⊢ Antitone fun x => b ^ x

case inr
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x => 1 ^ x

Tactic:
case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone

Result:
case inr
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
⊢ Antitone fun x => 1 ^ x
-- Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
/-- Shortcut version for the commonly arising special case when `p i = π * q i` for some other
sequence `q`. -/
lemma hasSum_mellin_pi_mul {a : ι → ℂ} {q : ι → ℝ} {F : ℝ → ℂ} {s : ℂ}
    (hq : ∀ i, a i = 0 ∨ 0 < q i) (hs : 0 < s.re)
    (hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * rexp (-π * q i * t)) (F t))
    (h_sum : Summable fun i ↦ ‖a i‖ / (q i) ^ s.re) :
    HasSum (fun i ↦ π ^ (-s) * Gamma s * a i / q i ^ s) (mellin F s)

Proof state:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
i : ι
⊢ a i = 0 ∨ 0 < π * q i

Tactic:
rcases hq i with h | h <;> simp [h, pi_pos]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-(π * q i) * t))) (?m.32128 t)

Tactic:
simpa using hF

Result:
no goals

Proof state:
case h.e'_5.h
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
this : a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s
⊢ ↑π ^ (-s) * Complex.Gamma s * (a i / ↑(q i) ^ s) = Complex.Gamma s * (↑π ^ (-s) * a i / ↑(q i) ^ s)

Tactic:
ring_nf

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
/--
The dual basis of a powerbasis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`,
with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.
-/
lemma traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (pb : PowerBasis K L) (i) :
    (Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) pb.basis i =
      (minpolyDiv K pb.gen).coeff i / aeval pb.gen (derivative <| minpoly K pb.gen)

Proof state:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ ∀ x ∈ Finset.univ,
    x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
      x ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)) * pb.gen ^ ↑j)

Tactic:
intro σ _

Result:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
σ : L →ₐ[K] AlgebraicClosure K
a✝ : σ ∈ Finset.univ
⊢ σ pb.gen ^ ↑j / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ ((minpolyDiv K pb.gen).coeff ↑i) =
    σ ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)) * pb.gen ^ ↑j)
-- Mathlib/Topology/Inseparable.lean
theorem tendsto_lift₂_nhds {f : X → Y → α} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
    {x : X} {y : Y} {l : Filter α} :
    Tendsto (uncurry <| lift₂ f hf) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Proof state:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
rw [← map_prod_map_mk_nhds, tendsto_map'_iff]

Result:
X : Type u_1
Y : Type u_2
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
-- Mathlib/Data/Fintype/BigOperators.lean
lemma card_filter_piFinset_eq [∀ i, DecidableEq (α i)] (s : ∀ i, Finset (α i)) (i : ι) (a : α i) :
    #{f ∈ piFinset s | f i = a} = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0

Proof state:
case pos
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
⊢ #(filter (fun f => f i = a) (piFinset s)) = ∏ b ∈ univ.erase i, #(s b)

Tactic:
rw [card_filter_piFinset_eq_of_mem _ _ h]

Result:
no goals

Proof state:
case neg
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∉ s i
⊢ #(filter (fun f => f i = a) (piFinset s)) = 0

Tactic:
rw [filter_piFinset_of_not_mem _ _ _ h, Finset.card_empty]

Result:
no goals

Proof state:
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
⊢ #(filter (fun f => f i = a) (piFinset s)) = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
⊢ #(filter (fun f => f i = a) (piFinset s)) = ∏ b ∈ univ.erase i, #(s b)

case neg
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∉ s i
⊢ #(filter (fun f => f i = a) (piFinset s)) = 0
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_coe (l : List α) (comm) : noncommProd (l : Multiset α) comm = l.prod

Proof state:
α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ (↑l).noncommProd comm = l.prod

Tactic:
rw [noncommProd]

Result:
α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ noncommFold (fun x1 x2 => x1 * x2) (↑l) comm 1 = l.prod

Proof state:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 => x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
y : α
hy : y ∈ {x | x ∈ ↑tl}
⊢ x ≠ y → Commute x y

Tactic:
exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)

Result:
no goals

Proof state:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 => x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ {x | x ∈ ↑tl}.Pairwise Commute

Tactic:
intro x hx y hy

Result:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 => x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
y : α
hy : y ∈ {x | x ∈ ↑tl}
⊢ x ≠ y → Commute x y

Proof state:
α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ List.foldr (fun x1 x2 => x1 * x2) 1 l = l.prod

Tactic:
induction' l with hd tl hl

Result:
case nil
α : Type u_3
inst✝ : Monoid α
comm : {x | x ∈ ↑[]}.Pairwise Commute
⊢ List.foldr (fun x1 x2 => x1 * x2) 1 [] = [].prod

case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 => x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ List.foldr (fun x1 x2 => x1 * x2) 1 (hd :: tl) = (hd :: tl).prod

Proof state:
α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ noncommFold (fun x1 x2 => x1 * x2) (↑l) comm 1 = l.prod

Tactic:
simp only [noncommFold_coe]

Result:
α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ List.foldr (fun x1 x2 => x1 * x2) 1 l = l.prod

Proof state:
case nil
α : Type u_3
inst✝ : Monoid α
comm : {x | x ∈ ↑[]}.Pairwise Commute
⊢ List.foldr (fun x1 x2 => x1 * x2) 1 [] = [].prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 => x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ List.foldr (fun x1 x2 => x1 * x2) 1 (hd :: tl) = (hd :: tl).prod

Tactic:
rw [List.prod_cons, List.foldr, hl]

Result:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 => x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
⊢ {x | x ∈ ↑tl}.Pairwise Commute
-- Mathlib/Order/LiminfLimsup.lean
theorem isBoundedUnder_le_finset_sup [LinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) :
    f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup s (fun i ↦ F i a))

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i => F i a) ≤ s.sup m

Tactic:
exact hm.mono fun _ h ↦ sup_mono_fun h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup fun i => F i a

Tactic:
choose! m hm using h

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup fun i => F i a

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i => F i a) ≤ s.sup m

Tactic:
rw [← eventually_all_finset s] at hm

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i => F i a) ≤ s.sup m

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup fun i => F i a

Tactic:
use sup s m

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ ∀ᶠ (x : β) in Filter.map (fun a => s.sup fun i => F i a) f, (fun x1 x2 => x1 ≤ x2) x (s.sup m)

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ ∀ᶠ (x : β) in Filter.map (fun a => s.sup fun i => F i a) f, (fun x1 x2 => x1 ≤ x2) x (s.sup m)

Tactic:
simp only [eventually_map] at hm ⊢

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup fun i => F i a) ≤ s.sup m
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem iterate_frobenius_coeff (x : 𝕎 R) (i k : ℕ) :
    (frobenius^[i] x).coeff k = x.coeff k ^ p ^ i

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ (x.coeff k ^ p ^ i) ^ p = x.coeff k ^ (p ^ i * p)

Tactic:
ring_nf

Result:
no goals

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ ((⇑frobenius)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)

Tactic:
rw [iterate_succ_apply', coeff_frobenius_charP, ih, Nat.pow_succ]

Result:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ (x.coeff k ^ p ^ i) ^ p = x.coeff k ^ (p ^ i * p)

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i k : ℕ
⊢ ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i

Tactic:
induction' i with i ih

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k : ℕ
⊢ ((⇑frobenius)^[0] x).coeff k = x.coeff k ^ p ^ 0

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ ((⇑frobenius)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k : ℕ
⊢ ((⇑frobenius)^[0] x).coeff k = x.coeff k ^ p ^ 0

Tactic:
simp

Result:
no goals