harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
theorem map_pow_le_pow' {F α : Type*} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {f : F}
    (hf1 : f 1 ≤ 1) (a : α) : ∀ n : ℕ, f (a ^ n) ≤ f a ^ n
  | 0 => by simp only [pow_zero, hf1]
  | n + 1 => by
    simp only [pow_succ _ n]
    exact le_trans (map_mul_le_mul f _ a)
      (mul_le_mul_of_nonneg_right (map_pow_le_pow' hf1 _ n) (apply_nonneg f a))

Proof state:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hf1 : f 1 ≤ 1
a : α
n : ℕ
⊢ f (a ^ n * a) ≤ f a ^ n * f a

Tactic:
exact le_trans (map_mul_le_mul f _ a)
  (mul_le_mul_of_nonneg_right (map_pow_le_pow' hf1 _ n) (apply_nonneg f a))

Result:
no goals

Proof state:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hf1 : f 1 ≤ 1
a : α
n : ℕ
⊢ f (a ^ (n + 1)) ≤ f a ^ (n + 1)

Tactic:
simp only [pow_succ _ n]

Result:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hf1 : f 1 ≤ 1
a : α
n : ℕ
⊢ f (a ^ n * a) ≤ f a ^ n * f a

Proof state:
F : Type u_2
α : Type u_3
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hf1 : f 1 ≤ 1
a : α
⊢ f (a ^ 0) ≤ f a ^ 0

Tactic:
simp only [pow_zero, hf1]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_biUnion_le {ι α : Type u} (A : ι → Set α) (s : Set ι) :
    #(⋃ x ∈ s, A x) ≤ #s * ⨆ x : s, #(A x.1)

Proof state:
ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x ∈ s, A x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Tactic:
rw [biUnion_eq_iUnion]

Result:
ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x, A ↑x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Proof state:
ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x, A ↑x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Tactic:
apply mk_iUnion_le

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_setAverage_le_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : IntegrableOn f s μ) :
    0 < μ ({x ∈ s | ⨍ a in s, f a ∂μ ≤ f x})

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
⊢ 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}

Tactic:
simpa [integral_neg, neg_div] using measure_le_setAverage_pos hμ hμ₁ hf.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_flatMap {l : List α} {f : α → List β} :
    (l.flatMap f).all p = l.all fun a => (f a).all p

Proof state:
α : Type u_1
β : Type u_2
p : β → Bool
l : List α
f : α → List β
⊢ (flatMap f l).all p = l.all fun a => (f a).all p

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma ofπ_π : (ofπ π hπ).π = π

Proof state:
case h.h
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
a✝ : relations.G
⊢ ((ofπ π hπ).π ∘ₗ Finsupp.lsingle a✝) 1 = (π ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
simp [ofπ]

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
⊢ (ofπ π hπ).π = π

Tactic:
ext

Result:
case h.h
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
a✝ : relations.G
⊢ ((ofπ π hπ).π ∘ₗ Finsupp.lsingle a✝) 1 = (π ∘ₗ Finsupp.lsingle a✝) 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem Nat.div_add_eq_left_of_lt {x y z : Nat} (hx : z ∣ x) (hy : y < z) (hz : 0 < z) :
    (x + y) / z = x / z

Proof state:
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ (x + y) / z = x / z

Tactic:
refine Nat.div_eq_of_lt_le ?lo ?hi

Result:
case lo
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x / z * z ≤ x + y

case hi
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x + y < (x / z + 1) * z

Proof state:
case hi.hlt
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ y < z

Tactic:
exact hy

Result:
no goals

Proof state:
case hi
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x + y < x / z * z + z

Tactic:
apply Nat.add_lt_add_of_le_of_lt

Result:
case hi.hle
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x ≤ x / z * z

case hi.hlt
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ y < z

Proof state:
case hi
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x + y < (x / z + 1) * z

Tactic:
simp only [succ_eq_add_one, Nat.add_mul, Nat.one_mul]

Result:
case hi
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x + y < x / z * z + z

Proof state:
case hi.hle
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x ≤ x / z * z

Tactic:
apply Nat.le_of_eq

Result:
case hi.hle.p
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x = x / z * z

Proof state:
case hi.hle.p
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x = x / z * z

Tactic:
exact (Nat.div_eq_iff_eq_mul_left hz hx).mp rfl

Result:
no goals

Proof state:
case lo.a
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x / z * z ≤ ?lo.m

Tactic:
exact div_mul_le_self x z

Result:
no goals

Proof state:
case lo.a
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x ≤ x + y

Tactic:
omega

Result:
no goals

Proof state:
case lo
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x / z * z ≤ x + y

Tactic:
apply Nat.le_trans

Result:
case lo.a
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ x / z * z ≤ ?lo.m

case lo.a
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ ?lo.m ≤ x + y

case lo.m
x y z : Nat
hx : z ∣ x
hy : y < z
hz : 0 < z
⊢ Nat
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem NNReal.hasSum_geometric {r : ℝ≥0} (hr : r < 1) : HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹

Proof state:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑(1 - r))⁻¹

Tactic:
rw [NNReal.coe_sub (le_of_lt hr)]

Result:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑1 - ↑r)⁻¹

Proof state:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑(r ^ a)) ↑(1 - r)⁻¹

Tactic:
push_cast

Result:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑(1 - r))⁻¹

Proof state:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑1 - ↑r)⁻¹

Tactic:
exact hasSum_geometric_of_lt_one r.coe_nonneg hr

Result:
no goals

Proof state:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun n => r ^ n) (1 - r)⁻¹

Tactic:
apply NNReal.hasSum_coe.1

Result:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑(r ^ a)) ↑(1 - r)⁻¹
-- Mathlib/Analysis/RCLike/Basic.lean
theorem pos_iff : 0 < z ↔ 0 < re z ∧ im z = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ 0 < re z ∧ im z = 0

Tactic:
simpa only [map_zero, eq_comm] using lt_iff_re_im (z := 0) (w := z)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_empty_eq : G'.deleteEdges ∅ = G'

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.deleteEdges ∅ = G'

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem of_smul_measure {c : ℝ≥0∞} (hc_ne_top : c ≠ ∞) (hT : FinMeasAdditive (c • μ) T) :
    FinMeasAdditive μ T

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : ¬c = 0 ∧ μ s = ⊤
⊢ μ s = ⊤

Tactic:
exact hμs.2

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : (c • μ) s = ⊤
⊢ μ s = ⊤

Tactic:
rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top] at hμs

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : c ≠ 0 ∧ μ s = ⊤ ∨ c = ⊤ ∧ μ s ≠ 0
⊢ μ s = ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
⊢ FinMeasAdditive μ T

Tactic:
refine of_eq_top_imp_eq_top (fun s _ hμs => ?_) hT

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : (c • μ) s = ⊤
⊢ μ s = ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : c ≠ 0 ∧ μ s = ⊤ ∨ c = ⊤ ∧ μ s ≠ 0
⊢ μ s = ⊤

Tactic:
simp only [hc_ne_top, or_false, Ne, false_and] at hμs

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : ¬c = 0 ∧ μ s = ⊤
⊢ μ s = ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_concat {l : List α} {e : α} {f : (i : Nat) → α → (h : i < (l ++ [e]).length) → β}:
    (l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i a h => f i a (by simp; omega)) ++ [f l.length e (by simp)]

Proof state:
α : Type ?u.29889
β : Type ?u.29986
l : List α
e : α
f : (i : Nat) → α → i < (l ++ [e]).length → β
i : Nat
a : α
h : i < l.length
⊢ i < l.length + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
e : α
f : (i : Nat) → α → i < (l ++ [e]).length → β
⊢ (l ++ [e]).mapFinIdx f = (l.mapFinIdx fun i a h => f i a ⋯) ++ [f l.length e ⋯]

Tactic:
simp [mapFinIdx_append]

Result:
no goals

Proof state:
α : Type ?u.29889
β : Type ?u.29986
l : List α
e : α
f : (i : Nat) → α → i < (l ++ [e]).length → β
i : Nat
a : α
h : i < l.length
⊢ i < (l ++ [e]).length

Tactic:
simp

Result:
α : Type ?u.29889
β : Type ?u.29986
l : List α
e : α
f : (i : Nat) → α → i < (l ++ [e]).length → β
i : Nat
a : α
h : i < l.length
⊢ i < l.length + 1

Proof state:
α : Type ?u.29889
β : Type ?u.29986
l : List α
e : α
f : (i : Nat) → α → i < (l ++ [e]).length → β
⊢ l.length < (l ++ [e]).length

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem isLocalHom_localRingHom (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P)
    (hIJ : I = J.comap f) : IsLocalHom (localRingHom I J f hIJ) :=
  IsLocalHom.mk fun x hx => by
    rcases IsLocalization.mk'_surjective I.primeCompl x with ⟨r, s, rfl⟩
    rw [localRingHom_mk'] at hx
    rw [AtPrime.isUnit_mk'_iff] at hx ⊢
    exact fun hr => hx ((SetLike.ext_iff.mp hIJ r).mp hr)

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit ((localRingHom I J f hIJ) (mk' (Localization.AtPrime I) r s))
⊢ IsUnit (mk' (Localization.AtPrime I) r s)

Tactic:
rw [localRingHom_mk'] at hx

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit (mk' (Localization.AtPrime J) (f r) ⟨f ↑s, ⋯⟩)
⊢ IsUnit (mk' (Localization.AtPrime I) r s)

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : f r ∈ J.primeCompl
⊢ r ∈ I.primeCompl

Tactic:
exact fun hr => hx ((SetLike.ext_iff.mp hIJ r).mp hr)

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit (mk' (Localization.AtPrime J) (f r) ⟨f ↑s, ⋯⟩)
⊢ IsUnit (mk' (Localization.AtPrime I) r s)

Tactic:
rw [AtPrime.isUnit_mk'_iff] at hx ⊢

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : f r ∈ J.primeCompl
⊢ r ∈ I.primeCompl

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
hx : IsUnit ((localRingHom I J f hIJ) x)
⊢ IsUnit x

Tactic:
rcases IsLocalization.mk'_surjective I.primeCompl x with ⟨r, s, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit ((localRingHom I J f hIJ) (mk' (Localization.AtPrime I) r s))
⊢ IsUnit (mk' (Localization.AtPrime I) r s)
-- Mathlib/Data/W/Basic.lean
theorem depth_pos (t : WType β) : 0 < t.depth

Proof state:
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < t.depth

Tactic:
cases t

Result:
case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < (mk a✝ f✝).depth

Proof state:
case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < (mk a✝ f✝).depth

Tactic:
apply Nat.succ_pos

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem three_dvd_iff (n : ℕ) : 3 ∣ n ↔ 3 ∣ (digits 10 n).sum :=
  dvd_iff_dvd_digits_sum 3 10 (by norm_num) n

Proof state:
n : ℕ
⊢ 10 % 3 = 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma biUnion_filter_eq_of_maps_to [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β}
    (h : ∀ x ∈ s, f x ∈ t) : (t.biUnion fun a ↦ s.filter fun c ↦ f c = a) = s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
s : Finset α
t : Finset β
f : α → β
h : ∀ x ∈ s, f x ∈ t
⊢ (t.biUnion fun a => filter (fun c => f c = a) s) = s

Tactic:
simpa only [disjiUnion_eq_biUnion] using disjiUnion_filter_eq_of_maps_to h

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x))
    (x₀ : α 0) (x : ∀ i : Fin n, α i.succ) : @consCases _ _ _ h (cons x₀ x) = h x₀ x

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
P : ((i : Fin n.succ) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ h (cons x₀ x 0) (tail (cons x₀ x)) = h x₀ x

Tactic:
congr

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
P : ((i : Fin n.succ) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ consCases h (cons x₀ x) = h x₀ x

Tactic:
rw [consCases, cast_eq]

Result:
n : ℕ
α : Fin (n + 1) → Sort u
P : ((i : Fin n.succ) → α i) → Sort v
h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ h (cons x₀ x 0) (tail (cons x₀ x)) = h x₀ x
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.div_const (hc : HasDerivWithinAt c c' s x) (d : 𝕜') :
    HasDerivWithinAt (fun x => c x / d) (c' / d) s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
d : 𝕜'
⊢ HasDerivWithinAt (fun x => c x / d) (c' / d) s x

Tactic:
simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem orElse_empty (c : Computation α) : (c <|> empty α) = c

Proof state:
case h2
α : Type u
c s' s✝ : Computation α
h : (s✝ <|> empty α) = s'
s : Computation α
⊢ (s <|> (empty α).think) = (s <|> empty α)

Tactic:
rw [← think_empty]

Result:
no goals

Proof state:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ => (c₂ <|> empty α) = c₁) s'.destruct s.destruct

Tactic:
rw [← h]

Result:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ => (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct

Proof state:
α : Type u
c : Computation α
⊢ IsBisimulation fun c₁ c₂ => (c₂ <|> empty α) = c₁

Tactic:
intro s' s h

Result:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ => (c₂ <|> empty α) = c₁) s'.destruct s.destruct

Proof state:
α : Type u
c : Computation α
⊢ (c <|> empty α) = c

Tactic:
apply eq_of_bisim (fun c₁ c₂ => (c₂ <|> empty α) = c₁) _ rfl

Result:
α : Type u
c : Computation α
⊢ IsBisimulation fun c₁ c₂ => (c₂ <|> empty α) = c₁

Proof state:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ => (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct

Tactic:
apply recOn s <;> intro s <;> rw [think_empty] <;> simp

Result:
case h2
α : Type u
c s' s✝ : Computation α
h : (s✝ <|> empty α) = s'
s : Computation α
⊢ (s <|> (empty α).think) = (s <|> empty α)
-- Mathlib/Analysis/Complex/AbelLimit.lean
theorem stolzSet_empty {M : ℝ} (hM : M ≤ 1) : stolzSet M = ∅

Proof state:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ 1 * (1 - ‖z‖) = ‖1‖ - ‖z‖

Tactic:
rw [one_mul, norm_one]

Result:
no goals

Proof state:
case h
M : ℝ
hM : M ≤ 1
z : ℂ
⊢ 0 < 1 - ‖z‖ → M * (1 - ‖z‖) ≤ ‖1 - z‖

Tactic:
intro zn

Result:
case h
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ M * (1 - ‖z‖) ≤ ‖1 - z‖

Proof state:
case h
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ M * (1 - ‖z‖) ≤ ‖1 - z‖

Tactic:
calc
  _ ≤ 1 * (1 - ‖z‖) := mul_le_mul_of_nonneg_right hM zn.le
  _ = ‖(1 : ℂ)‖ - ‖z‖ := by rw [one_mul, norm_one]
  _ ≤ _ := norm_sub_norm_le _ _

Result:
no goals

Proof state:
M : ℝ
hM : M ≤ 1
⊢ stolzSet M = ∅

Tactic:
ext z

Result:
case h
M : ℝ
hM : M ≤ 1
z : ℂ
⊢ z ∈ stolzSet M ↔ z ∈ ∅

Proof state:
case h
M : ℝ
hM : M ≤ 1
z : ℂ
⊢ z ∈ stolzSet M ↔ z ∈ ∅

Tactic:
rw [stolzSet, Set.mem_setOf, Set.mem_empty_iff_false, iff_false, not_and, not_lt, ← sub_pos]

Result:
case h
M : ℝ
hM : M ≤ 1
z : ℂ
⊢ 0 < 1 - ‖z‖ → M * (1 - ‖z‖) ≤ ‖1 - z‖
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
lemma SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber [DecidableRel G.Adj]
    (hG : G.LocallyLinear) : #(G.cliqueFinset 3) ≤ ruzsaSzemerediNumber α

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) ≤ ruzsaSzemerediNumber α

Tactic:
exact le_findGreatest card_cliqueFinset_le ⟨G, inferInstance, by congr, hG⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) ≤ ruzsaSzemerediNumber α

Tactic:
classical
exact le_findGreatest card_cliqueFinset_le ⟨G, inferInstance, by congr, hG⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) = #(G.cliqueFinset 3)

Tactic:
congr

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_le_iff_le_mul (h₁ : b = ∞ → a ≠ 0) (h₂ : a = ∞ → b ≠ 0) : a⁻¹ ≤ b ↔ 1 ≤ a * b

Proof state:
case hb0
a b : ℝ≥0∞
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ⊤

case hbt
a b : ℝ≥0∞
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ ⊤ ∨ b ≠ 0

Tactic:
exacts [or_not_of_imp h₁, not_or_of_imp h₂]

Result:
no goals

Proof state:
a b : ℝ≥0∞
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]

Result:
case hb0
a b : ℝ≥0∞
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ⊤

case hbt
a b : ℝ≥0∞
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ ⊤ ∨ b ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_empty_of_size_eq_zero (h : l.size = 0) : l = #[]

Proof state:
case mk
α✝ : Type u_1
toList✝ : List α✝
h : { toList := toList✝ }.size = 0
⊢ { toList := toList✝ } = #[]

Tactic:
simp_all

Result:
no goals

Proof state:
α✝ : Type u_1
l : Array α✝
h : l.size = 0
⊢ l = #[]

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
toList✝ : List α✝
h : { toList := toList✝ }.size = 0
⊢ { toList := toList✝ } = #[]
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_erase (p : R[ℕ]) (n : ℕ) :
    (⟨p.erase n⟩ : R[X]) = (⟨p⟩ : R[X]).erase n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[ℕ]
n : ℕ
⊢ { toFinsupp := Finsupp.erase n p } = erase n { toFinsupp := p }

Tactic:
rcases p with ⟨⟩

Result:
case mk
R : Type u
inst✝ : Semiring R
n : ℕ
support✝ : Finset ℕ
toFun✝ : ℕ → R
mem_support_toFun✝ : ∀ (a : ℕ), a ∈ support✝ ↔ toFun✝ a ≠ 0
⊢ { toFinsupp := Finsupp.erase n { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } } =
    erase n { toFinsupp := { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } }

Proof state:
case mk
R : Type u
inst✝ : Semiring R
n : ℕ
support✝ : Finset ℕ
toFun✝ : ℕ → R
mem_support_toFun✝ : ∀ (a : ℕ), a ∈ support✝ ↔ toFun✝ a ≠ 0
⊢ { toFinsupp := Finsupp.erase n { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } } =
    erase n { toFinsupp := { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } }

Tactic:
simp only [erase_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma ΨSq_ne_zero [NoZeroDivisors R] {n : ℤ} (h : (n : R) ≠ 0) : W.ΨSq n ≠ 0

Proof state:
case neg.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
hm : n.natAbs = 0
⊢ W.ΨSq n ≠ 0

Tactic:
push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
⊢ W.ΨSq n ≠ 0

Tactic:
rcases hm : n.natAbs with _ | m

Result:
case neg.zero
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
hm : n.natAbs = 0
⊢ W.ΨSq n ≠ 0

case neg.succ
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
m : ℕ
hm : n.natAbs = m + 1
⊢ W.ΨSq n ≠ 0

Proof state:
case neg.succ
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
m : ℕ
hm : n.natAbs = m + 1
⊢ W.ΨSq n ≠ 0

Tactic:
rcases Int.natAbs_eq_iff.mp hm with rfl | rfl <;>
  rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn <;>
  push_cast [hn, ΨSq_neg, ΨSq_one] <;>
  exact fun h' => h <| C_injective <| by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
⊢ W.ΨSq n ≠ 0

Tactic:
by_cases hn : 1 < n.natAbs

Result:
case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : 1 < n.natAbs
⊢ W.ΨSq n ≠ 0

case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
⊢ W.ΨSq n ≠ 0

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ C ↑(-↑(m + 1)) = C 0

Tactic:
push_cast [hn, C_neg, C_1, h', neg_zero, C_0]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
h' : 1 = 0
⊢ 0 = 0

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : 1 < n.natAbs
⊢ W.ΨSq n ≠ 0

Tactic:
exact ne_zero_of_natDegree_gt <| W.natDegree_ΨSq_pos hn h

Result:
no goals