harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_triangle (a b c : ℍ) : dist a c ≤ dist a b + dist b c

Proof state:
a b c : ℍ
⊢ ¬(↑b).im = 0

Tactic:
exact b.im_ne_zero

Result:
no goals

Proof state:
a b c : ℍ
⊢ dist a c ≤ dist a b + dist b c

Tactic:
rw [dist_le_iff_le_sinh, sinh_half_dist_add_dist, div_mul_eq_div_div _ _ (dist _ _), le_div_iff₀,
  div_mul_eq_mul_div]

Result:
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))

a b c : ℍ
⊢ 0 < dist (↑b) ((starRingEnd ℂ) ↑b)

Proof state:
case hab
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) ≤
    dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)

Tactic:
exact EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ))

Result:
no goals

Proof state:
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))

Tactic:
gcongr

Result:
case hab
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) ≤
    dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)

Proof state:
a b c : ℍ
⊢ 0 < dist (↑b) ((starRingEnd ℂ) ↑b)

Tactic:
rw [dist_comm, dist_pos, Ne, Complex.conj_eq_iff_im]

Result:
a b c : ℍ
⊢ ¬(↑b).im = 0
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma zpow_natCast_sub_natCast₀ (ha : a ≠ 0) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℕ
⊢ a ^ (↑m - ↑n) = a ^ m / a ^ n

Tactic:
simpa using zpow_sub₀ ha m n

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasToLpTrimLie_symm_toLp [one_le_p : Fact (1 ≤ p)] [NormedSpace ℝ F] (hm : m ≤ m0)
    (f : α → F) (hf : MemLp f p (μ.trim hm)) :
    ((lpMeasToLpTrimLie F ℝ p μ hm).symm (hf.toLp f) : Lp F p μ) =
      (memLp_of_memLp_trim hm hf).toLp f

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) = MemLp.toLp f ⋯

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ ↑↑↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) =ᶠ[ae μ] ↑↑(MemLp.toLp f ⋯)

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ ↑↑↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) =ᶠ[ae μ] ↑↑(MemLp.toLp f ⋯)

Tactic:
refine (lpTrimToLpMeas_ae_eq hm _).trans ?_

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ ↑↑(MemLp.toLp f hf) =ᶠ[ae μ] ↑↑(MemLp.toLp f ⋯)

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
⊢ ↑↑(MemLp.toLp f hf) =ᶠ[ae μ] ↑↑(MemLp.toLp f ⋯)

Tactic:
exact (ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp hf)).trans (MemLp.coeFn_toLp _).symm

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_one_iff' {x y : ℝ} (hx : 0 ≤ x) (hy : 0 < y) :
    x ^ y < 1 ↔ x < 1

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 < y
⊢ x ^ y < 1 ↔ x < 1

Tactic:
rw [← Real.rpow_lt_rpow_iff hx zero_le_one hy, Real.one_rpow]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left
    (hab : IntervalIntegrable f μ a b) (hmeas : StronglyMeasurableAtFilter f la' μ)
    (hf : Tendsto f (la' ⊓ ae μ) (𝓝 c)) (hu : Tendsto u lt la) (hv : Tendsto v lt la) :
    (fun t => ((∫ x in v t..b, f x ∂μ) - ∫ x in u t..b, f x ∂μ) + ∫ _ in u t..v t, c ∂μ) =o[lt]
      fun t => ∫ _ in u t..v t, (1 : ℝ) ∂μ

Proof state:
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
c : E
la la' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : FTCFilter a la la'
inst✝ : IsLocallyFiniteMeasure μ
hab : IntervalIntegrable f μ a b
hmeas : StronglyMeasurableAtFilter f la' μ
hf : Tendsto f (la' ⊓ ae μ) (𝓝 c)
hu : Tendsto u lt la
hv : Tendsto v lt la
⊢ (fun t => ∫ (x : ℝ) in v t..b, f x ∂μ - ∫ (x : ℝ) in u t..b, f x ∂μ + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
    ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
simpa using
  measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab hmeas
    stronglyMeasurableAt_bot hf ((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hu
    hv (tendsto_const_pure : Tendsto _ _ (pure b)) tendsto_const_pure

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem two_lt_card_iff : 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Proof state:
α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three,
  ← exists_and_left, exists_comm (α := Finset α)]

Result:
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Proof state:
case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
rintro ⟨a, b, c, t, hsub, hab, hac, hbc, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Proof state:
α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ {a, b, c} ⊆ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ {a, b, c} = {a, b, c}

Tactic:
simp_all [insert_subset_iff]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Tactic:
exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
constructor

Result:
case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Proof state:
case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Tactic:
rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Proof state:
α : Type u_1
s : Finset α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hsub : {a, b, c} ⊆ s
⊢ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_all [insert_subset_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Char/Lemmas.lean
theorem ofNat_toNat (c : Char) : Char.ofNat c.toNat = c

Proof state:
c : Char
⊢ ofNat c.toNat = c

Tactic:
rw [Char.ofNat, dif_pos]

Result:
c : Char
⊢ ofNatAux c.toNat ?hc = c

case hc
c : Char
⊢ c.toNat.isValidChar

Proof state:
c : Char
⊢ ofNatAux c.toNat ?hc = c

case hc
c : Char
⊢ c.toNat.isValidChar

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ENNReal/Operations.lean
theorem toNNReal_sum {s : Finset α} {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, f a ≠ ∞) :
    ENNReal.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, ENNReal.toNNReal (f a)

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

Tactic:
rw [← coe_inj, coe_toNNReal, coe_finset_sum, sum_congr rfl]

Result:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∀ x ∈ s, f x = ↑(f x).toNNReal

α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ a ∈ s, f a ≠ ⊤

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
x : α
hx : x ∈ s
⊢ f x = ↑(f x).toNNReal

Tactic:
exact (coe_toNNReal (hf x hx)).symm

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∀ x ∈ s, f x = ↑(f x).toNNReal

Tactic:
intro x hx

Result:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
x : α
hx : x ∈ s
⊢ f x = ↑(f x).toNNReal

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ ∑ a ∈ s, f a ≠ ⊤

Tactic:
exact sum_ne_top.2 hf

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem algebraMap_apply {R : Type*} [CommSemiring R] [Algebra R K[X]] (x : R) :
    algebraMap R (RatFunc K) x = algebraMap _ _ (algebraMap R K[X] x) / algebraMap K[X] _ 1

Proof state:
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ (algebraMap R (RatFunc K)) x = RatFunc.mk ((algebraMap R K[X]) x) 1

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ (algebraMap R (RatFunc K)) x = (algebraMap K[X] (RatFunc K)) ((algebraMap R K[X]) x) / (algebraMap K[X] (RatFunc K)) 1

Tactic:
rw [← mk_eq_div]

Result:
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
x : R
⊢ (algebraMap R (RatFunc K)) x = RatFunc.mk ((algebraMap R K[X]) x) 1
-- Mathlib/MeasureTheory/Group/LIntegral.lean
theorem lintegral_mul_left_eq_self [IsMulLeftInvariant μ] (f : G → ℝ≥0∞) (g : G) :
    (∫⁻ x, f (g * x) ∂μ) = ∫⁻ x, f x ∂μ

Proof state:
case h.e'_3.h.e'_3
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ μ = map (⇑(MeasurableEquiv.mulLeft g)) μ

Tactic:
simp [map_mul_left_eq_self μ g]

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
convert (lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm

Result:
case h.e'_3.h.e'_3
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ μ = map (⇑(MeasurableEquiv.mulLeft g)) μ
-- Mathlib/Algebra/Quaternion.lean
theorem mul_imI : (a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ :=
  (QuaternionAlgebra.mul_imI a b).trans <| by ring

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imI + a.imI * b.re + 0 * a.imI * b.imI - -1 * a.imJ * b.imK + -1 * a.imK * b.imJ =
    a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma finset_sup'_nhds_apply [SemilatticeSup L] [ContinuousSup L]
    (hne : s.Nonempty) (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
    Tendsto (fun a ↦ s.sup' hne (f · a)) l (𝓝 (s.sup' hne g))

Proof state:
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun a => s.sup' hne fun x => f x a) l (𝓝 (s.sup' hne g))

Tactic:
simpa only [← Finset.sup'_apply] using finset_sup'_nhds hne hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_range' {start size step : Nat} {i : Nat} :
    (Array.range' start size step)[i]? = if i < size then some (start + step * i) else none

Proof state:
start size step i : Nat
⊢ (range' start size step)[i]? = if i < size then some (start + step * i) else none

Tactic:
simp [getElem?_def, getElem_range']

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_zmod_eq_zero_iff_of_le {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZMod m) :
    (cast a : ZMod n) = 0 ↔ a = 0

Proof state:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = cast 0 ↔ a = 0

Tactic:
exact Injective.eq_iff' (cast_injective_of_le h) rfl

Result:
no goals

Proof state:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = 0 ↔ a = 0

Tactic:
rw [← ZMod.cast_zero (n := m)]

Result:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = cast 0 ↔ a = 0
-- Mathlib/Algebra/Group/Subsemigroup/Basic.lean
theorem dense_induction {p : M → Prop} (s : Set M) (closure : closure s = ⊤)
    (mem : ∀ x ∈ s, p x) (mul : ∀ x y, p x → p y → p (x * y)) (x : M) :
    p x

Proof state:
case mul
M : Type u_1
inst✝ : Mul M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x x✝ y✝ : M
hx✝ : x✝ ∈ Subsemigroup.closure s
hy✝ : y✝ ∈ Subsemigroup.closure s
h₁ : p x✝
h₂ : p y✝
⊢ p (x✝ * y✝)

Tactic:
exact mul _ _ h₁ h₂

Result:
no goals

Proof state:
case mem
M : Type u_1
inst✝ : Mul M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x x✝ : M
h : x✝ ∈ s
⊢ p x✝

Tactic:
exact mem _ h

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with
| mem _ h => exact mem _ h
| mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

Result:
no goals
-- Mathlib/Topology/Order/IsLocallyClosed.lean
theorem isLocallyClosed_Ico [LinearOrder X] [ClosedIciTopology X] :
    IsLocallyClosed (Set.Ico a b)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Ico a b)

Tactic:
rw [← Set.Iio_inter_Ici]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio b ∩ Set.Ici a)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio b ∩ Set.Ici a)

Tactic:
exact isLocallyClosed_Iio.inter isLocallyClosed_Ici

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- The trivial zero at `s = -2` of the zeta function gives that `F (-2) = 0`.
This is used later to obtain a contradction. -/
private lemma F_neg_two (B : BadChar N) : B.F (-2 : ℝ) = 0

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
this : riemannZeta (-2) = 0
⊢ B.F ↑(-2) = 0

Tactic:
rw [F, ofReal_neg, ofReal_ofNat, Function.update_of_ne (mod_cast (by omega : (-2 : ℤ) ≠ 1)),
  this, zero_mul]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
this : riemannZeta (-2 * (↑0 + 1)) = 0
⊢ B.F ↑(-2) = 0

Tactic:
rw [Nat.cast_zero, zero_add, mul_one] at this

Result:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
this : riemannZeta (-2) = 0
⊢ B.F ↑(-2) = 0

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
this : riemannZeta (-2) = 0
⊢ -2 ≠ 1

Tactic:
omega

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
⊢ B.F ↑(-2) = 0

Tactic:
have := riemannZeta_neg_two_mul_nat_add_one 0

Result:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
this : riemannZeta (-2 * (↑0 + 1)) = 0
⊢ B.F ↑(-2) = 0
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma oddKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : oddKernel a x = 0

Proof state:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ oddKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with | H a' =>
rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add,
  mul_zero, mul_zero] <;>
simpa

Result:
no goals

Proof state:
case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ oddKernel (↑a') x = 0

Tactic:
rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add,
  mul_zero, mul_zero] <;>
simpa

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
theorem FiberBundle.chartedSpace_chartAt (x : TotalSpace F E) :
    chartAt (ModelProd HB F) x =
      (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ
        (chartAt HB x.proj).prod (PartialHomeomorph.refl F)

Proof state:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ chartAt (ModelProd HB F) x =
    (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (PartialHomeomorph.refl F)

Tactic:
dsimp only [chartAt_comp, prodChartedSpace_chartAt, FiberBundle.chartedSpace'_chartAt,
  chartAt_self_eq]

Result:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ
      (chartAt HB (↑(trivializationAt F E x.proj).toPartialHomeomorph x).1).prod (PartialHomeomorph.refl F) =
    (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (PartialHomeomorph.refl F)

Proof state:
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ
      (chartAt HB (↑(trivializationAt F E x.proj).toPartialHomeomorph x).1).prod (PartialHomeomorph.refl F) =
    (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (PartialHomeomorph.refl F)

Tactic:
rw [Trivialization.coe_coe, Trivialization.coe_fst' _ (mem_baseSet_trivializationAt F E x.proj)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_filterMap_le (f : α → Option β) (l : List α) :
    (filterMap f l).length ≤ l.length

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (filterMap f l).length ≤ l.length

Tactic:
rw [← length_map _ some, map_filterMap_some_eq_filter_map_isSome, ← length_map _ f]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (filter (fun b => b.isSome) (map f l)).length ≤ (map f l).length

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (filter (fun b => b.isSome) (map f l)).length ≤ (map f l).length

Tactic:
apply length_filter_le

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma memLp_indicator_iff_restrict (hs : MeasurableSet s) :
    MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
s : Set α
hs : MeasurableSet s
⊢ MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s)

Tactic:
simp [MemLp, aestronglyMeasurable_indicator_iff hs, eLpNorm_indicator_eq_eLpNorm_restrict hs]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem update_snoc_last : update (snoc p x) (last n) z = snoc p z

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ update (snoc p x) (last n) z (last n) = snoc p z (last n)

Tactic:
simp

Result:
no goals

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ update (snoc p x) (last n) z j = snoc p z j

Tactic:
have : j ≠ last n := Fin.ne_of_lt h

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
this : j ≠ last n
⊢ update (snoc p x) (last n) z j = snoc p z j

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
⊢ update (snoc p x) (last n) z j = snoc p z j

Tactic:
by_cases h : j.val < n

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
⊢ update (snoc p x) (last n) z j = snoc p z j

case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ update (snoc p x) (last n) z j = snoc p z j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ↑j < n
this : j ≠ last n
⊢ update (snoc p x) (last n) z j = snoc p z j

Tactic:
simp [h, update_of_ne, this, snoc]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
⊢ update (snoc p x) (last n) z = snoc p z

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
⊢ update (snoc p x) (last n) z j = snoc p z j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ update (snoc p x) (last n) z j = snoc p z j

Tactic:
rw [eq_last_of_not_lt h]

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
z : α (last n)
j : Fin (n + 1)
h : ¬↑j < n
⊢ update (snoc p x) (last n) z (last n) = snoc p z (last n)