harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/PeakFunction.lean
theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn
    [MetrizableSpace α] [IsLocallyFiniteMeasure μ] [IsOpenPosMeasure μ] (hs : IsCompact s)
    {c : α → ℝ} (hc : ContinuousOn c s) (h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀)
    (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ closure (interior s))
    (hmg : IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) :
    Tendsto (fun n : ℕ => (∫ x in s, c x ^ n ∂μ)⁻¹ • ∫ x in s, c x ^ n • g x ∂μ) atTop
      (𝓝 (g x₀))

Proof state:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
⊢ Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
apply
  tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos hs _ hc
    h'c hnc hnc₀ this hmg hcg

Result:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
⊢ ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)

Proof state:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
u : Set α
u_open : IsOpen u
x₀_u : x₀ ∈ u
⊢ 0 < μ (u ∩ s)

Tactic:
calc
  0 < μ (u ∩ interior s) :=
    (u_open.inter isOpen_interior).measure_pos μ (_root_.mem_closure_iff.1 h₀ u u_open x₀_u)
  _ ≤ μ (u ∩ s) := by gcongr; apply interior_subset

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem toEquiv_injective : Injective (toEquiv : α ≃ᵐ β → α ≃ β)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e₁ : α ≃ β
measurable_toFun✝¹ : Measurable ⇑e₁
measurable_invFun✝¹ : Measurable ⇑e₁.symm
measurable_toFun✝ : Measurable ⇑e₁
measurable_invFun✝ : Measurable ⇑e₁.symm
⊢ { toEquiv := e₁, measurable_toFun := measurable_toFun✝¹, measurable_invFun := measurable_invFun✝¹ } =
    { toEquiv := e₁, measurable_toFun := measurable_toFun✝, measurable_invFun := measurable_invFun✝ }

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Injective toEquiv

Tactic:
rintro ⟨e₁, _, _⟩ ⟨e₂, _, _⟩ (rfl : e₁ = e₂)

Result:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e₁ : α ≃ β
measurable_toFun✝¹ : Measurable ⇑e₁
measurable_invFun✝¹ : Measurable ⇑e₁.symm
measurable_toFun✝ : Measurable ⇑e₁
measurable_invFun✝ : Measurable ⇑e₁.symm
⊢ { toEquiv := e₁, measurable_toFun := measurable_toFun✝¹, measurable_invFun := measurable_invFun✝¹ } =
    { toEquiv := e₁, measurable_toFun := measurable_toFun✝, measurable_invFun := measurable_invFun✝ }
-- Mathlib/Data/ENNReal/Basic.lean
theorem le_of_top_imp_top_of_toNNReal_le {a b : ℝ≥0∞} (h : a = ⊤ → b = ⊤)
    (h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal) : a ≤ b

Proof state:
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal
hlt : b < a
⊢ False

Tactic:
lift b to ℝ≥0 using hlt.ne_top

Result:
case intro
a : ℝ≥0∞
b : ℝ≥0
h : a = ⊤ → ↑b = ⊤
h_nnreal : a ≠ ⊤ → ↑b ≠ ⊤ → a.toNNReal ≤ (↑b).toNNReal
hlt : ↑b < a
⊢ False

Proof state:
case intro
a : ℝ≥0∞
b : ℝ≥0
h : a = ⊤ → ↑b = ⊤
h_nnreal : a ≠ ⊤ → ↑b ≠ ⊤ → a.toNNReal ≤ (↑b).toNNReal
hlt : ↑b < a
⊢ False

Tactic:
lift a to ℝ≥0 using mt h coe_ne_top

Result:
case intro.intro
b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ False

Proof state:
case intro.intro
b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ False

Tactic:
refine hlt.not_le ?_

Result:
case intro.intro
b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b

Proof state:
case intro.intro
b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b

Tactic:
simpa using h_nnreal

Result:
no goals

Proof state:
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal
⊢ a ≤ b

Tactic:
by_contra! hlt

Result:
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal
hlt : b < a
⊢ False
-- Mathlib/Data/Nat/Pairing.lean
theorem pair_lt_pair_left {a₁ a₂} (b) (h : a₁ < a₂) : pair a₁ b < pair a₂ b

Proof state:
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b

Tactic:
apply Nat.add_lt_add_right

Result:
case neg.h₂.h
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂

Proof state:
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
by_cases h₂ : a₂ < b <;> simp [pair, h₂, h]

Result:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Proof state:
case neg.h₂.h
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂

Tactic:
assumption

Result:
no goals

Proof state:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)

Tactic:
apply add_lt_add

Result:
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b

Proof state:
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

Tactic:
exact Nat.mul_self_lt_mul_self h

Result:
no goals

Proof state:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]

Result:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)

Proof state:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Tactic:
apply Nat.add_lt_add_of_le_of_lt

Result:
case neg.hle
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b ≤ a₂ * a₂

case neg.hlt
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b

Proof state:
a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b

Tactic:
by_cases h₁ : a₁ < b <;> simp [pair, h₁, Nat.add_assoc]

Result:
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Proof state:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Tactic:
simp? at h₂ says simp only [not_lt] at h₂

Result:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Proof state:
case neg.hlt
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b

Tactic:
exact Nat.lt_add_right _ h

Result:
no goals

Proof state:
case neg.hle
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b ≤ a₂ * a₂

Tactic:
exact Nat.mul_self_le_mul_self h₂

Result:
no goals

Proof state:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Tactic:
simp only [not_lt] at h₂

Result:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Proof state:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp at h₁

Result:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
-- Mathlib/Data/Finset/NAry.lean
theorem image_image₂ (f : α → β → γ) (g : γ → δ) :
    (image₂ f s t).image g = image₂ (fun a b => g (f a b)) s t :=
  coe_injective <| by
    push_cast
    exact image_image2 _ _

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ g '' image2 f ↑s ↑t = image2 (fun a b => g (f a b)) ↑s ↑t

Tactic:
exact image_image2 _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ (fun a b => g (f a b)) s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ g '' image2 f ↑s ↑t = image2 (fun a b => g (f a b)) ↑s ↑t
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_add_bot_coe (a : ℝ) :
    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊥, a)

Proof state:
a : ℝ
⊢ ContinuousAt (fun p => p.1 + p.2) (⊥, ↑a)

Tactic:
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]

Result:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ↑a), a.1 + a.2 < ↑x

Proof state:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ↑a), a.1 + a.2 < ↑x

Tactic:
refine fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
  (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_

Result:
a r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑(r - (a + 1)) ∧ x✝.2 < ↑(a + 1)
⊢ x✝.1 + x✝.2 < ↑r

Proof state:
a r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑(r - (a + 1)) ∧ x✝.2 < ↑(a + 1)
⊢ x✝.1 + x✝.2 < ↑r

Tactic:
simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasSum_iff_tendsto_nat {f : ℕ → ℝ≥0∞} (r : ℝ≥0∞) :
    HasSum f r ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Proof state:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
⊢ HasSum f r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
refine ⟨HasSum.tendsto_sum_nat, fun h => ?_⟩

Result:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f r

Proof state:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n => ∑ i ∈ Finset.range n, f i

Tactic:
exact fun s t hst => Finset.sum_le_sum_of_subset (Finset.range_subset.2 hst)

Result:
no goals

Proof state:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

Tactic:
exact ENNReal.summable.hasSum

Result:
no goals

Proof state:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f r

Tactic:
rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]

Result:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n => ∑ i ∈ Finset.range n, f i
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem SimpleFunc.lintegral_eq_lintegral {m : MeasurableSpace α} (f : α →ₛ ℝ≥0∞) (μ : Measure α) :
    ∫⁻ a, f a ∂μ = f.lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ ∫⁻ (a : α), f a ∂μ = f.lintegral μ

Tactic:
rw [MeasureTheory.lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ = f.lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ = f.lintegral μ

Tactic:
exact le_antisymm (iSup₂_le fun g hg => lintegral_mono hg <| le_rfl)
  (le_iSup₂_of_le f le_rfl le_rfl)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ioo {a b : α} (ha : 0 ≤ a) :
    (Nat.cast : ℕ → α) ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
simp [floor_lt, lt_ceil, ha]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
ha : 0 ≤ a
⊢ Nat.cast ⁻¹' Ioo a b = Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋₊ ⌈b⌉₊
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isGE_of_eq_gt {o : Ordering} : o = .gt → o.isGE

Proof state:
⊢ gt.isGE = true

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordering
⊢ o = gt → o.isGE = true

Tactic:
rintro rfl

Result:
⊢ gt.isGE = true
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_smul_of_tower {α} [Monoid α] [DistribMulAction α R] [IsScalarTower α R R]
    [SMulCommClass α R R] (c : α) (A : Matrix n n R) :
    det (c • A) = c ^ Fintype.card n • det A

Proof state:
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
R : Type v
inst✝⁴ : CommRing R
α : Type u_3
inst✝³ : Monoid α
inst✝² : DistribMulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ (c • A).det = c ^ Fintype.card n • A.det

Tactic:
rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem dart_card_eq_sum_degrees : Fintype.card G.Dart = ∑ v, G.degree v

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : DecidableEq V
⊢ Fintype.card G.Dart = ∑ v : V, G.degree v

Tactic:
simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : DecidableEq V
⊢ #univ = ∑ x : V, #(filter (fun d => d.toProd.1 = x) univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : DecidableEq V
⊢ ∀ x ∈ univ, x.toProd.1 ∈ univ

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : DecidableEq V
⊢ #univ = ∑ x : V, #(filter (fun d => d.toProd.1 = x) univ)

Tactic:
exact card_eq_sum_card_fiberwise (by simp)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Fintype.card G.Dart = ∑ v : V, G.degree v

Tactic:
haveI := Classical.decEq V

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : DecidableEq V
⊢ Fintype.card G.Dart = ∑ v : V, G.degree v
-- Mathlib/Order/Interval/Multiset.lean
theorem Ioc_eq_zero_iff : Ioc a b = 0 ↔ ¬a < b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc a b = 0 ↔ ¬a < b

Tactic:
rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma iInf_iSup_eq' (f : ∀ a, κ a → α) :
    let _ := minAx.toCompleteLattice
    ⨅ i, ⨆ j, f i j = ⨆ g : ∀ i, κ i, ⨅ i, f i (g i)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ let x := minAx.toCompleteLattice;
  ⨅ i, ⨆ j, f i j = ⨆ g, ⨅ i, f i (g i)

Tactic:
let _ := minAx.toCompleteLattice

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ let x := minAx.toCompleteLattice;
  ⨅ i, ⨆ j, f i j = ⨆ g, ⨅ i, f i (g i)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ let x := minAx.toCompleteLattice;
  ⨅ i, ⨆ j, f i j = ⨆ g, ⨅ i, f i (g i)

Tactic:
refine le_antisymm ?_ le_iInf_iSup

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ ⨅ i, ⨆ j, f i j ≤ ⨆ g, ⨅ i, f i (g i)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : (a : ↑(range fun x => range (f x))) → ↑↑a
⊢ ⨅ a, ↑(g a) ≤ ⨅ i, f i ((fun a => Classical.choose ⋯) i)

Tactic:
refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : (a : ↑(range fun x => range (f x))) → ↑↑a
a : ι
⊢ ↑(g ⟨range (f a), ⋯⟩) ≤ f a ((fun a => Classical.choose ⋯) a)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
⊢ ⨅ i, ⨆ j, f i j = ⨅ a, ⨆ b, ↑b

Tactic:
simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]

Result:
no goals

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : (a : ↑(range fun x => range (f x))) → ↑↑a
⊢ ⨅ a, ↑(g a) ≤ ⨆ g, ⨅ i, f i (g i)

Tactic:
refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2

Result:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : (a : ↑(range fun x => range (f x))) → ↑↑a
⊢ ⨅ a, ↑(g a) ≤ ⨅ i, f i ((fun a => Classical.choose ⋯) i)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x✝ : CompleteLattice α := minAx.toCompleteLattice
g : (a : ↑(range fun x => range (f x))) → ↑↑a
a : ι
⊢ ↑(g ⟨range (f a), ⋯⟩) ≤ f a ((fun a => Classical.choose ⋯) a)

Tactic:
rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_of_isEmpty [IsEmpty α] (f : α → M) : ∏ᶠ i, f i = 1

Proof state:
M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (x : ?m.12125), 1

M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.12122

Tactic:
congr

Result:
case e_f
M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ (fun i => f i) = fun x => 1

Proof state:
M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
rw [← finprod_one]

Result:
M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (x : ?m.12125), 1

M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.12122

Proof state:
case e_f
M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ (fun i => f i) = fun x => 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_le_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c)

Proof state:
a c b d : Nat
h : b ≥ d
⊢ (a + b ≤ c + d) = (a + (b - d) ≤ c)

Tactic:
rw [← Nat.add_sub_assoc h, Nat.sub_le_iff_le_add]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
/-- When its possible to compare the two, the composition of two `IsStronglyCartesian.map` will also
be given by a `IsStronglyCartesian.map`. In other words, given diagrams
```
a''         a'        a --φ--> b
|           |         |        |
v           v         v        v
R'' --g'--> R' --g--> R --f--> S
```
and
```
a' --φ'--> b
|          |
v          v
R' --f'--> S
```
and
```
a'' --φ''--> b
|            |
v            v
R'' --f''--> S
```
such that `φ` and `φ'` are strongly cartesian morphisms, and such that `f' = g ≫ f` and
`f'' = g' ≫ f'`. Then composing the induced map from `a'' ⟶ a'` with the induced map from
`a' ⟶ a` gives the induced map from `a'' ⟶ a`. -/
@[reassoc (attr := simp)]
lemma map_comp_map {R' R'' : 𝒮} {a' a'' : 𝒳} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R}
    {g' : R'' ⟶ R'} (H : f' = g ≫ f) (H' : f'' = g' ≫ f') (φ' : a' ⟶ b) (φ'' : a'' ⟶ b)
    [IsStronglyCartesian p f' φ'] [IsHomLift p f'' φ''] :
    map p f' φ' H' φ'' ≫ map p f φ H φ' =
      map p f φ (show f'' = (g' ≫ g) ≫ f by rwa [assoc, ← H]) φ''

Proof state:
case hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ (map p f' φ' H' φ'' ≫ map p f φ H φ') ≫ φ = φ''

Tactic:
simp only [assoc, fac]

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ map p f' φ' H' φ'' ≫ map p f φ H φ' = map p f φ ⋯ φ''

Tactic:
apply map_uniq p f φ

Result:
case hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ (map p f' φ' H' φ'' ≫ map p f φ H φ') ≫ φ = φ''

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ f'' = (g' ≫ g) ≫ f

Tactic:
rwa [assoc, ← H]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finRotate_last' : finRotate (n + 1) ⟨n, by omega⟩ = ⟨0, Nat.zero_lt_succ _⟩

Proof state:
n : ℕ
⊢ Fin.cast ⋯ (finAddFlip ⟨n, ⋯⟩) = 0

Tactic:
rw [finAddFlip_apply_mk_right le_rfl]

Result:
n : ℕ
⊢ Fin.cast ⋯ ⟨n - n, ⋯⟩ = 0

Proof state:
n : ℕ
⊢ Fin.cast ⋯ ⟨n - n, ⋯⟩ = 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ (finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩

Tactic:
dsimp [finRotate_succ]

Result:
n : ℕ
⊢ Fin.cast ⋯ (finAddFlip ⟨n, ⋯⟩) = 0

Proof state:
m n : ℕ
⊢ n < n + 1

Tactic:
omega

Result:
no goals