harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
theorem smul_finprod' {ι : Sort*} [Finite ι] {f : ι → β} (r : α) :
    r • ∏ᶠ x : ι, f x = ∏ᶠ x : ι, r • (f x)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : MulDistribMulAction α β
ι : Sort u_4
inst✝ : Finite ι
f : ι → β
r : α
val✝ : Fintype (PLift ι)
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x

Tactic:
simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp),
  finprod_eq_prod_of_fintype, Finset.smul_prod']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : MulDistribMulAction α β
ι : Sort u_4
inst✝ : Finite ι
f : ι → β
r : α
val✝ : Fintype (PLift ι)
⊢ Function.mulSupport (?m.13844 ∘ PLift.down) ⊆ ↑Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : MulDistribMulAction α β
ι : Sort u_4
inst✝ : Finite ι
f : ι → β
r : α
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x

Tactic:
cases nonempty_fintype (PLift ι)

Result:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : MulDistribMulAction α β
ι : Sort u_4
inst✝ : Finite ι
f : ι → β
r : α
val✝ : Fintype (PLift ι)
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem support_formPerm [Fintype α] (s : Cycle α) (h : Nodup s) (hn : Nontrivial s) :
    support (formPerm s h) = s.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
⊢ (s.formPerm h).support = s.toFinset

Tactic:
induction' s using Quot.inductionOn with s

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) s) h).support = toFinset (Quot.mk (⇑(IsRotated.setoid α)) s)

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : α
h : Nodup (Quot.mk ⇑(IsRotated.setoid α) [x✝])
hn : Nontrivial (Quot.mk ⇑(IsRotated.setoid α) [x✝])
⊢ False

Tactic:
simpa [Nat.succ_le_succ_iff] using length_nontrivial hn

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) s) h).support = toFinset (Quot.mk (⇑(IsRotated.setoid α)) s)

Tactic:
refine support_formPerm_of_nodup s h ?_

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ ∀ (x : α), s ≠ [x]

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) s)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ ∀ (x : α), s ≠ [x]

Tactic:
rintro _ rfl

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : α
h : Nodup (Quot.mk ⇑(IsRotated.setoid α) [x✝])
hn : Nontrivial (Quot.mk ⇑(IsRotated.setoid α) [x✝])
⊢ False
-- Mathlib/Probability/StrongLaw.lean
theorem sum_variance_truncation_le {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) (K : ℕ) :
    ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * 𝔼[truncation X j ^ 2] ≤ 2 * 𝔼[X]

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
⊢ x / (↑k + 1) ≤ 1

Tactic:
convert (div_le_one _).2 hx.2

Result:
case h.e'_3.h.e'_6
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
⊢ ↑k + 1 = ↑(k + 1)

Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n => truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
⊢ 0 < ↑(k + 1)
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem trim_eq_self : v.trim le_rfl = v

Proof state:
α : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
⊢ v.trim ⋯ = v

Tactic:
ext i hi

Result:
case h
α : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(v.trim ⋯) i = ↑v i

Proof state:
case h
α : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(v.trim ⋯) i = ↑v i

Tactic:
exact if_pos hi

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_le_inv_iff : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]

Result:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a⁻¹ * b ≤ a * b⁻¹ * b ↔ b ≤ a

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a * a⁻¹ * b ≤ a * b⁻¹ * b ↔ b ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem sub_one_covBy [NoMinOrder α] (x : α) : x - 1 ⋖ x

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
x : α
⊢ pred x ⋖ x

Tactic:
exact pred_covBy x

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
x : α
⊢ x - 1 ⋖ x

Tactic:
rw [← pred_eq_sub_one]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
x : α
⊢ pred x ⋖ x
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem sum_measure [Countable ι] {μ : ι → Measure α} (h : ∀ i, AEMeasurable f (μ i)) :
    AEMeasurable f (sum μ)

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋃ i, (s i)ᶜ).restrict f)

Tactic:
intro t ht

Result:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet ((⋃ i, (s i)ᶜ).restrict f ⁻¹' t)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : Real.Angle.tan (∡ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_pow_le (p : R[X]) : ∀ n : ℕ, degree (p ^ n) ≤ n • degree p
  | 0 => by rw [pow_zero, zero_nsmul]; exact degree_one_le
  | n + 1 =>
    calc
      degree (p ^ (n + 1)) ≤ degree (p ^ n) + degree p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n * p).degree ≤ (p ^ n).degree + p.degree

Tactic:
exact degree_mul_le _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).degree + p.degree ≤ (n + 1) • p.degree

Tactic:
rw [succ_nsmul]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).degree + p.degree ≤ n • p.degree + p.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).degree + p.degree ≤ n • p.degree + p.degree

Tactic:
exact add_le_add_right (degree_pow_le _ _) _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p ^ 0).degree ≤ 0 • p.degree

Tactic:
rw [pow_zero, zero_nsmul]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ degree 1 ≤ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ degree 1 ≤ 0

Tactic:
exact degree_one_le

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ (n + 1)).degree ≤ (p ^ n).degree + p.degree

Tactic:
rw [pow_succ]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n * p).degree ≤ (p ^ n).degree + p.degree
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (units : CNF.Clause (PosFin n)) :
    AssignmentsInvariant (insertRatUnits f units).1

Proof state:
case right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  InsertUnitInvariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j1 j2 : Fin (f.insertRatUnits units).fst.ratUnits.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[j1] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[j2] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
left✝¹ : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j1 → k ≠ j2 → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
j1_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j1]
j1_unit_def : j1_unit = unit (f.insertRatUnits units).fst.ratUnits[j1]
j1_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.toList ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRatUnits units).fst.ratUnits[j2]
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSet.indep_generateFrom_of_disjoint {s : ι → Set Ω}
    (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s κ μ) (S T : Set ι) (hST : Disjoint S T) :
    Indep (generateFrom { t | ∃ n ∈ S, s n = t }) (generateFrom { t | ∃ k ∈ T, s k = t }) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
⊢ Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) κ μ

Tactic:
rcases eq_or_ne μ 0 with rfl | hμ

Result:
case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
S T : Set ι
hST : Disjoint S T
hs : iIndepSet s κ 0
⊢ Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) κ 0

case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
⊢ Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) κ μ

Proof state:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
⊢ Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) κ μ

Tactic:
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
  exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ

Result:
case inr.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μ] ⇑η
hη : IsMarkovKernel η
⊢ Indep (generateFrom {t | ∃ n ∈ S, s n = t}) (generateFrom {t | ∃ k ∈ T, s k = t}) κ μ
-- Mathlib/Order/LiminfLimsup.lean
theorem eventually_lt_of_lt_liminf {f : Filter α} [ConditionallyCompleteLinearOrder β] {u : α → β}
    {b : β} (h : b < liminf u f)
    (hu : f.IsBoundedUnder (· ≥ ·) u

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
⊢ ∀ᶠ (a : α) in f, b < u a

Tactic:
obtain ⟨c, hc, hbc⟩ : ∃ (c : β) (_ : c ∈ { c : β | ∀ᶠ n : α in f, c ≤ u n }), b < c := by
  simp_rw [exists_prop]
  exact exists_lt_of_lt_csSup hu h

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
c : β
hc : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
⊢ ∃ c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}, b < c

Tactic:
exact exists_lt_of_lt_csSup hu h

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
c : β
hc : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a

Tactic:
exact hc.mono fun x hx => lt_of_lt_of_le hbc hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
⊢ ∃ c, ∃ (_ : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}), b < c

Tactic:
simp_rw [exists_prop]

Result:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
⊢ ∃ c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}, b < c
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_monomial {d : σ →₀ ℕ} (c : R) :
    m.leadingCoeff (monomial d c) = c

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d) c) = c

Tactic:
simp only [leadingCoeff, degree_monomial]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ coeff (if c = 0 then 0 else d) ((monomial d) c) = c

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ coeff (if c = 0 then 0 else d) ((monomial d) c) = c

Tactic:
split_ifs with hc <;> simp [hc]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d) c) = c

Tactic:
classical
simp only [leadingCoeff, degree_monomial]
split_ifs with hc <;> simp [hc]

Result:
no goals
-- Mathlib/Order/WellFounded.lean
theorem StrictMono.not_bddAbove_range_of_wellFoundedLT {f : β → β} [WellFoundedLT β] [NoMaxOrder β]
    (hf : StrictMono f) : ¬ BddAbove (Set.range f)

Proof state:
case intro
β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
⊢ False

Tactic:
obtain ⟨b, hb⟩ := exists_gt a

Result:
case intro.intro
β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
b : β
hb : a < b
⊢ False

Proof state:
β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
⊢ ¬BddAbove (Set.range f)

Tactic:
rintro ⟨a, ha⟩

Result:
case intro
β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
⊢ False

Proof state:
case intro.intro
β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
b : β
hb : a < b
⊢ False

Tactic:
exact ((hf.le_apply.trans_lt (hf hb)).trans_le <| ha (Set.mem_range_self _)).false

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem measure_preimage_lt_top_of_memLp (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) (f : α →ₛ E)
    (hf : MemLp f p μ) (y : E) (hy_ne : y ≠ 0) : μ (f ⁻¹' {y}) < ∞

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∈ f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
specialize hf_eLpNorm y hyf

Result:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (⇑f ⁻¹' {y}) < ⊤
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
lemma conjTranspose_mul_mul_same {A : Matrix n n R} (hA : PosSemidef A)
    {m : Type*} [Fintype m] (B : Matrix n m R) :
    PosSemidef (Bᴴ * A * B)

Proof state:
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix n m R
⊢ (Bᴴ * A * B).PosSemidef

Tactic:
constructor

Result:
case left
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix n m R
⊢ (Bᴴ * A * B).IsHermitian

case right
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix n m R
⊢ ∀ (x : m → R), 0 ≤ star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x

Proof state:
case left
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix n m R
⊢ (Bᴴ * A * B).IsHermitian

Tactic:
exact isHermitian_conjTranspose_mul_mul B hA.1

Result:
no goals

Proof state:
case right
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix n m R
x : m → R
⊢ 0 ≤ star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x

Tactic:
simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.2 (B *ᵥ x)

Result:
no goals

Proof state:
case right
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix n m R
⊢ ∀ (x : m → R), 0 ≤ star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x

Tactic:
intro x

Result:
case right
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
m : Type u_5
inst✝ : Fintype m
B : Matrix n m R
x : m → R
⊢ 0 ≤ star x ⬝ᵥ (Bᴴ * A * B) *ᵥ x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem safe_insert_of_performRupCheck_insertRat {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (rupHints : Array Nat) :
    (performRupCheck (insertRatUnits f (negate c)).1 rupHints).2.2.1 = true
      →
    Limplies (PosFin n) f (f.insert c)

Proof state:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ p ⊨ c'

Tactic:
exact pf c' c'_in_f

Result:
no goals