harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
/-- A function is integrable for the counting measure iff its norm is summable. -/
lemma integrable_count_iff :
    Integrable f Measure.count ↔ Summable (‖f ·‖)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEStronglyMeasurable f Measure.count

Tactic:
refine aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ AEMeasurable f Measure.count

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
⊢ {x | 0 x ≠ f x}.Countable

Tactic:
simpa only [Ne, Pi.zero_apply, eq_comm, Function.support] using hs'

Result:
no goals

Proof state:
case refine_2.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
this✝ : MeasurableSpace β := borel β
this : BorelSpace β
hg : 0 ∈ f '' univ
⊢ 0 ∈ f '' Function.support f ∪ {0}

Tactic:
exact Or.inr (mem_singleton _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
⊢ AEStronglyMeasurable f Measure.count

Tactic:
have hs' : (Function.support f).Countable := by
  simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero]
    using hs.countable_support

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
hs : Summable fun x => ‖f x‖
hs' : (Function.support f).Countable
⊢ AEStronglyMeasurable f Measure.count
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem bot_or_nontrivial (H : Subgroup G) : H = ⊥ ∨ Nontrivial H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : Nontrivial ↥H ↔ H ≠ ⊥
⊢ H = ⊥ ∨ Nontrivial ↥H

Tactic:
tauto

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ Nontrivial ↥H

Tactic:
have := nontrivial_iff_ne_bot H

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : Nontrivial ↥H ↔ H ≠ ⊥
⊢ H = ⊥ ∨ Nontrivial ↥H
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSumSq.prod [CommSemiring R] {ι : Type*} {I : Finset ι} {x : ι → R}
    (hx : ∀ i ∈ I, IsSumSq <| x i) : IsSumSq (∏ i ∈ I, x i)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSumSq (x i)
⊢ IsSumSq (∏ i ∈ I, x i)

Tactic:
simpa using prod_mem (S := Subsemiring.sumSq R) (by simpa)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
I : Finset ι
x : ι → R
hx : ∀ i ∈ I, IsSumSq (x i)
⊢ ∀ c ∈ I, x c ∈ Subsemiring.sumSq R

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem symm_comp_self (e : M₁ ≃SL[σ₁₂] M₂) : (e.symm : M₂ → M₁) ∘ (e : M₁ → M₂) = id

Proof state:
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
ext x

Result:
case h
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₁
⊢ (⇑e.symm ∘ ⇑e) x = id x

Proof state:
case h
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₁
⊢ (⇑e.symm ∘ ⇑e) x = id x

Tactic:
exact symm_apply_apply e x

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem degree_hermite (n : ℕ) : (hermite n).degree = n

Proof state:
case pn
n : ℕ
⊢ (hermite n).degree ≤ ↑n

Tactic:
simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]

Result:
case pn
n : ℕ
⊢ ∀ (m : ℕ), n < m → (hermite n).coeff m = 0

Proof state:
case pn
n m : ℕ
hnm : n < m
⊢ (hermite n).coeff m = 0

Tactic:
exact coeff_hermite_of_lt hnm

Result:
no goals

Proof state:
case pn
n : ℕ
⊢ ∀ (m : ℕ), n < m → (hermite n).coeff m = 0

Tactic:
rintro m hnm

Result:
case pn
n m : ℕ
hnm : n < m
⊢ (hermite n).coeff m = 0

Proof state:
case p1
n : ℕ
⊢ (hermite n).coeff n ≠ 0

Tactic:
simp [coeff_hermite_self n]

Result:
no goals

Proof state:
n : ℕ
⊢ (hermite n).degree = ↑n

Tactic:
rw [degree_eq_of_le_of_coeff_ne_zero]

Result:
case pn
n : ℕ
⊢ (hermite n).degree ≤ ↑n

case p1
n : ℕ
⊢ (hermite n).coeff n ≠ 0
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma isNilpotent_toEnd_sub_algebraMap [IsNoetherian R M] (χ : L → R) (x : L) :
    _root_.IsNilpotent <| toEnd R L (genWeightSpace M χ) x - algebraMap R _ (χ x)

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
⊢ ((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x)) ^ k = 0

Tactic:
ext ⟨m, hm⟩

Result:
case h.h.mk.a
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
this :
  (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯
k : ℕ
hk : ↑(genWeightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
m : M
hm : m ∈ genWeightSpace M χ
⊢ ↑((((toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x)) ^ k) ⟨m, hm⟩) =
    ↑(0 ⟨m, hm⟩)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
χ : L → R
x : L
⊢ (toEnd R L ↥(genWeightSpace M χ)) x - (algebraMap R (Module.End R ↥(genWeightSpace M χ))) (χ x) =
    LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/EssentiallySmall.lean
theorem essentiallySmall_congr {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
    (e : C ≌ D) : EssentiallySmall.{w} C ↔ EssentiallySmall.{w} D

Proof state:
case mpr.mk.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall.{w, v, u} C

Tactic:
exact EssentiallySmall.mk' (e.trans f)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v, u} C ↔ EssentiallySmall.{w, v', u'} D

Tactic:
fconstructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v, u} C → EssentiallySmall.{w, v', u'} D

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v', u'} D → EssentiallySmall.{w, v, u} C

Proof state:
case mp.mk.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall.{w, v', u'} D

Tactic:
exact EssentiallySmall.mk' (e.symm.trans f)

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v, u} C → EssentiallySmall.{w, v', u'} D

Tactic:
rintro ⟨S, 𝒮, ⟨f⟩⟩

Result:
case mp.mk.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : C ≌ S
⊢ EssentiallySmall.{w, v', u'} D

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v', u'} D → EssentiallySmall.{w, v, u} C

Tactic:
rintro ⟨S, 𝒮, ⟨f⟩⟩

Result:
case mpr.mk.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
S : Type w
𝒮 : SmallCategory S
f : D ≌ S
⊢ EssentiallySmall.{w, v, u} C
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma pairwiseDisjoint_disjointOfUnion_of_mem (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
    PairwiseDisjoint (hC.disjointOfUnion hJ j : Set (Set α)) id

Proof state:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
hj : j ∈ J
⊢ ↑(hC.disjointOfUnion hJ j) ⊆ ⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x)

Tactic:
exact subset_iUnion₂_of_subset j hj fun ⦃a⦄ a ↦ a

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
hj : j ∈ J
⊢ (↑(hC.disjointOfUnion hJ j)).PairwiseDisjoint id

Tactic:
apply PairwiseDisjoint.subset (hC.pairwiseDisjoint_biUnion_disjointOfUnion hJ)

Result:
α : Type u_1
C : Set (Set α)
j : Set α
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
hj : j ∈ J
⊢ ↑(hC.disjointOfUnion hJ j) ⊆ ⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x)
-- Mathlib/Algebra/Group/Equiv/Defs.lean
@[to_additive (attr := simp)]
lemma coe_monoidHom_comp_coe_monoidHom_symm (e : M ≃* N) :
    (e : M →* N).comp e.symm = MonoidHom.id _

Proof state:
case h
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : N
⊢ ((↑e).comp ↑e.symm) x✝ = (MonoidHom.id N) x✝

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
⊢ (↑e).comp ↑e.symm = MonoidHom.id N

Tactic:
ext

Result:
case h
M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : N
⊢ ((↑e).comp ↑e.symm) x✝ = (MonoidHom.id N) x✝
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem formPerm_eq_formPerm_iff {α : Type*} [DecidableEq α] {s s' : Cycle α} {hs : s.Nodup}
    {hs' : s'.Nodup} :
    s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.Subsingleton ∧ s'.Subsingleton

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
hs : s.Nodup
hs' : s'.Nodup
⊢ s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1

Tactic:
revert s s'

Result:
α : Type u_2
inst✝ : DecidableEq α
⊢ ∀ {s s' : Cycle α} {hs : s.Nodup} {hs' : s'.Nodup},
    s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
hs : s.Nodup
hs' : s'.Nodup
⊢ s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.Subsingleton ∧ s'.Subsingleton

Tactic:
rw [Cycle.length_subsingleton_iff, Cycle.length_subsingleton_iff]

Result:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
hs : s.Nodup
hs' : s'.Nodup
⊢ s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)},
    formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
      Quotient.mk'' a₁ = Quotient.mk'' a₂ ∨ length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1

Tactic:
intro l l' hl hl'

Result:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hl : Nodup (Quotient.mk'' l)
hl' : Nodup (Quotient.mk'' l')
⊢ formPerm (Quotient.mk'' l) hl = formPerm (Quotient.mk'' l') hl' ↔
    Quotient.mk'' l = Quotient.mk'' l' ∨ length (Quotient.mk'' l) ≤ 1 ∧ length (Quotient.mk'' l') ≤ 1

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ {hs : s.Nodup} {hs' : s'.Nodup}, s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1

Tactic:
apply @Quotient.inductionOn₂' _ _ _ _ _ s s'

Result:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)},
    formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
      Quotient.mk'' a₁ = Quotient.mk'' a₂ ∨ length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
l l' : List α
hl : Nodup (Quotient.mk'' l)
hl' : Nodup (Quotient.mk'' l')
⊢ formPerm (Quotient.mk'' l) hl = formPerm (Quotient.mk'' l') hl' ↔
    Quotient.mk'' l = Quotient.mk'' l' ∨ length (Quotient.mk'' l) ≤ 1 ∧ length (Quotient.mk'' l') ≤ 1

Tactic:
simpa using formPerm_eq_formPerm_iff hl hl'

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
⊢ ∀ {s s' : Cycle α} {hs : s.Nodup} {hs' : s'.Nodup},
    s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1

Tactic:
intro s s'

Result:
α : Type u_2
inst✝ : DecidableEq α
s s' : Cycle α
⊢ ∀ {hs : s.Nodup} {hs' : s'.Nodup}, s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem length_dropUntil_le {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.dropUntil u h).length ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.dropUntil u h).length + (p.takeUntil u h).length = p.length
⊢ (p.dropUntil u h).length ≤ p.length

Tactic:
exact Nat.le.intro this

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.dropUntil u h).length ≤ p.length

Tactic:
rw [length_append, add_comm] at this

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.dropUntil u h).length + (p.takeUntil u h).length = p.length
⊢ (p.dropUntil u h).length ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.dropUntil u h).length ≤ p.length

Tactic:
have := congr_arg Walk.length (p.take_spec h)

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.dropUntil u h).length ≤ p.length
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma isColimitLocallyConstantPresheafDiagram_desc_apply (S : LightProfinite)
    (s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X))
    (n : ℕ) (f : LocallyConstant (S.diagram.obj ⟨n⟩) X) :
    (isColimitLocallyConstantPresheafDiagram X S).desc s (f.comap (S.asLimitCone.π.app ⟨n⟩).hom) =
      s.ι.app n f

Proof state:
X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X
⊢ (isColimitLocallyConstantPresheafDiagram X S).desc s
      (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n))) f) =
    s.ι.app n f

Tactic:
change ((((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n) ≫
  (isColimitLocallyConstantPresheafDiagram X S).desc s) _ = _

Result:
X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X
⊢ (((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n ≫
        (isColimitLocallyConstantPresheafDiagram X S).desc s)
      f =
    s.ι.app n f

Proof state:
X : Type u
S : LightProfinite
s : Cocone (S.diagram.rightOp ⋙ locallyConstantPresheaf X)
n : ℕ
f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X
⊢ (((locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone)).ι.app n ≫
        (isColimitLocallyConstantPresheafDiagram X S).desc s)
      f =
    s.ι.app n f

Tactic:
rw [(isColimitLocallyConstantPresheafDiagram X S).fac]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_inl_union_inr_eq_prod (s) (t) :
    adjoin R (LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1})) =
      (adjoin R s).prod (adjoin R t)

Proof state:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
⊢ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) ≤ (adjoin R s).prod (adjoin R t)

Tactic:
simp only [adjoin_le_iff, Set.insert_subset_iff, Subalgebra.zero_mem, Subalgebra.one_mem,
  subset_adjoin,Set.union_subset_iff,
  LinearMap.coe_inl, Set.mk_preimage_prod_right, Set.image_subset_iff, SetLike.mem_coe,
  Set.mk_preimage_prod_left, LinearMap.coe_inr, and_self_iff, Set.union_singleton,
  Subalgebra.coe_prod]

Result:
no goals

Proof state:
case a.mk.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
Hb : (0, b) ∈ P
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
simpa [P] using Subalgebra.add_mem _ Ha Hb

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_sigma {β : Type w} (f : β → C) [HasCoproduct f] :
    IsSeparator (∐ f) ↔ IsSeparating (Set.range f)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
⊢ IsSeparator (∐ f) ↔ IsSeparating (Set.range f)

Tactic:
refine ⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h (colimit.isColimit _)⟩

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ u = v

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
b : Discrete β
⊢ colimit.ι (Discrete.functor f) b ≫ g ≫ u = colimit.ι (Discrete.functor f) b ≫ g ≫ v

Tactic:
simpa using huv (f b.as) (by simp) (colimit.ι (Discrete.functor f) _ ≫ g)

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
b : Discrete β
⊢ f b.as ∈ Set.range f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ u = v

Tactic:
refine h.def _ _ fun g => colimit.hom_ext fun b => ?_

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
b : Discrete β
⊢ colimit.ι (Discrete.functor f) b ≫ g ≫ u = colimit.ι (Discrete.functor f) b ≫ g ≫ v
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem le_trim (hm : m ≤ m0) : μ s ≤ μ.trim hm s

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ μ s ≤ (μ.trim hm) s

Tactic:
simp_rw [Measure.trim]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ μ s ≤ (μ.toMeasure ⋯) s

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ μ s ≤ (μ.toMeasure ⋯) s

Tactic:
exact @le_toMeasure_apply _ m _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
lemma measure_null_iff_singleton (hs : s.Countable) : μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : Set α
hs : s.Countable
⊢ μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0

Tactic:
rw [← measure_biUnion_null_iff hs, biUnion_of_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (map f arr).toList = List.map f arr.toList

Tactic:
rw [map, mapM_eq_foldlM]

Result:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (foldlM (fun bs a => bs.push <$> f a) #[] arr).run.toList = List.map f arr.toList

Proof state:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
H :
  ∀ (l : List α) (arr : Array β),
    List.foldl (fun bs a => bs.push (f a)) arr l = { toList := arr.toList ++ List.map f l }
⊢ (List.foldl (fun bs a => bs.push (f a)) #[] arr.toList).toList = List.map f arr.toList

Tactic:
simp [H]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (List.foldl (fun bs a => bs.push (f a)) #[] arr.toList).toList = List.map f arr.toList

Tactic:
have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
  induction l generalizing arr <;> simp [*]

Result:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
H :
  ∀ (l : List α) (arr : Array β),
    List.foldl (fun bs a => bs.push (f a)) arr l = { toList := arr.toList ++ List.map f l }
⊢ (List.foldl (fun bs a => bs.push (f a)) #[] arr.toList).toList = List.map f arr.toList

Proof state:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (foldlM (fun bs a => bs.push <$> f a) #[] arr).run.toList = List.map f arr.toList

Tactic:
apply congrArg toList (foldl_toList (fun bs a => push bs (f a)) #[] arr).symm |>.trans

Result:
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (List.foldl (fun bs a => bs.push (f a)) #[] arr.toList).toList = List.map f arr.toList

Proof state:
α : Type u_1
β : Type u_2
f : α → β
arr✝ : Array α
l : List α
arr : Array β
⊢ List.foldl (fun bs a => bs.push (f a)) arr l = { toList := arr.toList ++ List.map f l }

Tactic:
induction l generalizing arr <;> simp [*]

Result:
no goals