harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Quotient.lean
theorem compClosure_eq_self [h : Congruence r] :
    CompClosure r = r

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
⊢ CompClosure r = r

Tactic:
ext

Result:
case h.h.h.h.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ CompClosure r x✝¹ x✝ ↔ r x✝¹ x✝

Proof state:
case h.h.h.h.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ CompClosure r x✝¹ x✝ ↔ r x✝¹ x✝

Tactic:
simp only [compClosure_iff_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.lean
theorem blastSignExtend_empty_eq_zeroExtend (aig : AIG α) (target : ExtendTarget aig newWidth)
    (htarget : target.w = 0) :
    blastSignExtend aig target = blastZeroExtend aig target

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
htarget : target.w = 0
⊢ blastSignExtend aig target = blastZeroExtend aig target

Tactic:
unfold blastSignExtend

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
htarget : target.w = 0
⊢ (match target with
    | { w := width, vec := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, vec := input }
      else { aig := aig, vec := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefVec.empty }) =
    blastZeroExtend aig target

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
htarget : target.w = 0
⊢ (match target with
    | { w := width, vec := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, vec := input }
      else { aig := aig, vec := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefVec.empty }) =
    blastZeroExtend aig target

Tactic:
simp [htarget]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α}
    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
    getValueCast? k (insertList l toInsert) = getValueCast? k l

Proof state:
case h
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ getEntry? k (insertList l toInsert) = getEntry? k l

Tactic:
rw [getEntry?_insertList_of_contains_eq_false not_contains]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ getValueCast? k (insertList l toInsert) = getValueCast? k l

Tactic:
rw [getValueCast?_eq_getEntry?, getValueCast?_eq_getEntry?]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? k l) fun p h => cast ⋯ p.snd

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? k (insertList l toInsert)) fun p h => cast ⋯ p.snd) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? k l) fun p h => cast ⋯ p.snd

Tactic:
apply Option.dmap_congr

Result:
case h
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ getEntry? k (insertList l toInsert) = getEntry? k l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : (List.map Sigma.fst toInsert).contains k = false
⊢ getValueCast? k (insertList l toInsert) = getValueCast? k l

Tactic:
rw [← containsKey_eq_contains_map_fst] at not_contains

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ getValueCast? k (insertList l toInsert) = getValueCast? k l
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem countable_iff_lt_aleph_one {α : Type*} (s : Set α) : s.Countable ↔ #s < ℵ₁

Proof state:
α : Type u_1
s : Set α
⊢ s.Countable ↔ #↑s < ℵ_ 1

Tactic:
rw [← succ_aleph0, lt_succ_iff, le_aleph0_iff_set_countable]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma Cover.toPresieveOver_le_arrows_iff {X : Over S} (R : Sieve X) (𝒰 : Cover.{u} P X.left)
    [𝒰.Over S] :
    𝒰.toPresieveOver ≤ R.arrows ↔
      Presieve.ofArrows 𝒰.obj 𝒰.map ≤ (Sieve.overEquiv X R).arrows

Proof state:
P : MorphismProperty Scheme
S : Scheme
X : Over S
R : Sieve X
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
⊢ (Sieve.overEquiv X) (Sieve.generate 𝒰.toPresieveOver) ≤ (Sieve.overEquiv X) R ↔
    Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map) ≤ (Sieve.overEquiv X) R

Tactic:
rw [overEquiv_generate_toPresieveOver_eq_ofArrows]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
S : Scheme
X : Over S
R : Sieve X
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
⊢ 𝒰.toPresieveOver ≤ R.arrows ↔ Presieve.ofArrows 𝒰.obj 𝒰.map ≤ ((Sieve.overEquiv X) R).arrows

Tactic:
simp_rw [← Sieve.giGenerate.gc.le_iff_le, ← Sieve.overEquiv_le_overEquiv_iff]

Result:
P : MorphismProperty Scheme
S : Scheme
X : Over S
R : Sieve X
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
⊢ (Sieve.overEquiv X) (Sieve.generate 𝒰.toPresieveOver) ≤ (Sieve.overEquiv X) R ↔
    Sieve.generate (Presieve.ofArrows 𝒰.obj 𝒰.map) ≤ (Sieve.overEquiv X) R
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_le_self_of_le_one {x : ℝ≥0} {z : ℝ} (hx : x ≤ 1) (h_one_le : 1 ≤ z) : x ^ z ≤ x

Proof state:
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x

Tactic:
rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))

Result:
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥

case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x

Proof state:
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x ^ 1

Tactic:
exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le

Result:
no goals

Proof state:
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
this : z ≠ 0
⊢ ⊥ ^ z ≤ ⊥

Tactic:
simp [this]

Result:
no goals

Proof state:
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥

Tactic:
have : z ≠ 0 := by linarith

Result:
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
this : z ≠ 0
⊢ ⊥ ^ z ≤ ⊥

Proof state:
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x

Tactic:
nth_rw 2 [← NNReal.rpow_one x]

Result:
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x ^ 1

Proof state:
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ z ≠ 0

Tactic:
linarith

Result:
no goals
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
theorem IsLowerSet.mem_interior_of_forall_lt (hs : IsLowerSet s) (hx : x ∈ closure s)
    (h : ∀ i, y i < x i) : y ∈ interior s

Proof state:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ |x i - z i| ≤ ε

Tactic:
rw [← Real.norm_eq_abs, ← dist_eq_norm]

Result:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ dist (x i) (z i) ≤ ε

Proof state:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ dist (x i) (z i) ≤ ε

Tactic:
exact (hxz _).le

Result:
no goals

Proof state:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
⊢ y ∈ interior s

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
⊢ y ∈ interior s

Proof state:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ ∀ (i : ι), y i < z i

Tactic:
refine fun i =>
  (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans ?_)

Result:
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ |x i - z i| ≤ ε
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_iUnion {m0 : MeasurableSpace α} {μ : Measure α} [Countable ι] {f : ι → Set α}
    (hn : Pairwise (Disjoint on f)) (h : ∀ i, MeasurableSet (f i)) :
    μ (⋃ i, f i) = ∑' i, μ (f i)

Proof state:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → μ (⋃ i, f i) = ∑' (i : ℕ), μ (f i)

Tactic:
exact μ.m_iUnion

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)

Tactic:
rw [measure_eq_extend (MeasurableSet.iUnion h),
  extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]

Result:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∑' (i : ι), extend (fun t _ht => μ t) (f i) = ∑' (i : ι), μ (f i)

ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ μ ∅ = 0

ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → μ (⋃ i, f i) = ∑' (i : ℕ), μ (f i)

Proof state:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ ∑' (i : ι), extend (fun t _ht => μ t) (f i) = ∑' (i : ι), μ (f i)

Tactic:
simp [measure_eq_extend, h]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ μ ∅ = 0

Tactic:
exact μ.empty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_zipIdx' {x : α} {i : Nat} {xs : List α} (h : (x, i) ∈ xs.zipIdx) :
    i < xs.length ∧ x = xs[i]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
  ⟨by simpa using snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩

Proof state:
α : Type ?u.52268
x : α
i : Nat
xs : List α
h : (x, i) ∈ xs.zipIdx
this✝ : 0 ≤ (x, i).snd
this : (x, i).snd < 0 + xs.length
⊢ i < xs.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
x : α
i : Nat
xs : List α
h : (x, i) ∈ xs.zipIdx
⊢ i < xs.length

Tactic:
simpa using snd_lt_add_of_mem_zipIdx h

Result:
no goals

Proof state:
α : Type ?u.52268
x : α
i : Nat
xs : List α
h : (x, i) ∈ xs.zipIdx
⊢ i < xs.length

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.52268
x : α
i : Nat
xs : List α
h : (x, i) ∈ xs.zipIdx
this : 0 ≤ (x, i).snd
⊢ i < xs.length

Proof state:
α : Type ?u.52268
x : α
i : Nat
xs : List α
h : (x, i) ∈ xs.zipIdx
this : 0 ≤ (x, i).snd
⊢ i < xs.length

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.52268
x : α
i : Nat
xs : List α
h : (x, i) ∈ xs.zipIdx
this✝ : 0 ≤ (x, i).snd
this : (x, i).snd < 0 + xs.length
⊢ i < xs.length
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
lemma support_zpowers_of_mem_cycleFactorsFinset_le {g : Perm α}
    {c : g.cycleFactorsFinset} (v : Subgroup.zpowers (c : Perm α)) :
    (v : Perm α).support ≤ g.support

Proof state:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : { x // x ∈ g.cycleFactorsFinset }
v : ↥(Subgroup.zpowers ↑c)
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑v
⊢ (↑c ^ m).support ≤ g.support

Tactic:
exact le_trans (support_zpow_le _ _) (mem_cycleFactorsFinset_support_le c.prop)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : { x // x ∈ g.cycleFactorsFinset }
v : ↥(Subgroup.zpowers ↑c)
⊢ (↑v).support ≤ g.support

Tactic:
obtain ⟨m, hm⟩ := v.prop

Result:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : { x // x ∈ g.cycleFactorsFinset }
v : ↥(Subgroup.zpowers ↑c)
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑v
⊢ (↑v).support ≤ g.support

Proof state:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : { x // x ∈ g.cycleFactorsFinset }
v : ↥(Subgroup.zpowers ↑c)
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑v
⊢ (↑v).support ≤ g.support

Tactic:
simp only [← hm]

Result:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : { x // x ∈ g.cycleFactorsFinset }
v : ↥(Subgroup.zpowers ↑c)
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑v
⊢ (↑c ^ m).support ≤ g.support
-- Mathlib/Analysis/Analytic/Composition.lean
theorem comp_coeff_zero'' (q : FormalMultilinearSeries 𝕜 E F) (p : FormalMultilinearSeries 𝕜 E E) :
    (q.comp p) 0 = q 0

Proof state:
case H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
q : FormalMultilinearSeries 𝕜 E F
p : FormalMultilinearSeries 𝕜 E E
v : Fin 0 → E
⊢ (q.comp p 0) v = (q 0) v

Tactic:
exact q.comp_coeff_zero p _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
q : FormalMultilinearSeries 𝕜 E F
p : FormalMultilinearSeries 𝕜 E E
⊢ q.comp p 0 = q 0

Tactic:
ext v

Result:
case H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
q : FormalMultilinearSeries 𝕜 E F
p : FormalMultilinearSeries 𝕜 E E
v : Fin 0 → E
⊢ (q.comp p 0) v = (q 0) v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (l : Vector α n) (h : ∀ b ∈ l.push a, P b) :
    pmap f (l.push a) h =
      (pmap f l (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp)))

Proof state:
α : Type u_1
β : Type u_2
n : Nat
P : α → Prop
f : (a : α) → P a → β
a : α
l : Vector α n
h : ∀ (b : α), b ∈ l.push a → P b
⊢ pmap f (l.push a) h = (pmap f l ⋯).push (f a ⋯)

Tactic:
simp [pmap]

Result:
no goals

Proof state:
α : Type ?u.8815
β : Type ?u.8864
n : Nat
P : α → Prop
f : (a : α) → P a → β
a✝ : α
l : Vector α n
a : α
m : a ∈ l
h : ∀ (b : α), b ∈ l ∨ b = a✝ → P b
⊢ P a

Tactic:
exact h a (.inl m)

Result:
no goals

Proof state:
α : Type ?u.8815
β : Type ?u.8864
n : Nat
P : α → Prop
f : (a : α) → P a → β
a✝ : α
l : Vector α n
h : ∀ (b : α), b ∈ l.push a✝ → P b
a : α
m : a ∈ l
⊢ P a

Tactic:
simp at h

Result:
α : Type ?u.8815
β : Type ?u.8864
n : Nat
P : α → Prop
f : (a : α) → P a → β
a✝ : α
l : Vector α n
a : α
m : a ∈ l
h : ∀ (b : α), b ∈ l ∨ b = a✝ → P b
⊢ P a

Proof state:
α : Type ?u.8815
β : Type ?u.8864
n : Nat
P : α → Prop
f : (a : α) → P a → β
a : α
l : Vector α n
h : ∀ (b : α), b ∈ l.push a → P b
⊢ a ∈ l.push a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem coe_rpow_of_nonneg (x : ℝ≥0) {y : ℝ} (h : 0 ≤ y) : ↑(x ^ y) = (x : ℝ≥0∞) ^ y

Proof state:
x : ℝ≥0
y : ℝ
h : 0 ≤ y
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
by_cases hx : x = 0

Result:
case pos
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ ↑(x ^ y) = ↑x ^ y

case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑(x ^ y) = ↑x ^ y

Proof state:
case pos.inl
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
simp [hx, H.symm]

Result:
no goals

Proof state:
case pos
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
rcases le_iff_eq_or_lt.1 h with (H | H)

Result:
case pos.inl
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ ↑(x ^ y) = ↑x ^ y

case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑(x ^ y) = ↑x ^ y

Proof state:
case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
exact coe_rpow_of_ne_zero hx _

Result:
no goals

Proof state:
case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem mul_div_mul_comm_of_dvd_dvd {a b c d : R} (hac : c ∣ a) (hbd : d ∣ b) :
    a * b / (c * d) = a / c * (b / d)

Proof state:
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
rcases eq_or_ne d 0 with (rfl | hd0)

Result:
case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)

case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Proof state:
case inr.inr.intro.intro
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)

Tactic:
rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
  mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
obtain ⟨k1, rfl⟩ := hac

Result:
case inr.inr.intro
R : Type u
inst✝ : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)

Proof state:
case inr.inr.intro
R : Type u
inst✝ : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)

Tactic:
obtain ⟨k2, rfl⟩ := hbd

Result:
case inr.inr.intro.intro
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc0)

Result:
case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)

case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)

Proof state:
case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma π_leftRightHomologyComparison'_ι :
    h₁.π ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.ι = h₁.i ≫ h₂.p

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.π ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.ι = h₁.i ≫ h₂.p

Tactic:
simp only [leftRightHomologyComparison'_eq_liftH,
  RightHomologyData.liftH_ι, LeftHomologyData.π_descH]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_modify_self (h : m.1.WF) {k : α} {f : β k → β k} :
    (m.modify k f).get? k = (m.get? k).map f

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : β k → β k
⊢ (m.modify k f).get? k = Option.map f (m.get? k)

Tactic:
simp_to_model [modify] using List.getValueCast?_modifyKey_self

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem SimpleFunc.integral_eq_sum (f : α →ₛ E) (hfi : Integrable f μ) :
    ∫ x, f x ∂μ = ∑ x ∈ f.range, ENNReal.toReal (μ (f ⁻¹' {x})) • x

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ setToSimpleFunc (weightedSMul μ) f = integral μ f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ ∫ (x : α), f x ∂μ = ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal • x

Tactic:
rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ setToSimpleFunc (weightedSMul μ) f = integral μ f
-- Mathlib/Order/Filter/Map.lean
theorem map_eq_bot_iff : map m f = ⊥ ↔ f = ⊥ :=
  ⟨by
    rw [← empty_mem_iff_bot, ← empty_mem_iff_bot]
    exact id, fun h => by simp only [h, map_bot]⟩

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : f = ⊥
⊢ map m f = ⊥

Tactic:
simp only [h, map_bot]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ map m f = ⊥ → f = ⊥

Tactic:
rw [← empty_mem_iff_bot, ← empty_mem_iff_bot]

Result:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → ∅ ∈ f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → ∅ ∈ f

Tactic:
exact id

Result:
no goals