harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_nonneg_iff_sign_nonneg {θ : Angle} : 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

Proof state:
case inr.inl
θ : Angle
h : θ.toReal = 0
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

Tactic:
simp [h, sign, ← sin_toReal]

Result:
no goals

Proof state:
case inr.inr
θ : Angle
h : 0 < θ.toReal
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

Tactic:
refine ⟨fun _ => ?_, fun _ => h.le⟩

Result:
case inr.inr
θ : Angle
h : 0 < θ.toReal
x✝ : 0 ≤ θ.toReal
⊢ 0 ≤ θ.sign

Proof state:
θ : Angle
h : θ.toReal < 0
hn : 0 ≤ -1
⊢ -1 < 0

Tactic:
decide

Result:
no goals

Proof state:
case inl
θ : Angle
h : θ.toReal < 0
hn : 0 ≤ -1
⊢ 0 ≤ θ.toReal

Tactic:
exact False.elim (hn.not_lt (by decide))

Result:
no goals

Proof state:
case inr.inr
θ : Angle
h : 0 < θ.toReal
x✝ : 0 ≤ θ.toReal
⊢ 0 ≤ Real.sin θ.toReal

Tactic:
exact sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)

Result:
no goals

Proof state:
θ : Angle
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

Tactic:
rcases lt_trichotomy θ.toReal 0 with (h | h | h)

Result:
case inl
θ : Angle
h : θ.toReal < 0
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

case inr.inl
θ : Angle
h : θ.toReal = 0
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

case inr.inr
θ : Angle
h : 0 < θ.toReal
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

Proof state:
case inr.inr
θ : Angle
h : 0 < θ.toReal
x✝ : 0 ≤ θ.toReal
⊢ 0 ≤ θ.sign

Tactic:
rw [sign, ← sin_toReal, sign_nonneg_iff]

Result:
case inr.inr
θ : Angle
h : 0 < θ.toReal
x✝ : 0 ≤ θ.toReal
⊢ 0 ≤ Real.sin θ.toReal

Proof state:
case inl
θ : Angle
h : θ.toReal < 0
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

Tactic:
refine ⟨fun hn => False.elim (h.not_le hn), fun hn => ?_⟩

Result:
case inl
θ : Angle
h : θ.toReal < 0
hn : 0 ≤ θ.sign
⊢ 0 ≤ θ.toReal

Proof state:
case inl
θ : Angle
h : θ.toReal < 0
hn : 0 ≤ θ.sign
⊢ 0 ≤ θ.toReal

Tactic:
rw [toReal_neg_iff_sign_neg.1 h] at hn

Result:
case inl
θ : Angle
h : θ.toReal < 0
hn : 0 ≤ -1
⊢ 0 ≤ θ.toReal
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => pow_lt_ascFactorial' n k

Proof state:
n : ℕ
⊢ 2 ≤ 0 → (n + 1) ^ 0 < (n + 1).ascFactorial 0

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
n : ℕ
⊢ 2 ≤ 1 → (n + 1) ^ 1 < (n + 1).ascFactorial 1

Tactic:
intro

Result:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < (n + 1).ascFactorial 1

Proof state:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < (n + 1).ascFactorial 1

Tactic:
contradiction

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_comm (a b) : a ⨳ b = b ⨳ a

Proof state:
case e_a.h.mpr
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ c ⨳ b ♯ a ⨳ d < x ♯ c ⨳ d

Tactic:
rw [nadd_comm, nmul_comm, nmul_comm c, nmul_comm c]

Result:
case e_a.h.mpr
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ d ⨳ a ♯ b ⨳ c < x ♯ d ⨳ c

Proof state:
case e_a.h.mp
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ d ⨳ b ♯ a ⨳ c < x ♯ d ⨳ c

Tactic:
exact H _ hd _ hc

Result:
no goals

Proof state:
case e_a.h.mpr
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ d ⨳ a ♯ b ⨳ c < x ♯ d ⨳ c

Tactic:
exact H _ hd _ hc

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
⊢ sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} =
    sInf {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}

Tactic:
congr

Result:
case e_a
a b : Ordinal.{u_1}
⊢ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} = {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}

Proof state:
case e_a.h.mp
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ c ⨳ a ♯ b ⨳ d < x ♯ c ⨳ d

Tactic:
rw [nadd_comm, ← nmul_comm, ← nmul_comm a, ← nmul_comm d]

Result:
case e_a.h.mp
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ d ⨳ b ♯ a ⨳ c < x ♯ d ⨳ c

Proof state:
case e_a
a b : Ordinal.{u_1}
⊢ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} = {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}

Tactic:
ext x

Result:
case e_a.h
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ↔
    x ∈ {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}

Proof state:
case e_a.h
a b x : Ordinal.{u_1}
⊢ x ∈ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} ↔
    x ∈ {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}

Tactic:
constructor <;> intro H c hc d hd

Result:
case e_a.h.mp
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < b
d : Ordinal.{u_1}
hd : d < a
⊢ c ⨳ a ♯ b ⨳ d < x ♯ c ⨳ d

case e_a.h.mpr
a b x : Ordinal.{u_1}
H : x ∈ {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
⊢ c ⨳ b ♯ a ⨳ d < x ♯ c ⨳ d

Proof state:
a b : Ordinal.{u_1}
⊢ a ⨳ b = b ⨳ a

Tactic:
rw [nmul, nmul]

Result:
a b : Ordinal.{u_1}
⊢ sInf {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'} =
    sInf {c | ∀ a' < b, ∀ b' < a, a' ⨳ a ♯ b ⨳ b' < c ♯ a' ⨳ b'}
-- Mathlib/GroupTheory/PGroup.lean
theorem card_orbit (a : α) [Finite (orbit G a)] : ∃ n : ℕ, Nat.card (orbit G a) = p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Tactic:
haveI := Finite.of_equiv (orbit G a) ϕ

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this : Finite (G ⧸ stabilizer G a)
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Tactic:
let ϕ := orbitEquivQuotientStabilizer G a

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this : Finite (G ⧸ stabilizer G a)
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Tactic:
haveI := (stabilizer G a).finiteIndex_of_finite_quotient

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Finite (G ⧸ stabilizer G a)
this : (stabilizer G a).FiniteIndex
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Finite (G ⧸ stabilizer G a)
this : (stabilizer G a).FiniteIndex
⊢ ∃ n, Nat.card ↑(orbit G a) = p ^ n

Tactic:
rw [Nat.card_congr ϕ]

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Finite (G ⧸ stabilizer G a)
this : (stabilizer G a).FiniteIndex
⊢ ∃ n, Nat.card (G ⧸ stabilizer G a) = p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Finite ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Finite (G ⧸ stabilizer G a)
this : (stabilizer G a).FiniteIndex
⊢ ∃ n, Nat.card (G ⧸ stabilizer G a) = p ^ n

Tactic:
exact hG.index (stabilizer G a)

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem aemeasurable {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
    (hu : IsUniform X s ℙ μ) : AEMeasurable X ℙ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
⊢ AEMeasurable X ℙ

Tactic:
dsimp [IsUniform, ProbabilityTheory.cond] at hu

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s
⊢ AEMeasurable X ℙ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ 0 Set.univ = 1

Tactic:
rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False

Tactic:
rw [map_of_not_aemeasurable h] at hu

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s
⊢ AEMeasurable X ℙ

Tactic:
by_contra h

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False

Tactic:
apply zero_ne_one' ℝ≥0∞

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ 0 = 1

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ 0 = 1

Tactic:
calc
  0 = (0 : Measure E) Set.univ := rfl
  _ = _ := by rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
    Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem exists_cycleOn (s : Finset α) :
    ∃ f : Perm α, f.IsCycleOn s ∧ f.support ⊆ s

Proof state:
case h.e'_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ↑s = {a | a ∈ s.toList}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ∃ f, f.IsCycleOn ↑s ∧ f.support ⊆ s

Tactic:
refine ⟨s.toList.formPerm, ?_, fun x hx => by
  simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)⟩

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ s.toList.formPerm.IsCycleOn ↑s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ s.toList.formPerm.IsCycleOn ↑s

Tactic:
convert s.nodup_toList.isCycleOn_formPerm

Result:
case h.e'_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ↑s = {a | a ∈ s.toList}

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
x : α
hx : x ∈ s.toList.formPerm.support
⊢ x ∈ s

Tactic:
simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem zero_memℓp : Memℓp (0 : ∀ i, E i) p

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 0

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ⊤

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p

Proof state:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Summable fun i => ‖0 i‖ ^ p.toReal

Tactic:
simp [Real.zero_rpow hp.ne', summable_zero]

Result:
no goals

Proof state:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ {i | 0 i ≠ 0}.Finite

Tactic:
simp

Result:
no goals

Proof state:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ⊤

Tactic:
apply memℓp_infty

Result:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (Set.range fun i => ‖0 i‖)

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 0

Tactic:
apply memℓp_zero

Result:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ {i | 0 i ≠ 0}.Finite

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p

Tactic:
apply memℓp_gen

Result:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Summable fun i => ‖0 i‖ ^ p.toReal

Proof state:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (Set.range fun i => 0)

Tactic:
exact bddAbove_singleton.mono Set.range_const_subset

Result:
no goals

Proof state:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (Set.range fun i => ‖0 i‖)

Tactic:
simp only [norm_zero, Pi.zero_apply]

Result:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (Set.range fun i => 0)
-- Mathlib/Topology/Separation/Basic.lean
theorem R1Space.sInf {X : Type*} {T : Set (TopologicalSpace X)}
    (hT : ∀ t ∈ T, @R1Space X t) : @R1Space X (sInf T)

Proof state:
case inl.intro.intro
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
t : TopologicalSpace X
htT : t ∈ T
htd : Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
exact .inr <| htd.mono (iInf₂_le t htT) (iInf₂_le t htT)

Result:
no goals

Proof state:
case inr
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∀ t ∈ T, ¬Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
exact .inl <| iInf₂_mono fun t ht ↦ ((hT t ht).1 x y).resolve_right (hTd t ht)

Result:
no goals

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
⊢ R1Space X

Tactic:
refine ⟨fun x y ↦ ?_⟩

Result:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
rcases em (∃ t ∈ T, Disjoint (@nhds X t x) (@nhds X t y)) with ⟨t, htT, htd⟩ | hTd

Result:
case inl.intro.intro
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
t : TopologicalSpace X
htT : t ∈ T
htd : Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

case inr
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ¬∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Proof state:
case inr
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ¬∃ t ∈ T, Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Tactic:
push_neg at hTd

Result:
case inr
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
hTd : ∀ t ∈ T, ¬Disjoint (𝓝 x) (𝓝 y)
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
⊢ R1Space X

Tactic:
let _ := sInf T

Result:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
⊢ R1Space X

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)

Tactic:
simp only [Specializes, nhds_sInf]

Result:
X : Type u_3
T : Set (TopologicalSpace X)
hT : ∀ t ∈ T, R1Space X
x✝ : TopologicalSpace X := sInf T
x y : X
⊢ ⨅ t ∈ T, 𝓝 x ≤ ⨅ t ∈ T, 𝓝 y ∨ Disjoint (⨅ t ∈ T, 𝓝 x) (⨅ t ∈ T, 𝓝 y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_tdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b).tdiv b = a :=
  have : ∀ {a b : Nat}, (b : Int) ≠ 0 → (tdiv (a * b) b : Int) = a := fun H => by
    rw [← ofNat_mul, ← ofNat_tdiv,
      Nat.mul_div_cancel _ <| Nat.pos_of_ne_zero <| Int.ofNat_ne_zero.1 H]
  match a, b, a.eq_nat_or_neg, b.eq_nat_or_neg with
  | _, _, ⟨a, .inl rfl⟩, ⟨b, .inl rfl⟩ => this H
  | _, _, ⟨a, .inl rfl⟩, ⟨b, .inr rfl⟩ => by
    rw [Int.mul_neg, Int.neg_tdiv, Int.tdiv_neg, Int.neg_neg,
      this (Int.neg_ne_zero.1 H)]
  | _, _, ⟨a, .inr rfl⟩, ⟨b, .inl rfl⟩ => by rw [Int.neg_mul, Int.neg_tdiv, this H]
  | _, _, ⟨a, .inr rfl⟩, ⟨b, .inr rfl⟩ => by
    rw [Int.neg_mul_neg, Int.tdiv_neg, this (Int.neg_ne_zero.1 H)]

Proof state:
a b : Int
H✝ : b ≠ 0
a✝ b✝ : Nat
H : ↑b✝ ≠ 0
⊢ (↑a✝ * ↑b✝).tdiv ↑b✝ = ↑a✝

Tactic:
rw [← ofNat_mul, ← ofNat_tdiv,
  Nat.mul_div_cancel _ <| Nat.pos_of_ne_zero <| Int.ofNat_ne_zero.1 H]

Result:
no goals

Proof state:
a✝ b✝ : Int
this : ∀ {a b : Nat}, ↑b ≠ 0 → (↑a * ↑b).tdiv ↑b = ↑a
a b : Nat
H : -↑b ≠ 0
⊢ (-↑a * -↑b).tdiv (-↑b) = -↑a

Tactic:
rw [Int.neg_mul_neg, Int.tdiv_neg, this (Int.neg_ne_zero.1 H)]

Result:
no goals

Proof state:
a✝ b✝ : Int
this : ∀ {a b : Nat}, ↑b ≠ 0 → (↑a * ↑b).tdiv ↑b = ↑a
a b : Nat
H : -↑b ≠ 0
⊢ (↑a * -↑b).tdiv (-↑b) = ↑a

Tactic:
rw [Int.mul_neg, Int.neg_tdiv, Int.tdiv_neg, Int.neg_neg,
  this (Int.neg_ne_zero.1 H)]

Result:
no goals

Proof state:
a✝ b✝ : Int
this : ∀ {a b : Nat}, ↑b ≠ 0 → (↑a * ↑b).tdiv ↑b = ↑a
a b : Nat
H : ↑b ≠ 0
⊢ (-↑a * ↑b).tdiv ↑b = -↑a

Tactic:
rw [Int.neg_mul, Int.neg_tdiv, this H]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- We have that `λ` divides `x * (x - 1) * (x - (η + 1))`. -/
lemma lambda_dvd_mul_sub_one_mul_sub_eta_add_one : λ ∣ x * (x - 1) * (x - (η + 1))

Proof state:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x * (x - 1) * (x - (↑η + 1))

Tactic:
refine dvd_mul_of_dvd_right ?_ _

Result:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x - (↑η + 1)

Proof state:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x + 1 - (↑η - 1 + 3)

Tactic:
exact dvd_sub h <| dvd_add dvd_rfl hζ.toInteger_sub_one_dvd_prime'

Result:
no goals

Proof state:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x - (↑η + 1)

Tactic:
rw [show x - (η + 1) = x + 1 - (η - 1 + 3) by ring]

Result:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x + 1 - (↑η - 1 + 3)

Proof state:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x
⊢ λ ∣ x * (x - 1) * (x - (↑η + 1))

Tactic:
exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h _) _

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ∣ x * (x - 1) * (x - (↑η + 1))

Tactic:
rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h

Result:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x
⊢ λ ∣ x * (x - 1) * (x - (↑η + 1))

case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - (↑η + 1))

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x * (x - 1) * (x - (↑η + 1))

Proof state:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - (↑η + 1))

Tactic:
exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h _) _

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ x - (↑η + 1) = x + 1 - (↑η - 1 + 3)

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_left_sum {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι}
    {i : ι} (hi : i ∈ s) : ⟪∑ i ∈ s, l i • v i, v i⟫ = conj (l i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ inner (∑ i ∈ s, l i • v i) (v i) = (starRingEnd 𝕜) (l i)

Tactic:
classical
simp only [sum_inner, inner_smul_left, orthonormal_iff_ite.mp hv, hi, mul_boole,
  Finset.sum_ite_eq', if_true]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ inner (∑ i ∈ s, l i • v i) (v i) = (starRingEnd 𝕜) (l i)

Tactic:
simp only [sum_inner, inner_smul_left, orthonormal_iff_ite.mp hv, hi, mul_boole,
  Finset.sum_ite_eq', if_true]

Result:
no goals