harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem finset_sum_apply {m : MeasurableSpace α} (I : Finset ι) (μ : ι → Measure α) (s : Set α) :
    (∑ i ∈ I, μ i) s = ∑ i ∈ I, μ i s

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
s : Set α
⊢ (∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s

Tactic:
rw [coe_finset_sum, Finset.sum_apply]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem Finset.prod_fin_eq_prod_range [CommMonoid β] {n : ℕ} (c : Fin n → β) :
    ∏ i, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ x ∈ univ, c x = if h : ↑x < n then c ⟨↑x, h⟩ else 1

Tactic:
rintro ⟨i, hi⟩ _

Result:
case mk
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
a✝ : ⟨i, hi⟩ ∈ univ
⊢ c ⟨i, hi⟩ = if h : ↑⟨i, hi⟩ < n then c ⟨↑⟨i, hi⟩, h⟩ else 1

Proof state:
case mk
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
a✝ : ⟨i, hi⟩ ∈ univ
⊢ c ⟨i, hi⟩ = if h : ↑⟨i, hi⟩ < n then c ⟨↑⟨i, hi⟩, h⟩ else 1

Tactic:
simp only [hi, dif_pos]

Result:
no goals

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i : Fin n, c i = ∏ i ∈ range n, if h : i < n then c ⟨i, h⟩ else 1

Tactic:
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]

Result:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ x ∈ univ, c x = if h : ↑x < n then c ⟨↑x, h⟩ else 1
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@[simp]
lemma _root_.NonUnitalAlgHom.map_adjoin_singleton [IsScalarTower R B B] [SMulCommClass R B B]
    (f : F) (x : A) : map f (adjoin R {x}) = adjoin R {f x}

Proof state:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : NonUnitalNonAssocSemiring A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
x : A
⊢ map f (adjoin R {x}) = adjoin R {f x}

Tactic:
simp [NonUnitalAlgHom.map_adjoin]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma primeSpectrumProd_symm_inr (x) :
    (primeSpectrumProd R S).symm (.inr x) = comap (RingHom.snd R S) x

Proof state:
case asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum S
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal ↔ x✝ ∈ ((comap (RingHom.snd R S)) x).asIdeal

Tactic:
simp [Ideal.prod]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum S
⊢ (primeSpectrumProd R S).symm (Sum.inr x) = (comap (RingHom.snd R S)) x

Tactic:
ext

Result:
case asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum S
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal ↔ x✝ ∈ ((comap (RingHom.snd R S)) x).asIdeal
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[deprecated posPart_eq_self (since := "2024-11-18")]
lemma eq_posPart_iff (a : A) : a = a⁺ ↔ 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ a = a⁺ ↔ 0 ≤ a

Tactic:
rw [eq_comm, posPart_eq_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasDerivAt.cpow (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x)
    (h0 : f x ∈ slitPlane) : HasDerivAt (fun x => f x ^ g x)
      (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Proof state:
f g : ℂ → ℂ
f' g' x : ℂ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Tactic:
simpa only [aux] using (hf.hasFDerivAt.cpow hg h0).hasDerivAt

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma ιMapObj_D₁ (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : ComplexShape.π c₁ c₂ c₁₂ i = i₁₂) :
    K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) i i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' =
      K.d₁ c₁₂ i.1 i.2 i₁₂'

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
i : I₁ × I₂
h : c₁.π c₂ c₁₂ i = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.d₁ c₁₂ i.1 i.2 i₁₂'

Tactic:
simp [D₁]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.re (hf : Integrable f μ) : Integrable (fun x => RCLike.re (f x)) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (fun x => RCLike.re (f x)) 1 μ

Tactic:
exact hf.re

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : Integrable f μ
⊢ Integrable (fun x => RCLike.re (f x)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (fun x => RCLike.re (f x)) 1 μ
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma comap_surjective [Algebra k K] [Algebra.IsAlgebraic k K] :
    Function.Surjective (comap · (algebraMap k K)) := fun w ↦
  letI := w.embedding.toAlgebra
  ⟨mk (IsAlgClosed.lift (M := ℂ) (R := k)).toRingHom,
    by simp [this, comap_mk, RingHom.algebraMap_toAlgebra]⟩

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
w : InfinitePlace k
this : Algebra k ℂ := w.embedding.toAlgebra
⊢ (fun x => x.comap (algebraMap k K)) (mk IsAlgClosed.lift.toRingHom) = w

Tactic:
simp [this, comap_mk, RingHom.algebraMap_toAlgebra]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma div_lt_iff (h : 0 < c) (h' : c ≠ ⊤) :  b / c < a ↔ b < a * c

Proof state:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a

Tactic:
exact (strictMono_div_right_of_pos h h').lt_iff_lt

Result:
no goals

Proof state:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * (a / c) ↔ b < a * c

Tactic:
rw [EReal.mul_div c a c, mul_comm a c]

Result:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a

Proof state:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < a ↔ b < a * c

Tactic:
nth_rw 1 [← @mul_div_cancel a c (ne_bot_of_gt h) h' (ne_of_gt h)]

Result:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * (a / c) ↔ b < a * c
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
theorem ae_le_iff_absolutelyContinuous : ae μ ≤ ae ν ↔ μ ≪ ν :=
  ⟨fun h s => by
    rw [measure_zero_iff_ae_nmem, measure_zero_iff_ae_nmem]
    exact fun hs => h hs, fun h _ hs => h hs⟩

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s

Tactic:
exact fun hs => h hs

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ ν s = 0 → μ s = 0

Tactic:
rw [measure_zero_iff_ae_nmem, measure_zero_iff_ae_nmem]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s
-- Mathlib/Data/Multiset/Bind.lean
theorem add_bind : (s + t).bind f = s.bind f + t.bind f

Proof state:
α : Type u_1
β : Type v
s t : Multiset α
f : α → Multiset β
⊢ (s + t).bind f = s.bind f + t.bind f

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.get!_eq_getValue! [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    [Inhabited β] {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} :
    Const.get! m a = getValue! a (toListModel m.1.buckets)

Proof state:
α : Type u
β : Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : PartialEquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
m : Raw₀ α fun x => β
hm : Raw.WFImp m.val
a : α
⊢ get! m a = getValue! a (toListModel m.val.buckets)

Tactic:
rw [get!_eq_get!ₘ, get!ₘ_eq_getValue! hm]

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
    (map₂ f a b).map g = map₂ f' (b.map g') a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
β' : Type u_6
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' b) a

Tactic:
cases a <;> cases b <;> simp [h_antidistrib]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    getD m a fallback = (get? m a).getD fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
fallback : β
⊢ getD m a fallback = (get? m a).getD fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_eq_getD_get?

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_neg_sub_two (n : ℤ) : S R (-n - 2) = -S R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (-n - 2) = -S R n

Tactic:
simpa [sub_eq_add_neg, add_comm] using S_neg R (n + 2)

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
protected lemma Decidable.mul_lt_mul'' [PosMulMono M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀]
    [DecidableRel (α := M₀) (· ≤ ·)] (h1 : a < c) (h2 : b < d)
    (h3 : 0 ≤ a) (h4 : 0 ≤ b) : a * b < c * d :=
  h4.lt_or_eq_dec.elim (fun b0 ↦ mul_lt_mul h1 h2.le b0 <| h3.trans h1.le) fun b0 ↦ by
    rw [← b0, mul_zero]; exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)

Proof state:
M₀ : Type u_1
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d

Tactic:
exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ a * b < c * d

Tactic:
rw [← b0, mul_zero]

Result:
M₀ : Type u_1
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d
-- Mathlib/Algebra/Polynomial/Div.lean
theorem divByMonic_one (p : R[X]) : p /ₘ 1 = p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ p /ₘ 1 = p

Tactic:
conv_rhs => rw [← modByMonic_add_div p monic_one]; simp

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
theorem dfinsuppFamily_smul
    [Monoid S] [∀ p, DistribMulAction S (N p)] [∀ p, SMulCommClass R S (N p)]
    (s : S) (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    dfinsuppFamily (s • f) = s • dfinsuppFamily f

Proof state:
case H.h
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily (s • f)) x✝) i✝ = ((s • dfinsuppFamily f) x✝) i✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
⊢ dfinsuppFamily (s • f) = s • dfinsuppFamily f

Tactic:
ext

Result:
case H.h
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily (s • f)) x✝) i✝ = ((s • dfinsuppFamily f) x✝) i✝
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app (n : A) (X : C) :
    ((shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).hom.app X)⟦n⟧' =
    (shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).hom.app (X⟦n⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n : A
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n (-n) ⋯).hom.app X) =
    (shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((shiftFunctor C n).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_hom_app

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem foldl_pmap (l : Vector α n) {P : α → Prop} (f : (a : α) → P a → β)
  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x

Proof state:
α : Type u_1
n : Nat
β : Type u_2
γ : Type u_3
l : Vector α n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
g : γ → β → γ
x : γ
⊢ foldl g x (pmap f l H) = foldl (fun acc a => g acc (f a.val ⋯)) x l.attach

Tactic:
rw [pmap_eq_map_attach, foldl_map]

Result:
no goals
-- Mathlib/Combinatorics/Additive/CovBySMul.lean
@[to_additive (attr := simp)]
lemma CovBySMul.of_subset (hAB : A ⊆ B) : CovBySMul M 1 A B := ⟨1, by simpa⟩

Proof state:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
A B : Set X
hAB : A ⊆ B
⊢ ↑(#1) ≤ 1 ∧ A ⊆ ↑1 • B

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) :
    foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝ : Monad m
f : Fin n → α → m α
x : α
⊢ foldrM.loop n f ⟨0, ⋯⟩ x = pure x

Tactic:
rw [foldrM.loop]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem one_eq_top : (1 : Ideal R) = ⊤

Proof state:
R : Type u
inst✝ : Semiring R
⊢ 1 = ⊤

Tactic:
rw [Submodule.one_eq_span, ← Ideal.span, Ideal.span_singleton_one]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma monotoneOn_of_le_add_one (hs : s.OrdConnected) :
    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s

Tactic:
simpa [Order.succ_eq_add_one] using monotoneOn_of_le_succ hs (f := f)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pushoutIsoUnopPullback_inl_hom {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] :
    pushout.inl _ _ ≫ (pushoutIsoUnopPullback f g).hom = (pullback.fst f.op g.op).unop :=
  (IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _).trans (by simp)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (PullbackCone.unop (limit.cone (cospan f.op g.op))).ι.app WalkingSpan.left = (pullback.fst f.op g.op).unop

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem rootSet_X_pow [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) :
    (X ^ n : R[X]).rootSet S = {0}

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ (X ^ n).rootSet S = {0}

Tactic:
rw [← one_mul (X ^ n : R[X]), ← C_1, rootSet_C_mul_X_pow hn]

Result:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ 1 ≠ 0

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.or_beq_zero_iff (a b : BitVec w) : (a ||| b == 0#w) = (a == 0#w && b == 0#w)

Proof state:
w : Nat
a b : BitVec w
⊢ (a ||| b == 0#w) = true ↔ (a == 0#w && b == 0#w) = true

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
a b : BitVec w
⊢ (a ||| b == 0#w) = (a == 0#w && b == 0#w)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b : BitVec w
⊢ (a ||| b == 0#w) = true ↔ (a == 0#w && b == 0#w) = true
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem vars_neg : (-p).vars = p.vars

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (-p).vars = p.vars

Tactic:
simp [vars, degrees_neg]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_one_iff (q : ℕ) [ExpChar F q] (hm : f.Monic) :
    f.natSepDegree = 1 ↔ ∃ (m n : ℕ) (y : F), m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
⊢ f.natSepDegree = 1 ↔ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨m, n, y, hm, h⟩ ↦ ?_⟩

Result:
case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ f.natSepDegree = 1

Proof state:
case refine_1.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
h✝ : f.natSepDegree = 1
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
exact ⟨m, n, y, hm, h⟩

Result:
no goals

Proof state:
case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

Tactic:
obtain ⟨m, n, y, hm, -, h⟩ := hm.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one q h

Result:
case refine_1.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
h✝ : f.natSepDegree = 1
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ f.natSepDegree = 1

Tactic:
simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]

Result:
no goals
-- Mathlib/Algebra/Lie/Abelian.lean
theorem isFaithful_self_iff : LieModule.IsFaithful R L L ↔ center R L = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ LieModule.IsFaithful R L L ↔ center R L = ⊥

Tactic:
rw [LieModule.isFaithful_iff_ker_eq_bot, self_module_ker_eq_center]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Cast.lean
lemma cast_natAbs : (n.natAbs : R) = |n|

Proof state:
case negSucc
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : ℕ
⊢ ↑-[a✝+1].natAbs = ↑|-[a✝+1]|

Tactic:
rw [abs_eq_natAbs, natAbs_negSucc, cast_succ, cast_natCast, cast_succ]

Result:
no goals

Proof state:
case ofNat
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : ℕ
⊢ ↑(ofNat a✝).natAbs = ↑|ofNat a✝|

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
n : ℤ
⊢ ↑n.natAbs = ↑|n|

Tactic:
cases n

Result:
case ofNat
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : ℕ
⊢ ↑(ofNat a✝).natAbs = ↑|ofNat a✝|

case negSucc
R : Type u_1
inst✝ : LinearOrderedRing R
a✝ : ℕ
⊢ ↑-[a✝+1].natAbs = ↑|-[a✝+1]|
-- Mathlib/Data/Set/Sigma.lean
theorem sigma_diff_sigma : s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁ :=
  ext fun x ↦ by
    by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ x.1 <;> simp [*, ← imp_iff_or_not]

Proof state:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ x.1 <;> simp [*, ← imp_iff_or_not]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_le_lowerCrossingTime :
    upperCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N n ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N n ω

Tactic:
simp only [lowerCrossingTime, le_hitting upperCrossingTime_le ω]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) : Monotone fun x : ℝ≥0∞ => x ^ z :=
  h.eq_or_lt.elim (fun h0 => h0 ▸ by simp only [rpow_zero, monotone_const]) fun h0 =>
    (strictMono_rpow_of_pos h0).monotone

Proof state:
z : ℝ
h : 0 ≤ z
h0 : 0 = z
⊢ Monotone fun x => x ^ 0

Tactic:
simp only [rpow_zero, monotone_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_add_const (l : Array α) (a b : Nat) :
    l.foldr (fun _ x => x + a) b = b + a * l.size

Proof state:
α : Type u_1
l : Array α
a b : Nat
⊢ foldr (fun x x => x + a) b l = b + a * l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ foldr (fun x x => x + a) b { toList := l } = b + a * { toList := l }.size

Proof state:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ foldr (fun x x => x + a) b { toList := l } = b + a * { toList := l }.size

Tactic:
simp

Result:
no goals