harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_mul_right {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :
    normalize (n * a) (d * a) (Nat.mul_ne_zero d0 a0) = normalize n d d0

Proof state:
d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (n * ↑a) (d * a) ⋯ = normalize (↑a * n) (a * d) ⋯

Tactic:
congr 1 <;> [apply Int.mul_comm; apply Nat.mul_comm]

Result:
no goals

Proof state:
d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (n * ↑a) (d * a) ⋯ = normalize n d d0

Tactic:
rw [← normalize_mul_left (d0 := d0) a0]

Result:
d : Nat
n : Int
a : Nat
d0 : d ≠ 0
a0 : a ≠ 0
⊢ normalize (n * ↑a) (d * a) ⋯ = normalize (↑a * n) (a * d) ⋯
-- Mathlib/Order/Compare.lean
theorem cmp_swap [Preorder α] [DecidableRel (α := α) (· < ·)] (a b : α) :
    (cmp a b).swap = cmp b a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a b : α
⊢ (if (fun x1 x2 => x1 < x2) a b then lt else if (fun x1 x2 => x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 => x1 < x2) b a then lt else if (fun x1 x2 => x1 < x2) a b then gt else eq

Tactic:
by_cases h : a < b <;> by_cases h₂ : b < a <;> simp [h, h₂, Ordering.swap]

Result:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a b : α
h : a < b
h₂ : b < a
⊢ False

Proof state:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a b : α
h : a < b
h₂ : b < a
⊢ False

Tactic:
exact lt_asymm h h₂

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a b : α
⊢ (cmp a b).swap = cmp b a

Tactic:
unfold cmp cmpUsing

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a b : α
⊢ (if (fun x1 x2 => x1 < x2) a b then lt else if (fun x1 x2 => x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 => x1 < x2) b a then lt else if (fun x1 x2 => x1 < x2) a b then gt else eq
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem measurableSet_support [MeasurableSpace α] (f : α →ₛ β) : MeasurableSet (support f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (support ⇑f)

Tactic:
rw [f.support_eq]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ⇑f ⁻¹' {y})

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ⇑f ⁻¹' {y})

Tactic:
exact Finset.measurableSet_biUnion _ fun y _ => measurableSet_fiber _ _

Result:
no goals
-- Mathlib/Algebra/Group/Prod.lean
theorem comp_coprod {Q : Type*} [CommSemigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :
    h.comp (f.coprod g) = (h.comp f).coprod (h.comp g) :=
  ext fun x => by simp

Proof state:
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : CommSemigroup P
Q : Type u_6
inst✝ : CommSemigroup Q
h : P →ₙ* Q
f : M →ₙ* P
g : N →ₙ* P
x : M × N
⊢ (h.comp (f.coprod g)) x = ((h.comp f).coprod (h.comp g)) x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem ultrafilter_extend_extends (f : α → γ) : Ultrafilter.extend f ∘ pure = f

Proof state:
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
⊢ Ultrafilter.extend f ∘ pure = f

Tactic:
letI : TopologicalSpace α := ⊥

Result:
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this : TopologicalSpace α := ⊥
⊢ Ultrafilter.extend f ∘ pure = f

Proof state:
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this : TopologicalSpace α := ⊥
⊢ Ultrafilter.extend f ∘ pure = f

Tactic:
haveI : DiscreteTopology α := ⟨rfl⟩

Result:
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Ultrafilter.extend f ∘ pure = f

Proof state:
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Ultrafilter.extend f ∘ pure = f

Tactic:
exact funext (isDenseInducing_pure.extend_eq continuous_of_discreteTopology)

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem mapMono_id : mapMono K (𝟙 Δ) = 𝟙 _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
Δ : SimplexCategory
⊢ (if h : Δ = Δ then eqToHom ⋯ else if h : Isδ₀ (𝟙 Δ) then K.d Δ.len Δ.len else 0) = 𝟙 (K.X Δ.len)

Tactic:
simp only [eq_self_iff_true, eqToHom_refl, dite_eq_ite, if_true]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
Δ : SimplexCategory
⊢ mapMono K (𝟙 Δ) = 𝟙 (K.X Δ.len)

Tactic:
unfold mapMono

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K : ChainComplex C ℕ
Δ : SimplexCategory
⊢ (if h : Δ = Δ then eqToHom ⋯ else if h : Isδ₀ (𝟙 Δ) then K.d Δ.len Δ.len else 0) = 𝟙 (K.X Δ.len)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_expand [BEq α] [Hashable α] [PartialEquivBEq α]
    {buckets : {d : Array (AssocList α β) // 0 < d.size}} :
    Perm (toListModel (expand buckets).1) (toListModel buckets.1)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
buckets : { d // 0 < d.size }
⊢ 0 < (mkArray (buckets.val.size * 2) AssocList.nil).size

Tactic:
simpa using Nat.mul_pos buckets.2 Nat.two_pos

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
buckets : { d // 0 < d.size }
⊢ toListModel (expand buckets).val ~ toListModel buckets.val

Tactic:
simpa [expand, expand.go_eq] using toListModel_foldl_reinsertAux (toListModel buckets.1)
  ⟨mkArray (buckets.1.size * 2) .nil, by simpa using Nat.mul_pos buckets.2 Nat.two_pos⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_flatMap {α β} (f : α → β) (l : Array α) : map f l = l.flatMap fun x => #[f x]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f l = flatMap (fun x => #[f x]) l

Tactic:
simp only [← map_singleton]

Result:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f l = flatMap (fun x => map f #[x]) l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f l = flatMap (fun x => map f #[x]) l

Tactic:
rw [← flatMap_singleton' l, map_flatMap, flatMap_singleton']

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem pure_bind (a : α) (f : α → PMF β) : (pure a).bind f = f a

Proof state:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
this : ∀ (b : β) (a' : α), (if a' = a then (f a') b else 0) = if a' = a then (f a) b else 0
⊢ (pure a).bind f = f a

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
this : ∀ (b : β) (a' : α), (if a' = a then (f a') b else 0) = if a' = a then (f a) b else 0
b : β
⊢ ((pure a).bind f) b = (f a) b

Proof state:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
b : β
a' : α
⊢ (if a' = a then (f a') b else 0) = if a' = a then (f a) b else 0

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

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
⊢ (pure a).bind f = f a

Tactic:
classical
have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by
  split_ifs with h <;> simp [h]
ext b
simp [this]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
⊢ (pure a).bind f = f a

Tactic:
have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by
  split_ifs with h <;> simp [h]

Result:
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
this : ∀ (b : β) (a' : α), (if a' = a then (f a') b else 0) = if a' = a then (f a) b else 0
⊢ (pure a).bind f = f a

Proof state:
case h
α : Type u_1
β : Type u_2
a : α
f : α → PMF β
this : ∀ (b : β) (a' : α), (if a' = a then (f a') b else 0) = if a' = a then (f a) b else 0
b : β
⊢ ((pure a).bind f) b = (f a) b

Tactic:
simp [this]

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
lemma LieSubmodule.coe_toEnd_pow (N : LieSubmodule R L M) (x : L) (y : N) (n : ℕ) :
    ((toEnd R L N x ^ n) y : M) = (toEnd R L M x ^ n) y

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
y : ↥N
⊢ ↑(((toEnd R L ↥N) x ^ 0) y) = ((toEnd R L M) x ^ 0) ↑y

Tactic:
rfl

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
n : ℕ
ih : ∀ (y : ↥N), ↑(((toEnd R L ↥N) x ^ n) y) = ((toEnd R L M) x ^ n) ↑y
y : ↥N
⊢ ↑(((toEnd R L ↥N) x ^ (n + 1)) y) = ((toEnd R L M) x ^ (n + 1)) ↑y

Tactic:
simp only [pow_succ', LinearMap.mul_apply, ih, LieSubmodule.coe_toEnd]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
y : ↥N
n : ℕ
⊢ ↑(((toEnd R L ↥N) x ^ n) y) = ((toEnd R L M) x ^ n) ↑y

Tactic:
induction n generalizing y with
| zero => rfl
| succ n ih => simp only [pow_succ', LinearMap.mul_apply, ih, LieSubmodule.coe_toEnd]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem Monic.prod {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι}
    (H : ∀ i ∈ s, m.Monic (P i)) :
    m.Monic (∏ i ∈ s, P i)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))

Tactic:
intro i hi

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular (m.leadingCoeff (P i))

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ m.Monic (∏ i ∈ s, P i)

Tactic:
rw [Monic, leadingCoeff_prod_of_regular]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∏ i ∈ s, m.leadingCoeff (P i) = 1

σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∏ i ∈ s, m.leadingCoeff (P i) = 1

Tactic:
exact Finset.prod_eq_one H

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular (m.leadingCoeff (P i))

Tactic:
rw [(H i hi).leadingCoeff_eq_one]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular 1

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular 1

Tactic:
exact isRegular_one

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.inf_principal (hl : l.HasBasis p s) (s' : Set α) :
    (l ⊓ 𝓟 s').HasBasis p fun i => s i ∩ s' :=
  ⟨fun t => by
    simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_setOf_eq, mem_inter_iff, and_imp]⟩

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
s' t : Set α
⊢ t ∈ l ⊓ 𝓟 s' ↔ ∃ i, p i ∧ s i ∩ s' ⊆ t

Tactic:
simp only [mem_inf_principal, hl.mem_iff, subset_def, mem_setOf_eq, mem_inter_iff, and_imp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insertIfNew k v).size = if m.contains k = true then m.size else m.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insertIfNew k v).size = if m.contains k = true then m.size else m.size + 1

Tactic:
simp_to_raw using Raw₀.size_insertIfNew

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean
theorem energy_le_one : P.energy G ≤ 1 :=
  div_le_of_le_mul₀ (sq_nonneg _) zero_le_one <|
    calc
      ∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2 ≤ #P.parts.offDiag • (1 : ℚ) :=
        sum_le_card_nsmul _ _ 1 fun _ _ =>
          (sq_le_one_iff₀ <| G.edgeDensity_nonneg _ _).2 <| G.edgeDensity_le_one _ _
      _ = #P.parts.offDiag := Nat.smul_one_eq_cast _
      _ ≤ _

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts * #P.parts - #P.parts) ≤ ↑(#P.parts) ^ 2

Tactic:
norm_cast

Result:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts ^ 2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts

Tactic:
exact tsub_le_self

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts.offDiag) ≤ 1 * ↑(#P.parts) ^ 2

Tactic:
rw [offDiag_card, one_mul]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts * #P.parts - #P.parts) ≤ ↑(#P.parts) ^ 2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts ^ 2

Tactic:
rw [sq]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_vecMul [Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) :
    v ᵥ* M ᵥ* N = v ᵥ* (M * N)

Proof state:
case h
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
x✝ : o
⊢ (v ᵥ* M ᵥ* N) x✝ = (v ᵥ* (M * N)) x✝

Tactic:
apply dotProduct_assoc

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
⊢ v ᵥ* M ᵥ* N = v ᵥ* (M * N)

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
x✝ : o
⊢ (v ᵥ* M ᵥ* N) x✝ = (v ᵥ* (M * N)) x✝
-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma measure_univ_unique (hμ : IsProjectiveLimit μ P) (hν : IsProjectiveLimit ν P) :
    μ univ = ν univ

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ ν : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit μ P
hν : IsProjectiveLimit ν P
⊢ μ univ = ν univ

Tactic:
rw [hμ.measure_univ_eq (∅ : Finset ι), hν.measure_univ_eq (∅ : Finset ι)]

Result:
no goals
-- Mathlib/Order/Filter/CountableInter.lean
theorem le_countableGenerate_iff_of_countableInterFilter {f : Filter α} [CountableInterFilter f] :
    f ≤ countableGenerate g ↔ g ⊆ f.sets

Proof state:
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets

case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g

Proof state:
case mpr.superset
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s s✝ t✝ : Set α
a✝ : CountableGenerateSets g s✝
st : s✝ ⊆ t✝
ih : s✝ ∈ f
⊢ t✝ ∈ f

Tactic:
exact mem_of_superset ih st

Result:
no goals

Proof state:
case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
hs : s ∈ countableGenerate g
⊢ s ∈ f

Tactic:
induction hs with
| basic hs => exact h hs
| univ => exact univ_mem
| superset _ st ih => exact mem_of_superset ih st
| sInter Sct _ ih => exact (countable_sInter_mem Sct).mpr ih

Result:
no goals

Proof state:
case mpr.basic
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s s✝ : Set α
hs : s✝ ∈ g
⊢ s✝ ∈ f

Tactic:
exact h hs

Result:
no goals

Proof state:
case mpr.univ
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ univ ∈ f

Tactic:
exact univ_mem

Result:
no goals

Proof state:
case mpr.sInter
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
S✝ : Set (Set α)
Sct : S✝.Countable
a✝ : ∀ s ∈ S✝, CountableGenerateSets g s
ih : ∀ s ∈ S✝, s ∈ f
⊢ ⋂₀ S✝ ∈ f

Tactic:
exact (countable_sInter_mem Sct).mpr ih

Result:
no goals

Proof state:
case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g

Tactic:
intro s hs

Result:
case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
hs : s ∈ countableGenerate g
⊢ s ∈ f

Proof state:
case mp
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets

Tactic:
exact subset_trans (fun s => CountableGenerateSets.basic) h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
    (Const.alter m k f).getKey? k = if (f (Const.get? m k)).isSome then some k else none

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
⊢ (alter m k f).getKey? k = if (f (get? m k)).isSome = true then some k else none

Tactic:
simp [getKey?_alter]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem aeval_id_rename (f : σ → MvPolynomial τ R) (p : MvPolynomial σ R) :
    aeval id (rename f p) = aeval f p

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → MvPolynomial τ R
p : MvPolynomial σ R
⊢ (aeval id) ((rename f) p) = (aeval f) p

Tactic:
rw [aeval_rename, Function.id_comp]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_eq_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
n : ℕ
ha : 0 ≤ a
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1

Tactic:
simpa only [one_pow] using pow_left_inj₀ ha zero_le_one hn

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem coeff_p_zero [CharP R p] : (p : 𝕎 R).coeff 0 = 0

Proof state:
case hnc
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ ¬0 = 1

Tactic:
exact zero_ne_one

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ (↑p).coeff 0 = 0

Tactic:
rw [coeff_p, if_neg]

Result:
case hnc
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ ¬0 = 1
-- Mathlib/RingTheory/Kaehler/Basic.lean
lemma KaehlerDifferential.mapBaseChange_surjective
    (h : Function.Surjective (algebraMap A B)) :
    Function.Surjective (KaehlerDifferential.mapBaseChange R A B)

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
this : Subsingleton (Ω[B⁄A])
⊢ ⊤ ≤ LinearMap.ker (map R A B B)

Tactic:
exact fun x _ ↦ Subsingleton.elim _ _

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Function.Surjective ⇑(mapBaseChange R A B)

Tactic:
have := subsingleton_of_surjective A B h

Result:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
this : Subsingleton (Ω[B⁄A])
⊢ Function.Surjective ⇑(mapBaseChange R A B)

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
this : Subsingleton (Ω[B⁄A])
⊢ Function.Surjective ⇑(mapBaseChange R A B)

Tactic:
rw [← LinearMap.range_eq_top, range_mapBaseChange, ← top_le_iff]

Result:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
this : Subsingleton (Ω[B⁄A])
⊢ ⊤ ≤ LinearMap.ker (map R A B B)
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_zero (m : ℕ) : hyperoperation 0 m = Nat.succ :=
  funext fun k => by rw [hyperoperation, Nat.succ_eq_add_one]

Proof state:
m k : ℕ
⊢ hyperoperation 0 m k = k.succ

Tactic:
rw [hyperoperation, Nat.succ_eq_add_one]

Result:
no goals