harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_deriv_le_segment' {f' : ℝ → E} {C : ℝ}
    (hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x)
    (bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C) : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt f (f' x) (Ici x) x

Tactic:
exact (hf x <| Ico_subset_Icc_self hx).mono_of_mem_nhdsWithin (Icc_mem_nhdsGE_of_mem hx)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
refine
  norm_image_sub_le_of_norm_deriv_right_le_segment (fun x hx => (hf x hx).continuousWithinAt)
    (fun x hx => ?_) bound

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt f (f' x) (Ici x) x
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem add_powHalf_succ_self_eq_powHalf (n) : powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n

Proof state:
case h.right.right
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : (powHalf (n + 1) + powHalf (n + 1)).RightMoves), powHalf n ⧏ (powHalf (n + 1) + powHalf (n + 1)).moveRight j

Tactic:
rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt

Result:
case h.right.right.inl.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < (powHalf (n + 1) + powHalf (n + 1)).moveRight (Sum.inl PUnit.unit)

case h.right.right.inr.unit.h
n : ℕ
hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < (powHalf (n + 1) + powHalf (n + 1)).moveRight (Sum.inr PUnit.unit)
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem toZ_of_eq : toZ i0 i0 = 0

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ = 0

Tactic:
refine le_antisymm (Nat.find_le ?_) (zero_le _)

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ succ^[0] i0 = i0

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ toZ i0 i0 = 0

Tactic:
rw [toZ_of_ge le_rfl]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ ↑(Nat.find ⋯) = 0

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ ↑(Nat.find ⋯) = 0

Tactic:
norm_cast

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ = 0

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ succ^[0] i0 = i0

Tactic:
rw [Function.iterate_zero, id]

Result:
no goals
-- Mathlib/RingTheory/Etale/Kaehler.lean
lemma tensorCotangentInvFun_smul_mk
    [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
    (H : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) (x : Q.Ring) (y : P.ker) :
    tensorCotangentInvFun f halg H (x • .mk ⟨f.toRingHom y, (f.mapKer halg y).2⟩) =
      x • 1 ⊗ₜ .mk y

Proof state:
R S T : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) = x • 1 ⊗ₜ[S] Cotangent.mk y

Tactic:
trans tensorCotangentInvFun f halg H (.mk ((f.mapKer halg).liftBaseChange Q.Ring (x ⊗ₜ y)))

Result:
R S T : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) =
    (tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (x ⊗ₜ[P.Ring] y)))

R S T : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
⊢ (tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (x ⊗ₜ[P.Ring] y))) =
    x • 1 ⊗ₜ[S] Cotangent.mk y
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma _root_.MeasurableEmbedding.map_withDensity_rnDeriv (hf : MeasurableEmbedding f)
    (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] :
    (ν.withDensity (μ.rnDeriv ν)).map f = (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f))

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f (ν.withDensity (μ.rnDeriv ν)) = (map f ν).withDensity ((map f μ).rnDeriv (map f ν))

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ (map f (ν.withDensity (μ.rnDeriv ν))) s = ((map f ν).withDensity ((map f μ).rnDeriv (map f ν))) s

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ (map f (ν.withDensity (μ.rnDeriv ν))) s = ((map f ν).withDensity ((map f μ).rnDeriv (map f ν))) s

Tactic:
rw [hf.map_apply, withDensity_apply _ (hf.measurable hs), withDensity_apply _ hs,
  setLIntegral_map hs (Measure.measurable_rnDeriv _ _) hf.measurable]

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, (map f μ).rnDeriv (map f ν) (f x) ∂ν

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = (map f μ).rnDeriv (map f ν) (f x)

Tactic:
filter_upwards [hf.rnDeriv_map μ ν] with a ha _ using ha.symm

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, (map f μ).rnDeriv (map f ν) (f x) ∂ν

Tactic:
refine setLIntegral_congr_fun (hf.measurable hs) ?_

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = (map f μ).rnDeriv (map f ν) (f x)
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem toUniqueFactorizationMonoid (hR : HasUnitMulPowIrreducibleFactorization R) :
    UniqueFactorizationMonoid R :=
  let p := Classical.choose hR
  let spec := Classical.choose_spec hR
  UniqueFactorizationMonoid.of_exists_prime_factors fun x hx => by
    use Multiset.replicate (Classical.choose (spec.2 hx)) p
    constructor
    · intro q hq
      have hpq := Multiset.eq_of_mem_replicate hq
      rw [hpq]
      refine ⟨spec.1.ne_zero, spec.1.not_unit, ?_⟩
      intro a b h
      by_cases ha : a = 0
      · rw [ha]
        simp only [true_or, dvd_zero]
      obtain ⟨m, u, rfl⟩ := spec.2 ha
      rw [mul_assoc, mul_left_comm, Units.dvd_mul_left] at h
      rw [Units.dvd_mul_right]
      by_cases hm : m = 0
      · simp only [hm, one_mul, pow_zero] at h ⊢
        right
        exact h
      left
      obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
      rw [pow_succ']
      apply dvd_mul_of_dvd_left dvd_rfl _
    · rw [Multiset.prod_replicate]
      exact Classical.choose_spec (spec.2 hx)

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
h : p ∣ Classical.choose hR ^ m * b
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
⊢ p ∣ Classical.choose hR ^ m ∨ p ∣ b

Tactic:
simp only [hm, one_mul, pow_zero] at h ⊢

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
p : R := Classical.choose hR
spec : Irreducible (Classical.choose hR) ∧ ∀ {x : R}, x ≠ 0 → ∃ n, Associated (Classical.choose hR ^ n) x :=
  Classical.choose_spec hR
x : R
hx : x ≠ 0
q : R
hq : q ∈ Multiset.replicate (Classical.choose ⋯) p
hpq : q = p
b : R
m : ℕ
u : Rˣ
ha : ¬Classical.choose hR ^ m * ↑u = 0
hm : m = 0
h : p ∣ b
⊢ p ∣ 1 ∨ p ∣ b
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma norm_div_le_norm_div_add_norm_div (a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b c : E
⊢ ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

Tactic:
simpa only [dist_eq_norm_div] using dist_triangle a b c

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_iff_codisjoint : IsCoprime I J ↔ Codisjoint I J

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ ∃ a b, a * I + b * J = 1

Tactic:
refine ⟨1, 1, ?_⟩

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ 1 * I + 1 * J = 1

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) ↔ I ⊔ J = ⊤

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) → I ⊔ J = ⊤

case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I ⊔ J = ⊤ → ∃ a b, a * I + b * J = 1

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ 1 * I + 1 * J = 1

Tactic:
simpa only [one_eq_top, top_mul, Submodule.add_eq_sup]

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) → I ⊔ J = ⊤

Tactic:
rintro ⟨x, y, hxy⟩

Result:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ I ⊔ J = ⊤

Proof state:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ I ⊔ J

Tactic:
apply (show x * I + y * J ≤ I ⊔ J from
  sup_le (mul_le_left.trans le_sup_left) (mul_le_left.trans le_sup_right))

Result:
case mp.intro.intro.a
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ x * I + y * J

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I ⊔ J = ⊤ → ∃ a b, a * I + b * J = 1

Tactic:
intro h

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ ∃ a b, a * I + b * J = 1

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ Codisjoint I J

Tactic:
rw [IsCoprime, codisjoint_iff]

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) ↔ I ⊔ J = ⊤

Proof state:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ I ⊔ J = ⊤

Tactic:
rw [eq_top_iff_one]

Result:
case mp.intro.intro
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ I ⊔ J

Proof state:
case mp.intro.intro.a
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ x * I + y * J

Tactic:
rw [hxy]

Result:
case mp.intro.intro.a
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ 1

Proof state:
case mp.intro.intro.a
R : Type u
inst✝ : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ 1

Tactic:
simp only [one_eq_top, Submodule.mem_top]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem iSup_eq_adjoin {ι} (f : ι → IntermediateField F E) :
    ⨆ i, f i = adjoin F (⋃ i, f i : Set E)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Sort u_3
f : ι → IntermediateField F E
⊢ ⨆ i, f i = adjoin F (⋃ i, ↑(f i))

Tactic:
simp_rw [adjoin_iUnion, adjoin_self]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_singleton_neg (x : α) : (span {-x} : Ideal α) = span {x}

Proof state:
α : Type u
inst✝ : Ring α
x : α
⊢ span {-x} = span {x}

Tactic:
ext

Result:
case h
α : Type u
inst✝ : Ring α
x x✝ : α
⊢ x✝ ∈ span {-x} ↔ x✝ ∈ span {x}

Proof state:
case h
α : Type u
inst✝ : Ring α
x x✝ : α
⊢ x✝ ∈ span {-x} ↔ x✝ ∈ span {x}

Tactic:
simp only [mem_span_singleton']

Result:
case h
α : Type u
inst✝ : Ring α
x x✝ : α
⊢ (∃ a, a * -x = x✝) ↔ ∃ a, a * x = x✝

Proof state:
case h
α : Type u
inst✝ : Ring α
x x✝ : α
⊢ (∃ a, a * -x = x✝) ↔ ∃ a, a * x = x✝

Tactic:
exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem find?_toList (p : α → Bool) (as : Array α) :
    as.toList.find? p = as.find? p

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ List.find? p as.toList = find? p as

Tactic:
cases as

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ List.find? p { toList := toList✝ }.toList = find? p { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ List.find? p { toList := toList✝ }.toList = find? p { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
lemma exp_neg (x : EReal) : exp (-x) = (exp x)⁻¹

Proof state:
case h_bot

⊢ (-⊥).exp = ⊥.exp⁻¹

Tactic:
simp

Result:
no goals

Proof state:
x : EReal
⊢ (-x).exp = x.exp⁻¹

Tactic:
induction x

Result:
case h_bot

⊢ (-⊥).exp = ⊥.exp⁻¹

case h_real
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹

case h_top

⊢ (-⊤).exp = ⊤.exp⁻¹

Proof state:
case h_top

⊢ (-⊤).exp = ⊤.exp⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h_real
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹

Tactic:
rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
  Real.exp_neg]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem map_id : map (@id α) = id

Proof state:
α : Type u_1
⊢ map id = id

Tactic:
ext ⟨⟨x, y⟩⟩

Result:
case h.mk.mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ map id (Quot.mk (Rel α) (x, y)) = id (Quot.mk (Rel α) (x, y))

Proof state:
case h.mk.mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ map id (Quot.mk (Rel α) (x, y)) = id (Quot.mk (Rel α) (x, y))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightShift_units_smul (a n' : ℤ) (hn' : n' + a = n) (x : Rˣ) :
    (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : Rˣ
⊢ (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Tactic:
apply rightShift_smul

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem map_eval_pi (f : ∀ i, Filter (α i)) [∀ i, NeBot (f i)] (i : ι) :
    map (eval i) (pi f) = f i

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
⊢ map (eval i) (pi f) = f i

Tactic:
refine le_antisymm (tendsto_eval_pi f i) fun s hs => ?_

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : I.pi t ⊆ eval i ⁻¹' s
⊢ s ∈ f i

Tactic:
rw [← image_subset_iff] at hI

Result:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ s ∈ f i

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i

Tactic:
rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩

Result:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : I.pi t ⊆ eval i ⁻¹' s
⊢ s ∈ f i

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ s ∈ f i

Tactic:
refine mem_of_superset (htf i) ((subset_eval_image_pi ?_ _).trans hI)

Result:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ (I.pi t).Nonempty

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ (I.pi t).Nonempty

Tactic:
exact nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_go_length {arr : Array β} :
    length (mapIdx.go f l arr) = length l + arr.size

Proof state:
case cons
β : Type u_1
α✝ : Type u_2
f : Nat → α✝ → β
head✝ : α✝
tail✝ : List α✝
ih : ∀ {arr : Array β}, (mapIdx.go f tail✝ arr).length = tail✝.length + arr.size
arr : Array β
⊢ (mapIdx.go f (head✝ :: tail✝) arr).length = (head✝ :: tail✝).length + arr.size

Tactic:
simp only [mapIdx.go, ih, Array.size_push, Nat.add_succ, length_cons, Nat.add_comm]

Result:
no goals

Proof state:
β : Type u_1
α✝ : Type u_2
f : Nat → α✝ → β
l : List α✝
arr : Array β
⊢ (mapIdx.go f l arr).length = l.length + arr.size

Tactic:
induction l generalizing arr with
| nil => simp only [mapIdx.go, length_nil, Nat.zero_add]
| cons _ _ ih =>
  simp only [mapIdx.go, ih, Array.size_push, Nat.add_succ, length_cons, Nat.add_comm]

Result:
no goals

Proof state:
case nil
β : Type u_1
α✝ : Type u_2
f : Nat → α✝ → β
arr : Array β
⊢ (mapIdx.go f [] arr).length = [].length + arr.size

Tactic:
simp only [mapIdx.go, length_nil, Nat.zero_add]

Result:
no goals
-- Mathlib/Probability/StrongLaw.lean
theorem truncation_eq_of_nonneg {f : α → ℝ} {A : ℝ} (h : ∀ x, 0 ≤ f x) :
    truncation f A = indicator (Set.Ioc 0 A) id ∘ f

Proof state:
case h.inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
by_cases h'x : f x ≤ A

Result:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

case neg
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : ¬f x ≤ A
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Proof state:
case neg
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : ¬f x ≤ A
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
simp only [h'x, and_false]

Result:
no goals

Proof state:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
have : -A < f x := by linarith [h x]

Result:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
this : -A < f x
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
⊢ truncation f A = (Set.Ioc 0 A).indicator id ∘ f

Tactic:
ext x

Result:
case h
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Proof state:
case h.inr
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 = f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
simp only [truncation, indicator, hx, id, Function.comp_apply, ite_self]

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
rcases (h x).lt_or_eq with (hx | hx)

Result:
case h.inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

case h.inr
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 = f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Proof state:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
this : -A < f x
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
simp only [this, true_and]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
⊢ -A < f x

Tactic:
linarith [h x]

Result:
no goals

Proof state:
case h.inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
simp only [truncation, indicator, hx, Set.mem_Ioc, id, Function.comp_apply]

Result:
case h.inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0