harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
@[simp] lemma cylinderEvents_univ : cylinderEvents (π := π) univ = MeasurableSpace.pi

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
⊢ cylinderEvents univ = MeasurableSpace.pi

Tactic:
simp [cylinderEvents, MeasurableSpace.pi]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem enum_le_enum (r : α → α → Prop) [IsWellOrder α r] {o₁ o₂ : Iio (type r)} :
    ¬r (enum r o₁) (enum r o₂) ↔ o₂ ≤ o₁

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : ↑(Iio (type r))
⊢ ¬r ((enum r) o₁) ((enum r) o₂) ↔ o₂ ≤ o₁

Tactic:
rw [enum_lt_enum (r := r), not_lt]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_iff_isIso_leftHomologyMap' (φ : S₁ ⟶ S₂)
    (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
rw [γ.quasiIso_iff, γ.leftHomologyMap'_eq]

Result:
no goals
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
lemma isOpen_iff_ωScottContinuous_mem {α} [OmegaCompletePartialOrder α] {s : Set (Scott α)} :
    IsOpen s ↔ ωScottContinuous fun x ↦ x ∈ s

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
s : Set (Scott α)
⊢ IsOpen s ↔ ωScottContinuous fun x => x ∈ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem mem_polar_singleton {x : E} (y : F) : y ∈ B.polar {x} ↔ ‖B x y‖ ≤ 1

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
x : E
y : F
⊢ y ∈ B.polar {x} ↔ ‖(B x) y‖ ≤ 1

Tactic:
simp only [polar_singleton, Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem ContDiffAt.rpow (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (h : f x ≠ 0) :
    ContDiffAt ℝ n (fun x => f x ^ g x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
x : E
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
h : f x ≠ 0
⊢ ContDiffAt ℝ n (fun x => f x ^ g x) x

Tactic:
exact (contDiffAt_rpow_of_ne (f x, g x) h).comp x (hf.prod hg)

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem zero_lf_inv' : ∀ x : PGame, 0 ⧏ inv' x
  | ⟨xl, xr, xL, xR⟩ => by
    convert lf_mk _ _ InvTy.zero
    rfl

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ 0 ⧏ (mk xl xr xL xR).inv'

Tactic:
convert lf_mk _ _ InvTy.zero

Result:
case h.e'_1
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ 0 = invVal (fun i => xL ↑i) xR (fun i => (xL ↑i).inv') (fun i => (xR i).inv') (mk xl xr xL xR) InvTy.zero

Proof state:
case h.e'_1
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ 0 = invVal (fun i => xL ↑i) xR (fun i => (xL ↑i).inv') (fun i => (xR i).inv') (mk xl xr xL xR) InvTy.zero

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_comp_add_left (a : E) :
    fderivWithin 𝕜 (fun x ↦ f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ fderivWithin 𝕜 (fun x => f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x)

Tactic:
classical
simp only [fderivWithin, hasFDerivWithinAt_comp_add_left, differentiableWithinAt_comp_add_left]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
a : E
⊢ fderivWithin 𝕜 (fun x => f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x)

Tactic:
simp only [fderivWithin, hasFDerivWithinAt_comp_add_left, differentiableWithinAt_comp_add_left]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem comp_coconePointsIsoOfNatIso_inv {F G : J ⥤ C} {s : Cocone F} {t : Cocone G}
    (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
    t.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).inv = w.inv.app j ≫ s.ι.app j

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
s : Cocone F
t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
j : J
⊢ t.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).inv = w.inv.app j ≫ s.ι.app j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem sub_eq_add_neg (a b : Rat) : a - b = a + -b

Proof state:
a b : Rat
⊢ a - b = a + -b

Tactic:
simp [add_def, sub_def, Int.neg_mul, Int.sub_eq_add_neg]

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

Proof state:
case asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal ↔ x✝ ∈ ((comap (RingHom.fst 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 R
⊢ (primeSpectrumProd R S).symm (Sum.inl x) = (comap (RingHom.fst R S)) x

Tactic:
ext

Result:
case asIdeal.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal ↔ x✝ ∈ ((comap (RingHom.fst R S)) x).asIdeal
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_add_left {f : α → ℝ≥0∞} (hf : Measurable f) (g : α → ℝ≥0∞) :
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
refine le_antisymm ?_ (le_lintegral_add _ _)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
rcases exists_measurable_le_lintegral_eq μ fun a => f a + g a with ⟨φ, hφm, hφ_le, hφ_eq⟩

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun a => f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Proof state:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun a => f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
calc
  ∫⁻ a, f a + g a ∂μ = ∫⁻ a, φ a ∂μ := hφ_eq
  _ ≤ ∫⁻ a, f a + (φ a - f a) ∂μ := lintegral_mono fun a => le_add_tsub
  _ = ∫⁻ a, f a ∂μ + ∫⁻ a, φ a - f a ∂μ := lintegral_add_aux hf (hφm.sub hf)
  _ ≤ ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
    add_le_add_left (lintegral_mono fun a => tsub_le_iff_left.2 <| hφ_le a) _

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
lemma count_nth_succ_of_infinite (hp : (setOf p).Infinite) (n : ℕ) :
    count p (nth p n + 1) = n + 1

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (setOf p).Infinite
n : ℕ
⊢ count p (nth p n + 1) = n + 1

Tactic:
rw [count_succ, count_nth_of_infinite hp, if_pos (nth_mem_of_infinite hp _)]

Result:
no goals
-- Mathlib/NumberTheory/Primorial.lean
theorem primorial_add_dvd {m n : ℕ} (h : n ≤ m) : (m + n)# ∣ m# * choose (m + n) m :=
  calc
    (m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p := primorial_add _ _
    _ ∣ m# * choose (m + n) m :=
      mul_dvd_mul_left _ <|
        prod_primes_dvd _ (fun _ hk ↦ (mem_filter.1 hk).2.prime) fun p hp ↦ by
          rw [mem_filter, mem_Ico] at hp
          exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
              (Nat.lt_succ_iff.1 hp.1.2)

Proof state:
m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ filter (fun p => Nat.Prime p) (Ico (m + 1) (m + n + 1))
⊢ p ∣ (m + n).choose m

Tactic:
rw [mem_filter, mem_Ico] at hp

Result:
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m

Proof state:
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m

Tactic:
exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
    (Nat.lt_succ_iff.1 hp.1.2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
    as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs

Proof state:
α : Type u_1
as bs : Array α
xs : List α
⊢ as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs

Tactic:
cases as

Result:
case mk
α : Type u_1
bs : Array α
xs toList✝ : List α
⊢ { toList := toList✝ } ++ bs = xs.toArray ↔ { toList := toList✝ }.toList ++ bs.toList = xs

Proof state:
case mk.mk
α : Type u_1
xs toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } ++ { toList := toList✝ } = xs.toArray ↔
    { toList := toList✝¹ }.toList ++ { toList := toList✝ }.toList = xs

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
bs : Array α
xs toList✝ : List α
⊢ { toList := toList✝ } ++ bs = xs.toArray ↔ { toList := toList✝ }.toList ++ bs.toList = xs

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
xs toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } ++ { toList := toList✝ } = xs.toArray ↔
    { toList := toList✝¹ }.toList ++ { toList := toList✝ }.toList = xs
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.sub_nsmul_eq [AddGroup α] (h : Periodic f c) (n : ℕ) : f (x - n • c) = f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : AddGroup α
h : Periodic f c
n : ℕ
⊢ f (x - n • c) = f x

Tactic:
simpa only [sub_eq_add_neg] using h.neg_nsmul n x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_nil_iff {l : List α} : List.mapIdx f l = [] ↔ l = []

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
⊢ mapIdx f l = [] ↔ l = []

Tactic:
rw [List.mapIdx_eq_zipIdx_map, List.map_eq_nil_iff, List.zipIdx_eq_nil_iff]

Result:
no goals
-- Mathlib/Tactic/NormNum/RealSqrt.lean
lemma isNat_realSqrt_of_isRat_negOfNat {x : ℝ} {num : ℕ} {denom : ℕ}
    (h : IsRat x (.negOfNat num) denom) : IsNat √x (nat_lit 0)

Proof state:
case mk
num denom : ℕ
inv : Invertible ↑denom
h₁ : 0 ≤ ↑↑num * ⅟↑denom
⊢ √(↑(Int.negOfNat num) * ⅟↑denom) = ↑0

Tactic:
simpa [Nat.cast_zero, Real.sqrt_eq_zero', Int.cast_negOfNat, neg_mul, neg_nonpos] using h₁

Result:
no goals

Proof state:
case mk
num denom : ℕ
inv : Invertible ↑denom
⊢ √(↑(Int.negOfNat num) * ⅟↑denom) = ↑0

Tactic:
have h₁ : 0 ≤ (num : ℚ) * ⅟(denom : ℝ) :=
  mul_nonneg (Nat.cast_nonneg' _) (invOf_nonneg.2 <| Nat.cast_nonneg' _)

Result:
case mk
num denom : ℕ
inv : Invertible ↑denom
h₁ : 0 ≤ ↑↑num * ⅟↑denom
⊢ √(↑(Int.negOfNat num) * ⅟↑denom) = ↑0

Proof state:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
⊢ √x = ↑0

Tactic:
obtain ⟨inv, rfl⟩ := h

Result:
case mk
num denom : ℕ
inv : Invertible ↑denom
⊢ √(↑(Int.negOfNat num) * ⅟↑denom) = ↑0

Proof state:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
⊢ IsNat (√x) 0

Tactic:
refine ⟨?_⟩

Result:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
⊢ √x = ↑0
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_indicator_subset (w : ι → k) (p : ι → P) (b : P) {s₁ s₂ : Finset ι}
    (h : s₁ ⊆ s₂) :
    s₁.weightedVSubOfPoint p b w = s₂.weightedVSubOfPoint p b (Set.indicator (↑s₁) w)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ (s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ∑ i ∈ s₁, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (↑s₁).indicator w i • (p i -ᵥ b)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ∑ i ∈ s₁, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (↑s₁).indicator w i • (p i -ᵥ b)

Tactic:
exact Eq.symm <|
  sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma Nonempty.zero_div (hs : s.Nonempty) : 0 / s = 0 :=
  s.zero_div_subset.antisymm <| by simpa [mem_div] using hs

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
simpa [mem_div] using hs

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem balancedSz_up {l r₁ r₂ : ℕ} (h₁ : r₁ ≤ r₂) (h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l)
    (H : BalancedSz l r₁) : BalancedSz l r₂

Proof state:
case inr
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l ≤ delta * r₁ ∧ r₁ ≤ delta * l
⊢ l ≤ delta * r₂

Tactic:
exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)

Result:
no goals

Proof state:
case inl.zero
l r₁ : ℕ
H : l + r₁ ≤ 1
h₁ : r₁ ≤ 0
h₂ : l + 0 ≤ 1 ∨ 0 ≤ delta * l
h : ¬l + 0 ≤ 1
⊢ l ≤ delta * 0

Tactic:
cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)

Result:
no goals

Proof state:
case inl.succ
l r₁ : ℕ
H : l + r₁ ≤ 1
n✝ : ℕ
h₁ : r₁ ≤ n✝ + 1
h₂ : l + (n✝ + 1) ≤ 1 ∨ n✝ + 1 ≤ delta * l
h : ¬l + (n✝ + 1) ≤ 1
⊢ l ≤ delta * (n✝ + 1)

Tactic:
exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)

Result:
no goals

Proof state:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
⊢ BalancedSz l r₂

Tactic:
refine or_iff_not_imp_left.2 fun h => ?_

Result:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l

Proof state:
case inl
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l + r₁ ≤ 1
⊢ l ≤ delta * r₂

Tactic:
cases r₂

Result:
case inl.zero
l r₁ : ℕ
H : l + r₁ ≤ 1
h₁ : r₁ ≤ 0
h₂ : l + 0 ≤ 1 ∨ 0 ≤ delta * l
h : ¬l + 0 ≤ 1
⊢ l ≤ delta * 0

case inl.succ
l r₁ : ℕ
H : l + r₁ ≤ 1
n✝ : ℕ
h₁ : r₁ ≤ n✝ + 1
h₂ : l + (n✝ + 1) ≤ 1 ∨ n✝ + 1 ≤ delta * l
h : ¬l + (n✝ + 1) ≤ 1
⊢ l ≤ delta * (n✝ + 1)

Proof state:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂ ∧ r₂ ≤ delta * l

Tactic:
refine ⟨?_, h₂.resolve_left h⟩

Result:
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- `Fintype.expect_bijective` is a variant of `Finset.expect_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.expect_comp` for a version without `h`. -/
lemma expect_bijective (e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M)
    (h : ∀ i, f i = g (e i)) : 𝔼 i, f i = 𝔼 i, g i :=
  expect_nbij e (fun _ _ ↦ mem_univ _) (fun i _ ↦ h i) he.injective.injOn <| by
    simpa using he.surjective.surjOn _

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (i : ι), f i = g (e i)
⊢ Set.SurjOn e ↑univ ↑univ

Tactic:
simpa using he.surjective.surjOn _

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean
theorem smul_Lp_add (c : Mᵈᵐᵃ) : ∀ f g : Lp E p μ, c • (f + g) = c • f + c • g

Proof state:
case mk.mk.mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • (⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ + ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩) =
    c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ + c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
⊢ ∀ (f g : ↥(Lp E p μ)), c • (f + g) = c • f + c • g

Tactic:
rintro ⟨⟨⟩, _⟩ ⟨⟨⟩, _⟩

Result:
case mk.mk.mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • (⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ + ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩) =
    c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ + c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩
-- Mathlib/Topology/LocallyClosed.lean
lemma closure_inter_coborder :
    closure s ∩ coborder s = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ∩ coborder s = s

Tactic:
rw [inter_comm, coborder_inter_closure]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_centroidWeights_eq_one_of_cast_card_ne_zero (h : (#s : k) ≠ 0) :
    ∑ i ∈ s, s.centroidWeights k i = 1

Proof state:
k : Type u_1
inst✝ : DivisionRing k
ι : Type u_4
s : Finset ι
h : ↑(#s) ≠ 0
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem _root_.Decidable.List.eq_or_ne_mem_of_mem [DecidableEq α]
    {a b : α} {l : List α} (h : a ∈ b :: l) : a = b ∨ a ≠ b ∧ a ∈ l

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
by_cases hab : a = b

Result:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact ((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact Or.inl hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} :
    (empty c : Raw α β).getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
a : α
fallback : β a
c : Nat
⊢ (empty c).getD a fallback = fallback

Tactic:
simp_to_raw using Raw₀.getD_empty

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_deriv_comp_mul_deriv' {f f' g g' : ℝ → ℝ} (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
    (hf' : ContinuousOn f' [[a, b]]) (hg : ContinuousOn g [[f a, f b]])
    (hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x)
    (hg' : ContinuousOn g' (f '' [[a, b]])) :
    (∫ x in a..b, (g' ∘ f) x * f' x) = (g ∘ f) b - (g ∘ f) a

Proof state:
a b : ℝ
f f' g g' : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (f a ⊓ f b) (f a ⊔ f b), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a

Tactic:
simpa [mul_comm] using integral_deriv_comp_smul_deriv' hf hff' hf' hg hgg' hg'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.sle_eq_ult (x y : BitVec w) :
    x.sle y = !((!x.getLsbD (w - 1) == y.getLsbD (w - 1)) ^^ y.ult x)

Proof state:
w : Nat
x y : BitVec w
⊢ x.sle y = !(!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ y.ult x)

Tactic:
rw [BitVec.sle_eq_not_slt, BitVec.slt_eq_ult, Bool.beq_comm]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem isCycleOn_support_of_mem_cycleFactorsFinset {g c : Equiv.Perm α}
    (hc : c ∈ g.cycleFactorsFinset) :
    IsCycleOn g c.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ g.IsCycleOn ↑c.support

Tactic:
obtain ⟨x, hx⟩ := IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp hc).1

Result:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g.IsCycleOn ↑c.support

Proof state:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g.IsCycleOn ↑c.support

Tactic:
rw [cycle_is_cycleOf hx hc]

Result:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g.IsCycleOn ↑(g.cycleOf x).support

Proof state:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g.IsCycleOn ↑(g.cycleOf x).support

Tactic:
exact isCycleOn_support_cycleOf g x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem prefix_concat (a : α) (l) : l <+: concat l a

Proof state:
α : Type u_1
a : α
l : List α
⊢ l <+: l.concat a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mk_eq_top_iff {N : Submodule R M} {h} :
    (⟨N, h⟩ : LieSubmodule R L M) = ⊤ ↔ N = ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ { toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤

Tactic:
rw [← toSubmodule_inj, top_toSubmodule]

Result:
no goals