harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_ge_of_countable_range' (hτ : IsStoppingTime f τ)
    (h_countable : (Set.range τ).Countable) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | i ≤ τ ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | i ≤ τ ω} ↔ ω ∈ {ω | τ ω = i} ∪ {ω | i < τ ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}
⊢ MeasurableSet ({ω | τ ω = i} ∪ {ω | i < τ ω})

Tactic:
exact (hτ.measurableSet_eq_of_countable_range' h_countable i).union (hτ.measurableSet_gt' i)

Result:
no goals

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ i < τ ω ∨ i = τ ω ↔ τ ω = i ∨ i < τ ω

Tactic:
rw [@eq_comm _ i, or_comm]

Result:
no goals

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | i ≤ τ ω} ↔ ω ∈ {ω | τ ω = i} ∪ {ω | i < τ ω}

Tactic:
simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ i < τ ω ∨ i = τ ω ↔ τ ω = i ∨ i < τ ω

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}
⊢ MeasurableSet {ω | i ≤ τ ω}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}
⊢ MeasurableSet ({ω | τ ω = i} ∪ {ω | i < τ ω})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | i ≤ τ ω}

Tactic:
have : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω} := by
  ext1 ω
  simp only [le_iff_lt_or_eq, Set.mem_setOf_eq, Set.mem_union]
  rw [@eq_comm _ i, or_comm]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}
⊢ MeasurableSet {ω | i ≤ τ ω}
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isNClique_compl : Gᶜ.IsNClique n s ↔ G.IsNIndepSet n s

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNClique n s ↔ G.IsNIndepSet n s

Tactic:
rw [isNIndepSet_iff]

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNClique n s ↔ G.IsIndepSet ↑s ∧ #s = n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNClique n s ↔ G.IsIndepSet ↑s ∧ #s = n

Tactic:
simp [isNClique_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma iSup_genEigenspace_eq (f : End R M) (μ : R) :
    ⨆ k : ℕ, (f.genEigenspace μ) k = f.maxGenEigenspace μ

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ⨆ k, (f.genEigenspace μ) ↑k = f.maxGenEigenspace μ

Tactic:
simp_rw [maxGenEigenspace, genEigenspace_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Ψ_zero : W.Ψ 0 = 0

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ 0 = 0

Tactic:
rw [← Nat.cast_zero, Ψ_ofNat, preΨ'_zero, C_0, zero_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
    (as.push a).all p 0 stop = (as.all p && p a)

Proof state:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ ({ toList := toList✝ }.push a).all p 0 stop = ({ toList := toList✝ }.all p && p a)

Tactic:
rw [List.push_toArray]

Result:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ (toList✝ ++ [a]).toArray.all p 0 stop = ({ toList := toList✝ }.all p && p a)

Proof state:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ (toList✝ ++ [a]).toArray.all p 0 stop = ({ toList := toList✝ }.all p && p a)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
stop : Nat
inst✝ : BEq α
as : Array α
a : α
p : α → Bool
h : stop = as.size + 1
⊢ (as.push a).all p 0 stop = (as.all p && p a)

Tactic:
cases as

Result:
case mk
α : Type u_1
stop : Nat
inst✝ : BEq α
a : α
p : α → Bool
toList✝ : List α
h : stop = { toList := toList✝ }.size + 1
⊢ ({ toList := toList✝ }.push a).all p 0 stop = ({ toList := toList✝ }.all p && p a)
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem decompose {x y : ℤ} : (⟨x, y⟩ : ℤ√d) = x + sqrtd (d := d) * y

Proof state:
d x y : ℤ
⊢ { re := x, im := y } = ↑x + sqrtd * ↑y

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem order_zero : (0 : FormalMultilinearSeries 𝕜 E F).order = 0

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
⊢ order 0 = 0

Tactic:
simp [order]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_mkVector_empty : (mkVector n (#v[] : Vector α 0)).flatten = #v[]

Proof state:
n : Nat
α : Type u_1
⊢ (mkVector n { toArray := #[], size_toArray := ⋯ }).flatten.toArray = { toArray := #[], size_toArray := ⋯ }.toArray

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α : Type u_1
⊢ (mkVector n { toArray := #[], size_toArray := ⋯ }).flatten = { toArray := #[], size_toArray := ⋯ }

Tactic:
rw [← toArray_inj]

Result:
n : Nat
α : Type u_1
⊢ (mkVector n { toArray := #[], size_toArray := ⋯ }).flatten.toArray = { toArray := #[], size_toArray := ⋯ }.toArray
-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
theorem HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum
    (h : HasFPowerSeriesOnBall f p x r) (h' : AnalyticOn 𝕜 f univ) {n : ℕ} (v : Fin n → E) :
    iteratedFDeriv 𝕜 n f x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ (iteratedFDerivWithin 𝕜 n f univ x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)

Tactic:
exact h.iteratedFDerivWithin_eq_sum h' uniqueDiffOn_univ (mem_univ x) v

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
⊢ (iteratedFDeriv 𝕜 n f x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)

Tactic:
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ (iteratedFDerivWithin 𝕜 n f univ x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)
-- Mathlib/Topology/Constructions.lean
lemma Pi.induced_restrict (S : Set ι) :
    induced (S.restrict) Pi.topologicalSpace =
    ⨅ i ∈ S, induced (eval i) (T i)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
S : Set ι
⊢ induced S.restrict topologicalSpace = ⨅ i ∈ S, induced (eval i) (T i)

Tactic:
simp (config := { unfoldPartialApp := true }) [← iInf_subtype'', ← induced_precomp' ((↑) : S → ι),
  restrict]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem inter_nonempty_of_card_lt_card_add_card (hts : t ⊆ s) (hus : u ⊆ s)
    (hstu : #s < #t + #u) : (t ∩ u).Nonempty

Proof state:
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : ¬(t ∩ u).Nonempty
⊢ #t + #u ≤ #s

Tactic:
calc
  _ = #(t ∪ u) := by simp [← card_union_add_card_inter, not_nonempty_iff_eq_empty.1 hstu]
  _ ≤ #s := by gcongr; exact union_subset hts hus

Result:
no goals

Proof state:
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : ¬(t ∩ u).Nonempty
⊢ #t + #u = #(t ∪ u)

Tactic:
simp [← card_union_add_card_inter, not_nonempty_iff_eq_empty.1 hstu]

Result:
no goals

Proof state:
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : #s < #t + #u
⊢ (t ∩ u).Nonempty

Tactic:
contrapose! hstu

Result:
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : ¬(t ∩ u).Nonempty
⊢ #t + #u ≤ #s

Proof state:
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : ¬(t ∩ u).Nonempty
⊢ #(t ∪ u) ≤ #s

Tactic:
gcongr

Result:
case a
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : ¬(t ∩ u).Nonempty
⊢ t ∪ u ⊆ s

Proof state:
case a
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : ¬(t ∩ u).Nonempty
⊢ t ∪ u ⊆ s

Tactic:
exact union_subset hts hus

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem mkPiRing_apply_one_eq_self [Fintype ι] (f : MultilinearMap R (fun _ : ι => R) M₂) :
    MultilinearMap.mkPiRing R ι (f fun _ => 1) = f

Proof state:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
this : m = fun i => m i • 1
⊢ (MultilinearMap.mkPiRing R ι (f fun x => 1)) m = (∏ i : ι, m i) • f fun i => 1

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
j : ι
⊢ m j = m j • 1

Tactic:
simp

Result:
no goals

Proof state:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
this : m = fun i => m i • 1
⊢ (MultilinearMap.mkPiRing R ι (f fun x => 1)) m = f m

Tactic:
conv_rhs => rw [this, f.map_smul_univ]

Result:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
this : m = fun i => m i • 1
⊢ (MultilinearMap.mkPiRing R ι (f fun x => 1)) m = (∏ i : ι, m i) • f fun i => 1

Proof state:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
⊢ (MultilinearMap.mkPiRing R ι (f fun x => 1)) m = f m

Tactic:
have : m = fun i => m i • (1 : R) := by
  ext j
  simp

Result:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
this : m = fun i => m i • 1
⊢ (MultilinearMap.mkPiRing R ι (f fun x => 1)) m = f m

Proof state:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
⊢ m = fun i => m i • 1

Tactic:
ext j

Result:
case h
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
j : ι
⊢ m j = m j • 1

Proof state:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
⊢ MultilinearMap.mkPiRing R ι (f fun x => 1) = f

Tactic:
ext m

Result:
case H
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
f : MultilinearMap R (fun x => R) M₂
m : ι → R
⊢ (MultilinearMap.mkPiRing R ι (f fun x => 1)) m = f m
-- Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
lemma prod_lt_prod_of_nonempty (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i)
    (h_ne : s.Nonempty) :
    ∏ i ∈ s, f i < ∏ i ∈ s, g i

Proof state:
case intro
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i ∈ s, f i < g i

Tactic:
exact ⟨i, hi, hfg i hi⟩

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
⊢ ∏ i ∈ s, f i < ∏ i ∈ s, g i

Tactic:
apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)

Result:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
⊢ ∃ i ∈ s, f i < g i

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
⊢ ∃ i ∈ s, f i < g i

Tactic:
obtain ⟨i, hi⟩ := h_ne

Result:
case intro
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i ∈ s, f i < g i
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem ite_prod_one (p : Prop) [Decidable p] (s : Finset α) (f : α → β) :
    (if p then (∏ x ∈ s, f x) else 1) = ∏ x ∈ s, if p then f x else 1

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
p : Prop
inst✝ : Decidable p
s : Finset α
f : α → β
⊢ (if p then ∏ x ∈ s, f x else 1) = ∏ x ∈ s, if p then f x else 1

Tactic:
simp only [prod_ite_irrel, prod_const_one]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma toNNReal_le_one {r : ℝ} : r.toNNReal ≤ 1 ↔ r ≤ 1

Proof state:
r : ℝ
⊢ r.toNNReal ≤ 1 ↔ r ≤ 1

Tactic:
simpa using toNNReal_le_toNNReal_iff zero_le_one

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
theorem ext_iff' : κ = η ↔ ∀ a s, MeasurableSet s → κ a s = η a s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s

Tactic:
simp_rw [Kernel.ext_iff, Measure.ext_iff]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_insert_of_not_mem (h : a ∉ s) : #(insert a s) = #s + 1

Proof state:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #(insert a s) = #s + 1

Tactic:
rw [← cons_eq_insert _ _ h, card_cons]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.mulVecLin_transpose [Fintype m] (M : Matrix m n R) :
    Mᵀ.mulVecLin = M.vecMulLinear

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype m
M : Matrix m n R
⊢ Mᵀ.mulVecLin = M.vecMulLinear

Tactic:
ext

Result:
case h.h
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype m
M : Matrix m n R
x✝¹ : m → R
x✝ : n
⊢ Mᵀ.mulVecLin x✝¹ x✝ = M.vecMulLinear x✝¹ x✝

Proof state:
case h.h
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype m
M : Matrix m n R
x✝¹ : m → R
x✝ : n
⊢ Mᵀ.mulVecLin x✝¹ x✝ = M.vecMulLinear x✝¹ x✝

Tactic:
simp [mulVec_transpose]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem cast_toNat_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) : ↑(toNat c) = c

Proof state:
case intro
c : ℕ
⊢ ↑(toNat ↑c) = ↑c

Tactic:
rw [toNat_natCast]

Result:
no goals

Proof state:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ↑(toNat c) = c

Tactic:
lift c to ℕ using h

Result:
case intro
c : ℕ
⊢ ↑(toNat ↑c) = ↑c
-- Mathlib/Data/List/Lex.lean
theorem ne_iff {l₁ l₂ : List α} (H : length l₁ ≤ length l₂) : Lex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂

Proof state:
α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
classical
exact Decidable.List.Lex.ne_iff H

Result:
no goals

Proof state:
α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
exact Decidable.List.Lex.ne_iff H

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerRight_id_symm {X Y : C} (f : X ⟶ Y) :
    f = (ρ_ X).inv ≫ f ▷ 𝟙_ C ≫ (ρ_ Y).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f = (ρ_ X).inv ≫ f ▷ 𝟙_ C ≫ (ρ_ Y).hom

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/FiniteAbelian/Basic.lean
/-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
some `ZMod (n i)` for some natural numbers `n i > 1`. -/
lemma equiv_directSum_zmod_of_finite' (G : Type*) [AddCommGroup G] [Finite G] :
    ∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ),
      (∀ i, 1 < n i) ∧ Nonempty (G ≃+ ⨁ i, ZMod (n i))

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
  ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩

Result:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
⊢ ∀ (i : { i // n i ≠ 0 }), 1 < (fun i => p ↑i ^ n ↑i) i

Proof state:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G

Result:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ ⨁ (i : ι), ZMod (n i))

Proof state:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
classical
obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
  ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
rintro ⟨i, hi⟩
exact one_lt_pow₀ (hp _).one_lt hi

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
⊢ ∀ (i : { i // n i ≠ 0 }), 1 < (fun i => p ↑i ^ n ↑i) i

Tactic:
rintro ⟨i, hi⟩

Result:
case intro.intro.intro.intro.intro.intro.mk
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
i : ι
hi : n i ≠ 0
⊢ 1 < (fun i => p ↑i ^ n ↑i) ⟨i, hi⟩

Proof state:
case intro.intro.intro.intro.intro.intro.mk
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
i : ι
hi : n i ≠ 0
⊢ 1 < (fun i => p ↑i ^ n ↑i) ⟨i, hi⟩

Tactic:
exact one_lt_pow₀ (hp _).one_lt hi

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
lemma mul_eq_neg_one_iff_eq_one_or_neg_one : u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Proof state:
u v : ℤ
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
  obtain ⟨rfl, rfl⟩ := H <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem one_mul (s : LowerSet α) : 1 * s = s :=
  SetLike.coe_injective <|
    (subset_mul_right _ right_mem_Iic).antisymm' <| by
      rw [← smul_eq_mul, ← Set.iUnion_smul_set]
      exact Set.iUnion₂_subset fun _ ↦ s.lower.smul_subset

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s : LowerSet α
⊢ Set.Iic 1 * ↑s ⊆ ↑s

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s : LowerSet α
⊢ ⋃ a ∈ Set.Iic 1, a • ↑s ⊆ ↑s

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s : LowerSet α
⊢ ⋃ a ∈ Set.Iic 1, a • ↑s ⊆ ↑s

Tactic:
exact Set.iUnion₂_subset fun _ ↦ s.lower.smul_subset

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_count [MeasurableSingletonClass α] (f : α → ℝ≥0∞) :
    ∫⁻ a, f a ∂count = ∑' a, f a

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∑' (i : α), ∫⁻ (a : α), f a ∂dirac i = ∑' (a : α), f a

Tactic:
congr

Result:
case e_f
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ (fun i => ∫⁻ (a : α), f a ∂dirac i) = fun a => f a

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂count = ∑' (a : α), f a

Tactic:
rw [count, lintegral_sum_measure]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∑' (i : α), ∫⁻ (a : α), f a ∂dirac i = ∑' (a : α), f a

Proof state:
case e_f
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ (fun i => ∫⁻ (a : α), f a ∂dirac i) = fun a => f a

Tactic:
exact funext fun a => lintegral_dirac a f

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_sub_Ioc : (fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b)

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem inv_eq_of_inv_hom_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = 𝟙 Y) :
    inv f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
inv_hom_id : g ≫ f = 𝟙 Y
⊢ inv f = g

Tactic:
apply (cancel_mono f).mp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
inv_hom_id : g ≫ f = 𝟙 Y
⊢ inv f ≫ f = g ≫ f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
inv_hom_id : g ≫ f = 𝟙 Y
⊢ inv f ≫ f = g ≫ f

Tactic:
simp [inv_hom_id]

Result:
no goals