harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffWithinAt_Ioi (a : ℝ) : UniqueDiffWithinAt ℝ (Ioi a) a :=
  uniqueDiffWithinAt_convex (convex_Ioi a) (by simp) (by simp)

Proof state:
a : ℝ
⊢ (interior (Ioi a)).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
⊢ a ∈ closure (Ioi a)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_zsmul_add (a b : α) (m : ℤ) : toIcoMod hp a (m • p + b) = toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (m • p + b) = toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_zsmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_replicate' {a : α} {b : β} {n : Nat} :
    zip (replicate n a) (replicate n b) = replicate n (a, b)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
n : Nat
⊢ (replicate n a).zip (replicate n b) = replicate n (a, b)

Tactic:
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
β : Type u_2
a : α
b : β
⊢ (replicate 0 a).zip (replicate 0 b) = replicate 0 (a, b)

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
a : α
b : β
n : Nat
ih : (replicate n a).zip (replicate n b) = replicate n (a, b)
⊢ (replicate (n + 1) a).zip (replicate (n + 1) b) = replicate (n + 1) (a, b)

Tactic:
simp [replicate_succ, ih]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem exists_disjoint_powers_of_span_eq_top (s : Set α) (hs : span s = ⊤) (I : Ideal α)
    (hI : I ≠ ⊤) : ∃ r ∈ s, Disjoint (I : Set α) (Submonoid.powers r)

Proof state:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : M ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
rw [Ne, eq_top_iff, ← hs, span_le, Set.not_subset] at this

Result:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Proof state:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ ↑M
a : α
has : a ∈ s
haM : a ∉ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
exact ⟨a, has, Set.disjoint_left.mpr fun x hx ⟨n, hn⟩ ↦
  haM (hM.isPrime.mem_of_pow_mem _ (le <| hn ▸ hx))⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
have := hM.1.1

Result:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : M ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Proof state:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
have ⟨M, hM, le⟩ := exists_le_maximal I hI

Result:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Proof state:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
have ⟨a, has, haM⟩ := this

Result:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ ↑M
a : α
has : a ∈ s
haM : a ∉ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
-- Mathlib/Algebra/Algebra/Rat.lean
/-- `nnqsmul` is equal to any other module structure via a cast. -/
lemma cast_smul_eq_nnqsmul [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a

Proof state:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : CharZero R
inst✝² : Semiring S
inst✝¹ : Module ℚ≥0 S
inst✝ : Module R S
q : ℚ≥0
a : S
⊢ ↑q.den • ↑q • a = ↑q.den • q • a

Tactic:
rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, ← smul_assoc,
  nsmul_eq_mul q.den, ← cast_natCast, ← cast_mul, den_mul_eq_num, cast_natCast,
  Nat.cast_smul_eq_nsmul]

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : CharZero R
inst✝² : Semiring S
inst✝¹ : Module ℚ≥0 S
inst✝ : Module R S
q : ℚ≥0
a : S
⊢ (fun x => ↑q.den • x) (↑q • a) = (fun x => ↑q.den • x) (q • a)

Tactic:
dsimp

Result:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : CharZero R
inst✝² : Semiring S
inst✝¹ : Module ℚ≥0 S
inst✝ : Module R S
q : ℚ≥0
a : S
⊢ ↑q.den • ↑q • a = ↑q.den • q • a

Proof state:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : CharZero R
inst✝² : Semiring S
inst✝¹ : Module ℚ≥0 S
inst✝ : Module R S
q : ℚ≥0
a : S
⊢ ↑q • a = q • a

Tactic:
refine MulAction.injective₀ (G₀ := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_

Result:
R : Type u_2
S : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : CharZero R
inst✝² : Semiring S
inst✝¹ : Module ℚ≥0 S
inst✝ : Module R S
q : ℚ≥0
a : S
⊢ (fun x => ↑q.den • x) (↑q • a) = (fun x => ↑q.den • x) (q • a)
-- Mathlib/Probability/Martingale/Basic.lean
theorem submartingale_of_condExp_sub_nonneg_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ}
    (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
    (hf : ∀ i, 0 ≤ᵐ[μ] μ[f (i + 1) - f i|𝒢 i]) : Submartingale f 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]
⊢ Submartingale f 𝒢 μ

Tactic:
refine submartingale_nat hadp hint fun i => ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]
i : ℕ
⊢ f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i] - μ[f i|↑𝒢 i]

Tactic:
exact EventuallyLE.trans (hf i) (condExp_sub (hint _) (hint _) _).le

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]
i : ℕ
⊢ f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]

Tactic:
rw [← condExp_of_stronglyMeasurable (𝒢.le _) (hadp _) (hint _), ← eventually_sub_nonneg]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i] - μ[f i|↑𝒢 i]
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDerivWithin_eq_iterate {x : 𝕜} :
    iteratedDerivWithin n f s x = (fun g : 𝕜 → F => derivWithin g s)^[n] f x

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n f s) s x = ((fun g => derivWithin g s) ∘ (fun g => derivWithin g s)^[n]) f x

Tactic:
exact derivWithin_congr (fun y hy => IH) IH

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x

Tactic:
induction n generalizing x with
| zero => simp
| succ n IH =>
  rw [iteratedDerivWithin_succ, Function.iterate_succ']
  exact derivWithin_congr (fun y hy => IH) IH

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f s x = (fun g => derivWithin g s)^[n + 1] f x

Tactic:
rw [iteratedDerivWithin_succ, Function.iterate_succ']

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n f s) s x = ((fun g => derivWithin g s) ∘ (fun g => derivWithin g s)^[n]) f x

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin 0 f s x = (fun g => derivWithin g s)^[0] f x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cons_append (x : BitVec w₁) (y : BitVec w₂) (a : Bool) :
    (cons a x) ++ y = (cons a (x ++ y)).cast (by omega)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
a : Bool
⊢ w₁ + w₂ + 1 = w₁ + 1 + w₂

Tactic:
omega

Result:
no goals

Proof state:
case a
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
a : Bool
⊢ (a.toNat <<< w₁ ||| x.toNat) <<< w₂ ||| y.toNat = a.toNat <<< (w₁ + w₂) ||| (x.toNat <<< w₂ ||| y.toNat)

Tactic:
rw [Nat.shiftLeft_add, Nat.shiftLeft_or_distrib, Nat.or_assoc]

Result:
no goals

Proof state:
case a
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
a : Bool
⊢ (cons a x ++ y).toNat = (BitVec.cast ⋯ (cons a (x ++ y))).toNat

Tactic:
simp only [toNat_append, toNat_cons, toNat_cast]

Result:
case a
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
a : Bool
⊢ (a.toNat <<< w₁ ||| x.toNat) <<< w₂ ||| y.toNat = a.toNat <<< (w₁ + w₂) ||| (x.toNat <<< w₂ ||| y.toNat)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
a : Bool
⊢ cons a x ++ y = BitVec.cast ⋯ (cons a (x ++ y))

Tactic:
apply eq_of_toNat_eq

Result:
case a
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
a : Bool
⊢ (cons a x ++ y).toNat = (BitVec.cast ⋯ (cons a (x ++ y))).toNat
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem apply_bucket_with_proof {γ : α → Type w} [BEq α] [Hashable α] [PartialEquivBEq α]
    [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) (a : α)
    (f : (a : α) → (l : AssocList α β) → l.contains a → γ a)
    (g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l → γ a)
    (hfg : ∀ {a l h}, f a l h = g a l.toList (AssocList.contains_eq.symm.trans h))
    (hg₁ : ∀ {l l' a h}, DistinctKeys l → (hl' : Perm l l') →
      g a l h = g a l' ((List.containsKey_of_perm hl').symm.trans h)) {h h'}
    (hg₂ : ∀ {l l' a h}, (hl' : containsKey a l' = false) →
      g a (l ++ l') h = g a l ((List.containsKey_append_of_not_contains_right hl').symm.trans h)) :
    f a (bucket m.1.buckets m.2 a) h = g a (toListModel m.1.buckets) h'

Proof state:
case intro.intro
α : Type u
β : α → Type v
γ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a
g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l = true → γ a
hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯
hg₁ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a l = true},
    DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯
h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true
h' : containsKey a (toListModel m.val.buckets) = true
hg₂ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false),
    g a (l ++ l') h = g a l ⋯
l : List ((a : α) × β a)
hl : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
hlk : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ f a (bucket m.val.buckets ⋯ a) h = g a (toListModel m.val.buckets) h'

Tactic:
refine Eq.trans ?_ (hg₁ hm.distinct hl).symm

Result:
case intro.intro
α : Type u
β : α → Type v
γ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
f : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a
g : (a : α) → (l : List ((a : α) × β a)) → containsKey a l = true → γ a
hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯
hg₁ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a l = true},
    DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯
h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true
h' : containsKey a (toListModel m.val.buckets) = true
hg₂ :
  ∀ {l l' : List ((a : α) × β a)} {a : α} {h : containsKey a (l ++ l') = true} (hl' : containsKey a l' = false),
    g a (l ++ l') h = g a l ⋯
l : List ((a : α) × β a)
hl : (toListModel m.val.buckets).Perm ((bucket m.val.buckets ⋯ a).toList ++ l)
hlk : ∀ [inst : LawfulHashable α], IsHashSelf m.val.buckets → ∀ (k' : α), hash a = hash k' → containsKey k' l = false
⊢ f a (bucket m.val.buckets ⋯ a) h = g a ((bucket m.val.buckets ⋯ a).toList ++ l) ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem le_add_of_sub_le {a b c : Nat} (h : a - b ≤ c) : a ≤ c + b

Proof state:
a b c : Nat
h : a - b ≤ c
d : Nat
hd : a - b + d = c
hge : b ≤ a
⊢ a + d = c + b

Tactic:
rw [Nat.add_comm, ← Nat.add_sub_assoc hge] at hd

Result:
a b c : Nat
h : a - b ≤ c
d : Nat
hd : d + a - b = c
hge : b ≤ a
⊢ a + d = c + b

Proof state:
a b c : Nat
h : a - b ≤ c
⊢ a ≤ c + b

Tactic:
match le.dest h, Nat.le_total a b with
| _, Or.inl hle =>
  exact Nat.le_trans hle (Nat.le_add_left ..)
| ⟨d, hd⟩, Or.inr hge =>
  apply @le.intro _ _ d
  rw [Nat.add_comm, ← Nat.add_sub_assoc hge] at hd
  have hd := Nat.eq_add_of_sub_eq (Nat.le_trans hge (Nat.le_add_left ..)) hd
  rw [Nat.add_comm, hd]

Result:
no goals

Proof state:
a b c : Nat
h : a - b ≤ c
d : Nat
hd✝ : d + a - b = c
hge : b ≤ a
hd : d + a = c + b
⊢ a + d = c + b

Tactic:
rw [Nat.add_comm, hd]

Result:
no goals

Proof state:
a b c : Nat
h : a - b ≤ c
d : Nat
hd : d + a - b = c
hge : b ≤ a
⊢ a + d = c + b

Tactic:
have hd := Nat.eq_add_of_sub_eq (Nat.le_trans hge (Nat.le_add_left ..)) hd

Result:
a b c : Nat
h : a - b ≤ c
d : Nat
hd✝ : d + a - b = c
hge : b ≤ a
hd : d + a = c + b
⊢ a + d = c + b

Proof state:
a b c : Nat
h : a - b ≤ c
d : Nat
hd : a - b + d = c
hge : b ≤ a
⊢ a ≤ c + b

Tactic:
apply @le.intro _ _ d

Result:
a b c : Nat
h : a - b ≤ c
d : Nat
hd : a - b + d = c
hge : b ≤ a
⊢ a + d = c + b

Proof state:
a b c : Nat
h : a - b ≤ c
x✝ : Exists fun k => a - b + k = c
hle : a ≤ b
⊢ a ≤ c + b

Tactic:
exact Nat.le_trans hle (Nat.le_add_left ..)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem forall_lt_succ_left {p : Nat → Prop} :
    (∀ m, m < n + 1 → p m) ↔ p 0 ∧ (∀ m, m < n → p (m + 1))

Proof state:
n : Nat
p : Nat → Prop
⊢ (∀ (m : Nat), m < n + 1 → p m) ↔ p 0 ∧ ∀ (m : Nat), m < n → p (m + 1)

Tactic:
simpa using forall_lt_succ_left' (p := fun m _ => p m)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} :
    (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l₁ l₂ : List α
⊢ mapM f (l₁ ++ l₂) = do
    let __do_lift ← mapM f l₁
    let __do_lift_1 ← mapM f l₂
    pure (__do_lift ++ __do_lift_1)

Tactic:
induction l₁ <;> simp [*]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem mem_idealSet :
    x ∈ idealSet K J ↔ x ∈ fundamentalCone K ∧ ∃ a : (𝓞 K), (a : 𝓞 K) ∈ (J : Set (𝓞 K)) ∧
      mixedEmbedding K (a : 𝓞 K) = x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ x ∈ idealSet K J ↔ x ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x

Tactic:
simp_rw [idealSet, Set.mem_inter_iff, idealLattice, SetLike.mem_coe, FractionalIdeal.coe_mk0,
  LinearMap.mem_range, LinearMap.coe_comp, LinearMap.coe_restrictScalars, coe_subtype,
  Function.comp_apply, AlgHom.toLinearMap_apply, RingHom.toIntAlgHom_coe, Subtype.exists,
  FractionalIdeal.mem_coe, FractionalIdeal.mem_coeIdeal, exists_prop', nonempty_prop,
  exists_exists_and_eq_and]

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lq (hpq : p.IsConjExponent q) :
    ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
by_cases H : (∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0

Result:
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
H : ¬((∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0)
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Proof state:
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = ⊤
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
rcases H' with H' | H' <;> simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]

Result:
no goals

Proof state:
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤
this :
  ↑(∑ i ∈ s, (fun i => (f i).toNNReal) i * (fun i => (g i).toNNReal) i) ≤
    ↑((∑ i ∈ s, (fun i => (f i).toNNReal) i ^ p) ^ (1 / p) * (∑ i ∈ s, (fun i => (g i).toNNReal) i ^ q) ^ (1 / q))
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
simp [ENNReal.coe_rpow_of_nonneg, hpq.pos.le, hpq.one_div_pos.le, hpq.symm.pos.le,
  hpq.symm.one_div_pos.le] at this

Result:
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤
this :
  ∑ x ∈ s, ↑(f x).toNNReal * ↑(g x).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
theorem integrable_of_nnreal [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) :
    Integrable (((↑) : ℝ≥0 → ℝ) ∘ ⇑f) μ

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (a : X), ↑(f a) ∂μ < ⊤

Tactic:
exact lintegral_lt_top_of_nnreal _ f

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Integrable (NNReal.toReal ∘ ⇑f) μ

Tactic:
refine ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ HasFiniteIntegral (NNReal.toReal ∘ ⇑f) μ

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ HasFiniteIntegral (NNReal.toReal ∘ ⇑f) μ

Tactic:
simp only [hasFiniteIntegral_iff_enorm, Function.comp_apply, NNReal.enorm_eq]

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (a : X), ↑(f a) ∂μ < ⊤
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem mul_edgeDensity_le_edgeDensity (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty)
    (ht₂ : t₂.Nonempty) :
    (#s₂ : ℚ) / #s₁ * (#t₂ / #t₁) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁

Tactic:
have hst : (#s₂ : ℚ) * #t₂ ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁

Tactic:
rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel₀ hst]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ ↑(#(interedges r s₂ t₂)) / (↑(#s₁) * ↑(#t₁)) ≤ ↑(#(interedges r s₁ t₁)) / (↑(#s₁) * ↑(#t₁))

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ ↑(#s₂) * ↑(#t₂) ≠ 0

Tactic:
simp [hs₂.ne_empty, ht₂.ne_empty]

Result:
no goals

Proof state:
case hab.h.a
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ interedges r s₂ t₂ ⊆ interedges r s₁ t₁

Tactic:
exact interedges_mono hs ht

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ ↑(#(interedges r s₂ t₂)) / (↑(#s₁) * ↑(#t₁)) ≤ ↑(#(interedges r s₁ t₁)) / (↑(#s₁) * ↑(#t₁))

Tactic:
gcongr

Result:
case hab.h.a
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ interedges r s₂ t₂ ⊆ interedges r s₁ t₁