harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.stronglyMeasurable_bot_iff [Nonempty β] [T2Space β] :
    StronglyMeasurable[⊥] f ↔ ∃ c, f = fun _ => c

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x => cs n
⊢ f = fun x => f hα.some

Tactic:
conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x => cs n
⊢ f = fun x => f hα.some

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x => cs n
h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
⊢ f = fun x => f hα.some

Tactic:
ext1 x

Result:
case inr.refine_1.h
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x => cs n
h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
x : α
⊢ f x = f hα.some
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_smul_le (s : Set M) (r : R) : span R (r • s) ≤ span R s

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ r • s ⊆ ↑(span R s)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
x : M
hx : x ∈ s
⊢ (fun x => r • x) x ∈ ↑(span R s)

Proof state:
case intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
x : M
hx : x ∈ s
⊢ (fun x => r • x) x ∈ ↑(span R s)

Tactic:
exact smul_mem (span R s) r (subset_span hx)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ span R (r • s) ≤ span R s

Tactic:
rw [span_le]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ r • s ⊆ ↑(span R s)
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
theorem multiset_sum_right (a : α) (h : ∀ b ∈ s, Commute a b) : Commute a s.sum

Proof state:
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
h : ∀ b ∈ s, Commute a b
⊢ Commute a s.sum

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ b ∈ ⟦a✝⟧, Commute a b
⊢ Commute a (sum ⟦a✝⟧)

Proof state:
case h
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ b ∈ ⟦a✝⟧, Commute a b
⊢ Commute a a✝.sum

Tactic:
exact Commute.list_sum_right _ _ h

Result:
no goals

Proof state:
case h
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ b ∈ ⟦a✝⟧, Commute a b
⊢ Commute a (sum ⟦a✝⟧)

Tactic:
rw [quot_mk_to_coe, sum_coe]

Result:
case h
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ b ∈ ⟦a✝⟧, Commute a b
⊢ Commute a a✝.sum
-- Mathlib/Analysis/Seminorm.lean
theorem preimage_metric_closedBall {r : ℝ} : p ⁻¹' Metric.closedBall 0 r = { x | p x ≤ r }

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ⇑p ⁻¹' Metric.closedBall 0 r ↔ x ∈ {x | p x ≤ r}

Tactic:
simp only [mem_setOf, mem_preimage, mem_closedBall_zero_iff,
  Real.norm_of_nonneg (apply_nonneg p _)]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ ⇑p ⁻¹' Metric.closedBall 0 r = {x | p x ≤ r}

Tactic:
ext x

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ⇑p ⁻¹' Metric.closedBall 0 r ↔ x ∈ {x | p x ≤ r}
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
/-- The **Ahlswede-Zhang Identity**. -/
lemma infSum_compls_add_supSum (𝒜 : Finset (Finset α)) :
    infSum 𝒜ᶜˢ + supSum 𝒜 = card α * ∑ k ∈ range (card α), (k : ℚ)⁻¹ + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ ∑ s : Finset α, ↑(#(𝒜ᶜˢ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
rw [← @map_univ_of_surjective (Finset α) _ _ _ ⟨compl, compl_injective⟩ compl_surjective, sum_map]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ ∑ x : Finset α,
        ↑(#(𝒜ᶜˢ.truncatedInf ({ toFun := compl, inj' := ⋯ } x))) /
          (↑(#({ toFun := compl, inj' := ⋯ } x)) * ↑((card α).choose #({ toFun := compl, inj' := ⋯ } x))) +
      ∑ s ∈ map { toFun := compl, inj' := ⋯ } univ,
        ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ infSum 𝒜ᶜˢ + supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
unfold infSum supSum

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ ∑ s : Finset α, ↑(#(𝒜ᶜˢ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s : Finset α, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ ∑ x : Finset α,
        ↑(#(𝒜ᶜˢ.truncatedInf ({ toFun := compl, inj' := ⋯ } x))) /
          (↑(#({ toFun := compl, inj' := ⋯ } x)) * ↑((card α).choose #({ toFun := compl, inj' := ⋯ } x))) +
      ∑ s ∈ map { toFun := compl, inj' := ⋯ } univ,
        ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
simp only [Function.Embedding.coeFn_mk, univ_map_embedding, ← compl_truncatedSup,
  ← sum_add_distrib, card_compl, cast_sub (card_le_univ _), choose_symm (card_le_univ _),
  div_add_div_same, sub_add_cancel, Fintype.sum_div_mul_card_choose_card]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_map (f : α → β) (l : List α) : getLast? (map f l) = (getLast? l).map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ (map f l).getLast? = Option.map f l.getLast?

Tactic:
cases l

Result:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map f []).getLast? = Option.map f [].getLast?

case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
⊢ (map f (head✝ :: tail✝)).getLast? = Option.map f (head✝ :: tail✝).getLast?

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map f []).getLast? = Option.map f [].getLast?

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
⊢ (map f (head✝ :: tail✝)).getLast? = Option.map f (head✝ :: tail✝).getLast?

Tactic:
rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_map] <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_filterMap {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
    Perm (toListModel (m.filterMap f).1.buckets)
      ((toListModel m.1.buckets).filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩))

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
⊢ toListModel (filterMap f m).val.buckets ~
    List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (toListModel m.val.buckets)

Tactic:
rw [filterMap_eq_filterMapₘ]

Result:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
⊢ toListModel (m.filterMapₘ f).val.buckets ~
    List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
⊢ toListModel (m.filterMapₘ f).val.buckets ~
    List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (toListModel m.val.buckets)

Tactic:
exact toListModel_filterMapₘ

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
theorem card_GL_field :
    Nat.card (GL (Fin n) 𝔽) = ∏ i : (Fin n), (q ^ n - q ^ ( i : ℕ ))

Proof state:
case inl
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
⊢ Nat.card (GL (Fin 0) 𝔽) = ∏ i : Fin 0, (q ^ 0 - q ^ ↑i)

Tactic:
simp [Nat.card_eq_fintype_card]

Result:
no goals

Proof state:
case inr
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
hn : n > 0
⊢ n ≤ Module.finrank 𝔽 (Fin n → 𝔽)

Tactic:
simp only [Module.finrank_fintype_fun_eq_card, Fintype.card_fin, le_refl]

Result:
no goals

Proof state:
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
⊢ Nat.card (GL (Fin n) 𝔽) = ∏ i : Fin n, (q ^ n - q ^ ↑i)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | hn

Result:
case inl
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
⊢ Nat.card (GL (Fin 0) 𝔽) = ∏ i : Fin 0, (q ^ 0 - q ^ ↑i)

case inr
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
hn : n > 0
⊢ Nat.card (GL (Fin n) 𝔽) = ∏ i : Fin n, (q ^ n - q ^ ↑i)

Proof state:
case inr
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
hn : n > 0
⊢ Nat.card (GL (Fin n) 𝔽) = ∏ i : Fin n, (q ^ n - q ^ ↑i)

Tactic:
rw [Nat.card_congr (equiv_GL_linearindependent n hn), card_linearIndependent,
Module.finrank_fintype_fun_eq_card, Fintype.card_fin]

Result:
case inr
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
hn : n > 0
⊢ n ≤ Module.finrank 𝔽 (Fin n → 𝔽)
-- Mathlib/Order/Filter/Tendsto.lean
theorem le_map_of_right_inverse {mab : α → β} {mba : β → α} {f : Filter α} {g : Filter β}
    (h₁ : mab ∘ mba =ᶠ[g] id) (h₂ : Tendsto mba g f) : g ≤ map mab f

Proof state:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map mab (map mba g) ≤ map mab f

Tactic:
exact map_mono h₂

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ g ≤ map mab f

Tactic:
rw [← @map_id _ g, ← map_congr h₁, ← map_map]

Result:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map mab (map mba g) ≤ map mab f
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem Measurable.ennreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) :
    Measurable fun x => ∑' i, f i x

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ⨆ s, ∑ i ∈ s, f i x

Tactic:
exact .iSup fun s ↦ s.measurable_sum fun i _ => h i

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ∑' (i : ι), f i x

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]

Result:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable fun x => ⨆ s, ∑ i ∈ s, f i x
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Ioo_iff_Iio (h : a < b) :
    ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsLT h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_preΨ₄ : (W.map f).preΨ₄ = W.preΨ₄.map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).preΨ₄ = Polynomial.map f W.preΨ₄

Tactic:
simp only [preΨ₄, map_b₂, map_b₄, map_b₆, map_b₈]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ 2 * X ^ 6 + C (f W.b₂) * X ^ 5 + 5 * C (f W.b₄) * X ^ 4 + 10 * C (f W.b₆) * X ^ 3 + 10 * C (f W.b₈) * X ^ 2 +
        C (f W.b₂ * f W.b₈ - f W.b₄ * f W.b₆) * X +
      C (f W.b₄ * f W.b₈ - f W.b₆ ^ 2) =
    Polynomial.map f
      (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
          C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
        C (W.b₄ * W.b₈ - W.b₆ ^ 2))

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ 2 * X ^ 6 + C (f W.b₂) * X ^ 5 + 5 * C (f W.b₄) * X ^ 4 + 10 * C (f W.b₆) * X ^ 3 + 10 * C (f W.b₈) * X ^ 2 +
        C (f W.b₂ * f W.b₈ - f W.b₄ * f W.b₆) * X +
      C (f W.b₄ * f W.b₈ - f W.b₆ ^ 2) =
    Polynomial.map f
      (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
          C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
        C (W.b₄ * W.b₈ - W.b₆ ^ 2))

Tactic:
map_simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem single_le_finprod {M : Type*} [OrderedCommMonoid M] (i : α) {f : α → M}
    (hf : (mulSupport f).Finite) (h : ∀ j, 1 ≤ f j) : f i ≤ ∏ᶠ j, f j

Proof state:
α : Type u_1
M : Type u_7
inst✝ : OrderedCommMonoid M
i : α
f : α → M
hf : (mulSupport f).Finite
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j

Tactic:
calc
f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
_ = ∏ᶠ j, f j :=
(finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

Result:
no goals

Proof state:
α : Type u_1
M : Type u_7
inst✝ : OrderedCommMonoid M
i : α
f : α → M
hf : (mulSupport f).Finite
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j

Tactic:
classical calc
    f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
      Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
    _ = ∏ᶠ j, f j :=
      (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

Result:
no goals
-- Mathlib/Control/Applicative.lean
theorem seq_pure (f : Comp F G (α → β)) (x : α) : f <*> pure x = (fun g : α → β => g x) <$> f :=
  Comp.ext <| by simp [comp_def, functor_norm]

Proof state:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : Comp F G (α → β)
x : α
⊢ (f <*> pure x).run = ((fun g => g x) <$> f).run

Tactic:
simp [comp_def, functor_norm]

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_div_mul_div (A B C : Finset G) :
    #(A / C) * #B ≤ #(A * B) * #(B / C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A * B) * #(B / C)

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(B * C⁻¹)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(B * C⁻¹)

Tactic:
exact ruzsa_triangle_inequality_mul_mul_mul _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem mul_continuousOn [LocallyCompactSpace X] [T2Space X] [NormedRing R]
    [SecondCountableTopologyEither X R] {f g : X → R} {s : Set X} (hf : LocallyIntegrableOn f s μ)
    (hg : ContinuousOn g s) (hs : IsLocallyClosed s) :
    LocallyIntegrableOn (fun x => f x * g x) s μ

Proof state:
X : Type u_1
R : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => f x * g x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).mul_continuousOn (hg.mono hk_sub) hk_c

Result:
no goals

Proof state:
X : Type u_1
R : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn (fun x => f x * g x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Result:
X : Type u_1
R : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => f x * g x) k μ
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[ext]
lemma ext ⦃f g : IncidenceAlgebra 𝕜 α⦄ (h : ∀ a b, a ≤ b → f a b = g a b) : f = g

Proof state:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b

Tactic:
rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le hab]

Result:
no goals

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
⊢ f a b = g a b

Tactic:
by_cases hab : a ≤ b

Result:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : a ≤ b
⊢ f a b = g a b

case neg
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
⊢ f = g

Tactic:
refine DFunLike.coe_injective' (funext₂ fun a b ↦ ?_)

Result:
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
⊢ f a b = g a b

Proof state:
case pos
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : a ≤ b
⊢ f a b = g a b

Tactic:
exact h _ _ hab

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem bijOn_ptsOfPeriod (f : α → α) {n : ℕ} (hn : 0 < n) :
    BijOn f (ptsOfPeriod f n) (ptsOfPeriod f n) :=
  ⟨(Commute.refl f).mapsTo_ptsOfPeriod n, fun _ hx _ hy hxy => hx.eq_of_apply_eq_same hy hn hxy,
    fun x hx =>
    ⟨f^[n.pred] x, hx.apply_iterate _, by
      rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]⟩⟩

Proof state:
α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f (f^[n.pred] x) = x

Tactic:
rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]

Result:
no goals
-- Mathlib/Order/Filter/SmallSets.lean
theorem Tendsto.smallSets_mono {s t : α → Set β} (ht : Tendsto t la lb.smallSets)
    (hst : ∀ᶠ x in la, s x ⊆ t x) : Tendsto s la lb.smallSets

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la lb.smallSets
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la lb.smallSets

Tactic:
rw [tendsto_smallSets_iff] at ht ⊢

Result:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t

Tactic:
exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem eq_iff_atom_le_iff {a b : α} : a = b ↔ ∀ c, IsAtom c → (c ≤ a ↔ c ≤ b)

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a = b

Tactic:
exact le_antisymm (le_iff_atom_le_imp.2 fun a ha hx => (h a ha).1 hx)
  (le_iff_atom_le_imp.2 fun a ha hy => (h a ha).2 hy)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
⊢ a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

Tactic:
refine ⟨fun h => h ▸ by simp, fun h => ?_⟩

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a = b

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
a b : α
h : a = b
⊢ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_replicate_of_lt {n : Nat} {m : Nat} (h : m < n) : (replicate n a)[m]? = some a

Proof state:
α✝ : Type u_1
a : α✝
n m : Nat
h : m < n
⊢ (replicate n a)[m]? = some a

Tactic:
simp [getElem?_replicate, h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_map_complex (f : V ≃ₗᵢ[ℝ] ℂ)
    (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : V) :
    o.oangle x y = Complex.arg (conj (f x) * f y)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle (f.symm (f x)) (f.symm (f y))

Tactic:
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg

Tactic:
rw [← Complex.oangle, ← hf, o.oangle_map]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle (f.symm (f x)) (f.symm (f y))

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : V
⊢ o.oangle x y = o.oangle x (f.symm (f y))

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Result:
no goals