harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem posSemidef_conjTranspose_mul_self [StarOrderedRing R] (A : Matrix m n R) :
    PosSemidef (Aᴴ * A)

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ 0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x

Tactic:
rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]

Result:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ 0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x

Tactic:
exact Finset.sum_nonneg fun i _ => star_mul_self_nonneg _

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (Aᴴ * A).PosSemidef

Tactic:
refine ⟨isHermitian_transpose_mul_self _, fun x => ?_⟩

Result:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
x : n → R
⊢ 0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x
-- Mathlib/Data/ENNReal/Order.lean
theorem le_toReal_sub {a b : ℝ≥0∞} (hb : b ≠ ∞) : a.toReal - b.toReal ≤ (a - b).toReal

Proof state:
case intro
a : ℝ≥0∞
b : ℝ≥0
⊢ a.toReal - (↑b).toReal ≤ (a - ↑b).toReal

Tactic:
induction a

Result:
case intro.top
b : ℝ≥0
⊢ ⊤.toReal - (↑b).toReal ≤ (⊤ - ↑b).toReal

case intro.coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal

Proof state:
a b : ℝ≥0∞
hb : b ≠ ⊤
⊢ a.toReal - b.toReal ≤ (a - b).toReal

Tactic:
lift b to ℝ≥0 using hb

Result:
case intro
a : ℝ≥0∞
b : ℝ≥0
⊢ a.toReal - (↑b).toReal ≤ (a - ↑b).toReal

Proof state:
case intro.coe
b x✝ : ℝ≥0
⊢ ↑x✝ - ↑b ≤ (↑x✝ - ↑b) ⊔ 0

Tactic:
exact le_max_left _ _

Result:
no goals

Proof state:
case intro.top
b : ℝ≥0
⊢ ⊤.toReal - (↑b).toReal ≤ (⊤ - ↑b).toReal

Tactic:
simp

Result:
no goals

Proof state:
case intro.coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal

Tactic:
simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]

Result:
case intro.coe
b x✝ : ℝ≥0
⊢ ↑x✝ - ↑b ≤ (↑x✝ - ↑b) ⊔ 0
-- Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
theorem Walk.three_le_chromaticNumber_of_odd_loop {α} {G : SimpleGraph α} {u : α} (p : G.Walk u u)
    (hOdd : Odd p.length) : 3 ≤ G.chromaticNumber := Classical.by_contradiction <| by
  intro h
  have h' : G.chromaticNumber ≤ 2 := Order.le_of_lt_add_one <| not_le.mp h
  let c : G.Coloring (Fin 2) := (chromaticNumber_le_iff_colorable.mp h').some
  let c' : G.Coloring Bool := recolorOfEquiv G finTwoEquiv c
  have : ¬c' u ↔ c' u := (c'.odd_length_iff_not_congr p).mp hOdd
  simp_all

Proof state:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
⊢ False

Tactic:
let c' : G.Coloring Bool := recolorOfEquiv G finTwoEquiv c

Result:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c
⊢ False

Tactic:
have : ¬c' u ↔ c' u := (c'.odd_length_iff_not_congr p).mp hOdd

Result:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c
this : ¬c' u = true ↔ c' u = true
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
⊢ False

Tactic:
have h' : G.chromaticNumber ≤ 2 := Order.le_of_lt_add_one <| not_le.mp h

Result:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
⊢ False

Tactic:
let c : G.Coloring (Fin 2) := (chromaticNumber_le_iff_colorable.mp h').some

Result:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c
this : ¬c' u = true ↔ c' u = true
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
⊢ ¬3 ≤ G.chromaticNumber → False

Tactic:
intro h

Result:
α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
⊢ False
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_right_mono₀ (ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 1 ≤ a
⊢ Monotone fun n => a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a

Tactic:
exact le_mul_of_one_le_right (zpow_nonneg (zero_le_one.trans ha) _) ha

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [zpow_add_one₀ (zero_lt_one.trans_le ha).ne']

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a
-- Mathlib/Data/List/Sigma.lean
theorem NodupKeys.kunion (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) : (kunion l₁ l₂).NodupKeys

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₁ : (s :: l₁).NodupKeys
nd₂ : l₂.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys

Tactic:
simp? at nd₁ says simp only [nodupKeys_cons] at nd₁

Result:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₂ : l₂.NodupKeys
nd₁ : s.fst ∉ l₁.keys ∧ l₁.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₁ : (s :: l₁).NodupKeys
nd₂ : l₂.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys

Tactic:
simp only [nodupKeys_cons] at nd₁

Result:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₂ : l₂.NodupKeys
nd₁ : s.fst ∉ l₁.keys ∧ l₁.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₂ : l₂.NodupKeys
nd₁ : s.fst ∉ l₁.keys ∧ l₁.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys

Tactic:
simp [not_or, nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
nd₁ : l₁.NodupKeys
nd₂ : l₂.NodupKeys
⊢ (l₁.kunion l₂).NodupKeys

Tactic:
induction l₁ generalizing l₂ with
| nil => simp only [nil_kunion, nd₂]
| cons s l₁ ih =>
  simp? at nd₁ says simp only [nodupKeys_cons] at nd₁
  simp [not_or, nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
nd₁ : [].NodupKeys
nd₂ : l₂.NodupKeys
⊢ ([].kunion l₂).NodupKeys

Tactic:
simp only [nil_kunion, nd₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
    (m.insert k v).contains a = (k == a || m.contains a)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a k : α
v : β k
⊢ (m.insert k v).contains a = (k == a || m.contains a)

Tactic:
simp_to_raw using Raw₀.contains_insert

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem or_exists_of_exists_mem_cons {p : α → Prop} {a : α} {l : List α} : (∃ x ∈ a :: l, p x) →
    p a ∨ ∃ x ∈ l, p x :=
  fun ⟨x, xal, px⟩ =>
    Or.elim (eq_or_mem_of_mem_cons xal) (fun h : x = a => by rw [← h]; left; exact px)
      fun h : x ∈ l => Or.inr ⟨x, h, px⟩

Proof state:
α : Type u
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
xal : x ∈ a :: l
px : p x
h : x = a
⊢ p a ∨ ∃ x, x ∈ l ∧ p x

Tactic:
rw [← h]

Result:
α : Type u
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
xal : x ∈ a :: l
px : p x
h : x = a
⊢ p x ∨ ∃ x, x ∈ l ∧ p x

Proof state:
case h
α : Type u
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
xal : x ∈ a :: l
px : p x
h : x = a
⊢ p x

Tactic:
exact px

Result:
no goals

Proof state:
α : Type u
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
xal : x ∈ a :: l
px : p x
h : x = a
⊢ p x ∨ ∃ x, x ∈ l ∧ p x

Tactic:
left

Result:
case h
α : Type u
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
xal : x ∈ a :: l
px : p x
h : x = a
⊢ p x
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma hasSum_int_cosKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
    HasSum (fun n : ℤ ↦ cexp (2 * π * I * a * n) * rexp (-π * n ^ 2 * t)) ↑(cosKernel a t)

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(cosKernel (↑a) t)

Tactic:
rw [cosKernel_def a t]

Result:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))

Proof state:
a t : ℝ
ht : 0 < t
this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)
⊢ 0 < (I * ↑t).im

Tactic:
simpa

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))

Tactic:
simpa [this] using hasSum_jacobiTheta₂_term _ (by simpa)

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (↑π * I * ↑a * ↑n * 2 - ↑π * ↑n ^ 2 * ↑t) = cexp (↑π * I * ↑a * ↑n * 2 + ↑π * I ^ 2 * ↑n ^ 2 * ↑t)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))

Tactic:
have (n : ℤ) : cexp (2 * π * I * a * n) * cexp (-(π * n ^ 2 * t)) =
    jacobiTheta₂_term n a (I * ↑t) := by
  rw [jacobiTheta₂_term, ← Complex.exp_add]
  ring_nf
  simp [sub_eq_add_neg]

Result:
a t : ℝ
ht : 0 < t
this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))

Proof state:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)

Tactic:
rw [jacobiTheta₂_term, ← Complex.exp_add]

Result:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n + -(↑π * ↑n ^ 2 * ↑t)) = cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))

Proof state:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n + -(↑π * ↑n ^ 2 * ↑t)) = cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))

Tactic:
ring_nf

Result:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (↑π * I * ↑a * ↑n * 2 - ↑π * ↑n ^ 2 * ↑t) = cexp (↑π * I * ↑a * ↑n * 2 + ↑π * I ^ 2 * ↑n ^ 2 * ↑t)
-- Mathlib/Analysis/PSeries.lean
theorem summable_condensed_iff {f : ℕ → ℝ≥0} (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) :
    (Summable fun k : ℕ => (2 : ℝ≥0) ^ k * f (2 ^ k)) ↔ Summable f

Proof state:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x
⊢ (Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
convert summable_schlomilch_iff hf (pow_pos zero_lt_two) (pow_right_strictMono₀ _root_.one_lt_two)
  two_ne_zero h_succ_diff

Result:
case h.e'_1.h.e'_5.h.h.e'_5
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x
x✝ : ℕ
⊢ 2 ^ x✝ = ↑(2 ^ (x✝ + 1)) - ↑(2 ^ x✝)

Proof state:
case h.e'_1.h.e'_5.h.h.e'_5
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x
x✝ : ℕ
⊢ 2 ^ x✝ = ↑(2 ^ (x✝ + 1)) - ↑(2 ^ x✝)

Tactic:
simp [pow_succ, mul_two, two_mul]

Result:
no goals

Proof state:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ SuccDiffBounded 2 fun x => 2 ^ x

Tactic:
intro n

Result:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ (fun x => 2 ^ x) (n + 2) - (fun x => 2 ^ x) (n + 1) ≤ 2 • ((fun x => 2 ^ x) (n + 1) - (fun x => 2 ^ x) n)

Proof state:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ (fun x => 2 ^ x) (n + 2) - (fun x => 2 ^ x) (n + 1) ≤ 2 • ((fun x => 2 ^ x) (n + 1) - (fun x => 2 ^ x) n)

Tactic:
simp [pow_succ, mul_two, two_mul]

Result:
no goals
-- Mathlib/Data/Real/Pointwise.lean
theorem Real.iSup_mul_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (⨆ i, f i) * r = ⨅ i, f i * r

Proof state:
ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨆ i, f i) * r = ⨅ i, f i * r

Tactic:
simp only [Real.mul_iSup_of_nonpos ha, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem DividedPowers.coe_injective :
    Function.Injective (fun (h : DividedPowers I) ↦ (h : ℕ → A → A)) := fun hI hI' h ↦ by
  ext n x
  exact congr_fun (congr_fun h n) x

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : (fun h => h.dpow) hI = (fun h => h.dpow) hI'
⊢ hI = hI'

Tactic:
ext n x

Result:
case h_eq
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : (fun h => h.dpow) hI = (fun h => h.dpow) hI'
n : ℕ
x : A
x✝ : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x

Proof state:
case h_eq
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : (fun h => h.dpow) hI = (fun h => h.dpow) hI'
n : ℕ
x : A
x✝ : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x

Tactic:
exact congr_fun (congr_fun h n) x

Result:
no goals
-- Mathlib/Algebra/Ring/Center.lean
theorem add_mem_center [Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
    a + b ∈ Set.center M  where
  comm _

Proof state:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (a + b) * x✝ = x✝¹ * ((a + b) * x✝)

Tactic:
rw [mul_add, add_mul, ha.mid_assoc, hb.mid_assoc, ← mul_add, ← add_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * (a + b) = x✝¹ * (x✝ * (a + b))

Tactic:
rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝ : M
⊢ (a + b) * x✝ = x✝ * (a + b)

Tactic:
rw [add_mul, mul_add, ha.comm, hb.comm]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ (a + b) * (x✝¹ * x✝) = (a + b) * x✝¹ * x✝

Tactic:
rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_left_right (H : IsCoprime (x * y) z) : IsCoprime y z

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * x) z
⊢ IsCoprime y z

Tactic:
exact H.of_mul_left_left

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
⊢ IsCoprime y z

Tactic:
rw [mul_comm] at H

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * x) z
⊢ IsCoprime y z
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem lift_of {x : R} : lift i a h x = i x

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
x : R
⊢ (lift i a h) ((of f) x) = i x

Tactic:
rw [← mk_C x, lift_mk, eval₂_C]

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem not_supPrime : ¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
rw [SupPrime, not_and_or]

Result:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
push_neg

Result:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_p : ‖(p : ℚ_[p])‖ = (p : ℝ)⁻¹

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑↑p)⁻¹

Tactic:
rw [← @Rat.cast_natCast ℚ_[p] _ p]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑↑p‖ = (↑↑p)⁻¹

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑p)⁻¹

Tactic:
rw [← @Rat.cast_natCast ℝ _ p]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑↑p)⁻¹

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑↑p‖ = (↑↑p)⁻¹

Tactic:
simp [hp.1.ne_zero, hp.1.ne_one, norm, padicNorm, padicValRat, padicValInt, zpow_neg,
  -Rat.cast_natCast]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_prod {f : γ → β → α} {a : γ → α} {s : Finset γ} :
    (∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i)

Tactic:
exact Finset.induction_on s (by simp only [hasProd_one, prod_empty, forall_true_iff]) <| by
  simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
    prod_insert, and_imp]
  exact fun x s _ IH hx h ↦ hx.mul (IH h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i)

Tactic:
classical
exact Finset.induction_on s (by simp only [hasProd_one, prod_empty, forall_true_iff]) <| by
  simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
    prod_insert, and_imp]
  exact fun x s _ IH hx h ↦ hx.mul (IH h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ ∅, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ ∅, f i b) (∏ i ∈ ∅, a i)

Tactic:
simp only [hasProd_one, prod_empty, forall_true_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i)) →
        (∀ i ∈ insert a_1 s, HasProd (f i) (a i)) →
          HasProd (fun b => ∏ i ∈ insert a_1 s, f i b) (∏ i ∈ insert a_1 s, a i)

Tactic:
simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
  prod_insert, and_imp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i)) →
        HasProd (f a_1) (a a_1) →
          (∀ a_5 ∈ s, HasProd (f a_5) (a a_5)) → HasProd (fun b => f a_1 b * ∏ i ∈ s, f i b) (a a_1 * ∏ i ∈ s, a i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i)) →
        HasProd (f a_1) (a a_1) →
          (∀ a_5 ∈ s, HasProd (f a_5) (a a_5)) → HasProd (fun b => f a_1 b * ∏ i ∈ s, f i b) (a a_1 * ∏ i ∈ s, a i)

Tactic:
exact fun x s _ IH hx h ↦ hx.mul (IH h)

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.topologicalClosure_eq_top_iff [CompleteSpace E] :
    K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮᗮ = ⊤
⊢ Kᗮ = ⊥

Tactic:
rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥

Tactic:
rw [← Submodule.orthogonal_orthogonal_eq_closure]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ = ⊤ ↔ Kᗮ = ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ = ⊤ ↔ Kᗮ = ⊥

Tactic:
constructor <;> intro h

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮᗮ = ⊤
⊢ Kᗮ = ⊥

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤

Tactic:
rw [h, Submodule.bot_orthogonal_eq_top]

Result:
no goals