harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_lt_length {p : α → Bool} {xs : List α} :
    xs.findIdx p < xs.length ↔ ∃ x ∈ xs, p x

Proof state:
α : Type u_1
p : α → Bool
xs : List α
this : findIdx p xs = xs.length ↔ xs.length ≤ findIdx p xs
⊢ (∀ (x : α), x ∈ xs → p x = false) ↔ ∀ (x : α), ¬(x ∈ xs ∧ p x = true)

Tactic:
simp only [Bool.not_eq_true, not_and]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p xs < xs.length ↔ ∃ x, x ∈ xs ∧ p x = true

Tactic:
rw [← Decidable.not_iff_not, Nat.not_lt]

Result:
α : Type u_1
p : α → Bool
xs : List α
⊢ xs.length ≤ findIdx p xs ↔ ¬∃ x, x ∈ xs ∧ p x = true

Proof state:
α : Type u_1
p : α → Bool
xs : List α
this : findIdx p xs = xs.length ↔ findIdx p xs ≤ xs.length ∧ xs.length ≤ findIdx p xs
⊢ xs.length ≤ findIdx p xs ↔ ¬∃ x, x ∈ xs ∧ p x = true

Tactic:
simp only [findIdx_le_length, true_and] at this

Result:
α : Type u_1
p : α → Bool
xs : List α
this : findIdx p xs = xs.length ↔ xs.length ≤ findIdx p xs
⊢ xs.length ≤ findIdx p xs ↔ ¬∃ x, x ∈ xs ∧ p x = true

Proof state:
α : Type u_1
p : α → Bool
xs : List α
this : findIdx p xs = xs.length ↔ xs.length ≤ findIdx p xs
⊢ xs.length ≤ findIdx p xs ↔ ¬∃ x, x ∈ xs ∧ p x = true

Tactic:
rw [← this, findIdx_eq_length, not_exists]

Result:
α : Type u_1
p : α → Bool
xs : List α
this : findIdx p xs = xs.length ↔ xs.length ≤ findIdx p xs
⊢ (∀ (x : α), x ∈ xs → p x = false) ↔ ∀ (x : α), ¬(x ∈ xs ∧ p x = true)

Proof state:
α : Type u_1
p : α → Bool
xs : List α
⊢ xs.length ≤ findIdx p xs ↔ ¬∃ x, x ∈ xs ∧ p x = true

Tactic:
have := @Nat.le_antisymm_iff (xs.findIdx p) xs.length

Result:
α : Type u_1
p : α → Bool
xs : List α
this : findIdx p xs = xs.length ↔ findIdx p xs ≤ xs.length ∧ xs.length ≤ findIdx p xs
⊢ xs.length ≤ findIdx p xs ↔ ¬∃ x, x ∈ xs ∧ p x = true
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_eq_getValueCast! [BEq α] [LawfulBEq α] [Inhabited β] {l : List ((_ : α) × β)}
    {a : α} : getValue! a l = getValueCast! a l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
a : α
⊢ getValue! a l = getValueCast! a l

Tactic:
simp only [getValue!_eq_getValue?, getValueCast!_eq_getValueCast?, getValue?_eq_getValueCast?]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem fst_eq (κ : Kernel α (β × γ)) : fst κ = map κ Prod.fst

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.fst = κ.map Prod.fst

Tactic:
simp [fst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_add {x y z : BitVec w} :
    x * (y + z) = x * y + x * z

Proof state:
case a
w : Nat
x y z : BitVec w
⊢ (x * (y + z)).toNat = (x * y + x * z).toNat

Tactic:
simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]

Result:
case a
w : Nat
x y z : BitVec w
⊢ x.toNat * ((y.toNat + z.toNat) % 2 ^ w) % 2 ^ w = (x.toNat * y.toNat + x.toNat * z.toNat) % 2 ^ w

Proof state:
w : Nat
x y z : BitVec w
⊢ x * (y + z) = x * y + x * z

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x y z : BitVec w
⊢ (x * (y + z)).toNat = (x * y + x * z).toNat

Proof state:
case a
w : Nat
x y z : BitVec w
⊢ x.toNat * ((y.toNat + z.toNat) % 2 ^ w) % 2 ^ w = (x.toNat * y.toNat + x.toNat * z.toNat) % 2 ^ w

Tactic:
rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
  ← Nat.mul_mod, Nat.mul_add]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/BaseChange.lean
@[simp] lemma restrictScalars_pairing (i j : ι) :
    algebraMap K L ((P.restrictScalars' K hP).pairing i j) = P.pairing i j

Proof state:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Field L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module L M
inst✝⁷ : Module L N
P : RootPairing ι L M N
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : Algebra K L
inst✝⁴ : Module K M
inst✝³ : Module K N
inst✝² : IsScalarTower K L M
inst✝¹ : IsScalarTower K L N
inst✝ : P.IsBalanced
hP : ∀ (i j : ι), P.pairing i j ∈ (algebraMap K L).range
i j : ι
⊢ (algebraMap K L) ((P.restrictScalars' K hP).pairing i j) = P.pairing i j

Tactic:
simp only [pairing, restrictScalars_toPerfectPairing_apply_apply, restrictScalars_coe_root,
  restrictScalars_coe_coroot]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovEDist_le_max_measure_univ (μ ν : Measure Ω) :
    levyProkhorovEDist μ ν ≤ max (μ univ) (ν univ)

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν ≤ μ univ ⊔ ν univ

Tactic:
refine sInf_le fun B _ ↦ ⟨?_, ?_⟩ <;> apply le_add_left <;> simp [measure_mono]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem decay (f : 𝓢(E, F)) (k n : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
C : ℝ
hC : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ 0 < C ⊔ 1

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ ∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

Tactic:
rcases f.decay' k n with ⟨C, hC⟩

Result:
case intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
C : ℝ
hC : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

Proof state:
case intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
C : ℝ
hC : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

Tactic:
exact ⟨max C 1, by positivity, fun x => (hC x).trans (le_max_left _ _)⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_empty : #[].Pairwise R

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
⊢ Pairwise R #[]

Tactic:
unfold Pairwise

Result:
α✝ : Type u_1
R : α✝ → α✝ → Prop
⊢ List.Pairwise R #[].toList

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
⊢ List.Pairwise R #[].toList

Tactic:
exact List.Pairwise.nil

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem FiniteMeasure.limsup_measure_closed_le_of_tendsto {Ω ι : Type*} {L : Filter ι}
    [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω]
    [OpensMeasurableSpace Ω] {μ : FiniteMeasure Ω}
    {μs : ι → FiniteMeasure Ω} (μs_lim : Tendsto μs L (𝓝 μ)) {F : Set Ω} (F_closed : IsClosed F) :
    (L.limsup fun i ↦ (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F

Proof state:
case inr.h
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε

Tactic:
let fs := F_closed.apprSeq

Result:
case inr.h
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
⊢ limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε

Proof state:
case inr.h.intro
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ⊤
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ ↑μ F + ↑ε / 2 + ↑ε / 2 ≤ ↑μ F + ↑ε

Tactic:
simp only [add_assoc, ENNReal.add_halves, le_refl]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.stieltjesFunctionAux_nonneg (a : α) (r : ℝ) :
    0 ≤ IsMeasurableRatCDF.stieltjesFunctionAux f a r

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
⊢ Nonempty { r' // r < ↑r' }

Tactic:
obtain ⟨r, hrx⟩ := exists_rat_gt r

Result:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r✝ : ℝ
r : ℚ
hrx : r✝ < ↑r
⊢ Nonempty { r' // r✝ < ↑r' }

Proof state:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r✝ : ℝ
r : ℚ
hrx : r✝ < ↑r
⊢ Nonempty { r' // r✝ < ↑r' }

Tactic:
exact ⟨⟨r, hrx⟩⟩

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ ⨅ q, f a ↑q

Tactic:
exact le_ciInf fun r' ↦ hf.nonneg a _

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
⊢ 0 ≤ stieltjesFunctionAux f a r

Tactic:
have : Nonempty { r' : ℚ // r < ↑r' } := by
  obtain ⟨r, hrx⟩ := exists_rat_gt r
  exact ⟨⟨r, hrx⟩⟩

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ stieltjesFunctionAux f a r

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ stieltjesFunctionAux f a r

Tactic:
rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ ⨅ q, f a ↑q
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableOn_Ioi_cpow_of_lt {a : ℂ} (ha : a.re < -1) {c : ℝ} (hc : 0 < c) :
    IntegrableOn (fun t : ℝ => (t : ℂ) ^ a) (Ioi c)

Proof state:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t => ↑t ^ a) (Ioi c) volume

Tactic:
refine (integrable_norm_iff ?_).mp <| integrableOn_Ioi_norm_cpow_of_lt ha hc

Result:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (fun t => ↑t ^ a) (volume.restrict (Ioi c))

Proof state:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (fun t => ↑t ^ a) (volume.restrict (Ioi c))

Tactic:
refine ContinuousOn.aestronglyMeasurable (fun t ht ↦ ?_) measurableSet_Ioi

Result:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (fun t => ↑t ^ a) (Ioi c) t

Proof state:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (fun t => ↑t ^ a) (Ioi c) t

Tactic:
exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem basis_repr (h : IsAdjoinRootMonic S f) (x : S) (i : Fin (natDegree f)) :
    h.basis.repr x i = (h.modByMonicHom x).coeff (i : ℕ)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
i : Fin f.natDegree
⊢ (Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp ⋯) i = (h.modByMonicHom x).coeff ↑i

Tactic:
rw [Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
i : Fin f.natDegree
⊢ (h.basis.repr x) i = (h.modByMonicHom x).coeff ↑i

Tactic:
change (h.modByMonicHom x).toFinsupp.comapDomain _ Fin.val_injective.injOn i = _

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
i : Fin f.natDegree
⊢ (Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp ⋯) i = (h.modByMonicHom x).coeff ↑i
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleType_cycleRange {n : ℕ} [NeZero n] {i : Fin n} (h0 : i ≠ 0) :
    cycleType (cycleRange i) = {(i + 1 : ℕ)}

Proof state:
case mk.succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.cycleType = {↑⟨n✝ + 1, hi⟩ + 1}

Tactic:
rw [cycleRange, cycleType_extendDomain]

Result:
case mk.succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ (finRotate (↑⟨n✝ + 1, hi⟩ + 1)).cycleType = {↑⟨n✝ + 1, hi⟩ + 1}

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin n
h0 : i ≠ 0
⊢ i.cycleRange.cycleType = {↑i + 1}

Tactic:
obtain ⟨i, hi⟩ := i

Result:
case mk
n : ℕ
inst✝ : NeZero n
i : ℕ
hi : i < n
h0 : ⟨i, hi⟩ ≠ 0
⊢ ⟨i, hi⟩.cycleRange.cycleType = {↑⟨i, hi⟩ + 1}

Proof state:
case mk.succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ (finRotate (↑⟨n✝ + 1, hi⟩ + 1)).cycleType = {↑⟨n✝ + 1, hi⟩ + 1}

Tactic:
exact cycleType_finRotate

Result:
no goals

Proof state:
case mk
n : ℕ
inst✝ : NeZero n
i : ℕ
hi : i < n
h0 : ⟨i, hi⟩ ≠ 0
⊢ ⟨i, hi⟩.cycleRange.cycleType = {↑⟨i, hi⟩ + 1}

Tactic:
cases i

Result:
case mk.zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.cycleType = {↑⟨0, hi⟩ + 1}

case mk.succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.cycleType = {↑⟨n✝ + 1, hi⟩ + 1}

Proof state:
case mk.zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.cycleType = {↑⟨0, hi⟩ + 1}

Tactic:
exact (h0 rfl).elim

Result:
no goals
-- Mathlib/Algebra/Order/Group/Indicator.lean
@[to_additive]
lemma mulSupport_iSup [ConditionallyCompleteLattice M] [Nonempty ι] (f : ι → α → M) :
    mulSupport (fun x ↦ ⨆ i, f i x) ⊆ ⋃ i, mulSupport (f i)

Proof state:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ (mulSupport fun x => ⨆ i, f i x) ⊆ ⋃ i, mulSupport (f i)

Tactic:
simp only [mulSupport_subset_iff', mem_iUnion, not_exists, nmem_mulSupport]

Result:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → ⨆ i, f i x = 1

Proof state:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → ⨆ i, f i x = 1

Tactic:
intro x hx

Result:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ ⨆ i, f i x = 1

Proof state:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
x : α
hx : ∀ (x_1 : ι), f x_1 x = 1
⊢ ⨆ i, f i x = 1

Tactic:
simp only [hx, ciSup_const]

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma reverse_comp_reverse :
    reverse ∘ reverse = (id : ContextFreeRule T N → ContextFreeRule T N)

Proof state:
T : Type u_1
N : Type u_2
⊢ reverse ∘ reverse = id

Tactic:
ext : 1

Result:
case h
T : Type u_1
N : Type u_2
x✝ : ContextFreeRule T N
⊢ (reverse ∘ reverse) x✝ = id x✝

Proof state:
case h
T : Type u_1
N : Type u_2
x✝ : ContextFreeRule T N
⊢ (reverse ∘ reverse) x✝ = id x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_eq [IsEmpty X] : #(FreeAlgebra R X) = #R

Proof state:
R : Type u
inst✝¹ : CommSemiring R
X : Type u
inst✝ : IsEmpty X
⊢ #(FreeAlgebra R X) = #R

Tactic:
simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iSup (f : ι → LowerSet α) : (↑(⨆ i, f i) : Set α) = ⋃ i, f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → LowerSet α
⊢ ↑(⨆ i, f i) = ⋃ i, ↑(f i)

Tactic:
simp_rw [iSup, coe_sSup, mem_range, iUnion_exists, iUnion_iUnion_eq']

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem toPointedCone_injective : Function.Injective ((↑) : ProperCone 𝕜 E → PointedCone 𝕜 E) :=
  fun S T h => by cases S; cases T; congr

Proof state:
case mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
T : ProperCone 𝕜 E
toSubmodule✝ : Submodule { c // 0 ≤ c } E
isClosed'✝ : IsClosed toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ } = ↑T
⊢ { toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ } = T

Tactic:
cases T

Result:
case mk.mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
toSubmodule✝¹ : Submodule { c // 0 ≤ c } E
isClosed'✝¹ : IsClosed toSubmodule✝¹.carrier
toSubmodule✝ : Submodule { c // 0 ≤ c } E
isClosed'✝ : IsClosed toSubmodule✝.carrier
h :
  ↑{ toSubmodule := toSubmodule✝¹, isClosed' := isClosed'✝¹ } =
    ↑{ toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ }
⊢ { toSubmodule := toSubmodule✝¹, isClosed' := isClosed'✝¹ } = { toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ }

Proof state:
case mk.mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
toSubmodule✝¹ : Submodule { c // 0 ≤ c } E
isClosed'✝¹ : IsClosed toSubmodule✝¹.carrier
toSubmodule✝ : Submodule { c // 0 ≤ c } E
isClosed'✝ : IsClosed toSubmodule✝.carrier
h :
  ↑{ toSubmodule := toSubmodule✝¹, isClosed' := isClosed'✝¹ } =
    ↑{ toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ }
⊢ { toSubmodule := toSubmodule✝¹, isClosed' := isClosed'✝¹ } = { toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ }

Tactic:
congr

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
S T : ProperCone 𝕜 E
h : ↑S = ↑T
⊢ S = T

Tactic:
cases S

Result:
case mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
T : ProperCone 𝕜 E
toSubmodule✝ : Submodule { c // 0 ≤ c } E
isClosed'✝ : IsClosed toSubmodule✝.carrier
h : ↑{ toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ } = ↑T
⊢ { toSubmodule := toSubmodule✝, isClosed' := isClosed'✝ } = T
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_sphere [Nontrivial E] (x : E) (r : ℝ) : μ (sphere x r) = 0

Proof state:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
⊢ μ (sphere x 0) = 0

Tactic:
rw [sphere_zero, measure_singleton]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ μ (sphere x r) = 0

Tactic:
rcases eq_or_ne r 0 with (rfl | h)

Result:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
⊢ μ (sphere x 0) = 0

case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : r ≠ 0
⊢ μ (sphere x r) = 0

Proof state:
case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : r ≠ 0
⊢ μ (sphere x r) = 0

Tactic:
exact addHaar_sphere_of_ne_zero μ x h

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Seminorm.lean
theorem smul_sup (r : R) (p q : GroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q :=
  have Real.smul_max : ∀ x y : ℝ, r • max x y = max (r • x) (r • y) := fun x y => by
    simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg
  ext fun _ => Real.smul_max _ _

Proof state:
R : Type u_1
E : Type u_3
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : GroupSeminorm E
x y : ℝ
⊢ r • (x ⊔ y) = r • x ⊔ r • y

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
  mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k a : α} (hl : DistinctKeys l) (hka : a == k) : containsKey a (eraseKey k l) = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
hka : (a == k) = true
⊢ containsKey a (eraseKey k l) = false

Tactic:
rw [containsKey_congr hka, containsKey_eraseKey_self hl]

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem tsum_mul_right (f : α → ℝ≥0) (a : ℝ≥0) : ∑' x, f x * a = (∑' x, f x) * a :=
  NNReal.eq <| by simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]

Proof state:
α : Type u_1
f : α → ℝ≥0
a : ℝ≥0
⊢ ↑(∑' (x : α), f x * a) = ↑((∑' (x : α), f x) * a)

Tactic:
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]

Result:
no goals