harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma comp_neg {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : z₁.comp (-z₂) h = -z₁.comp z₂ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (-z₂) h).v p q hpq = (-z₁.comp z₂ h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), neg_v, comp_neg]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (-z₂) h = -z₁.comp z₂ h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (-z₂) h).v p q hpq = (-z₁.comp z₂ h).v p q hpq
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySum_mem {x : K} :
    mixedEmbedding K x ∈ (convexBodySum K B) ↔
      ∑ w : InfinitePlace K, (mult w) * w.val x ≤ B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
⊢ ∑ x_1 : InfinitePlace K, ↑x_1.mult * x_1 x ≤ B ↔ ∑ w : InfinitePlace K, ↑w.mult * ↑w x ≤ B

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
⊢ (mixedEmbedding K) x ∈ convexBodySum K B ↔ ∑ w : InfinitePlace K, ↑w.mult * ↑w x ≤ B

Tactic:
simp_rw [Set.mem_setOf_eq, convexBodySumFun, normAtPlace_apply]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
⊢ ∑ x_1 : InfinitePlace K, ↑x_1.mult * x_1 x ≤ B ↔ ∑ w : InfinitePlace K, ↑w.mult * ↑w x ≤ B
-- Mathlib/Topology/Homeomorph.lean
theorem isQuotientMap (h : X ≃ₜ Y) : IsQuotientMap h :=
  IsQuotientMap.of_comp h.symm.continuous h.continuous <| by
    simp only [self_comp_symm, IsQuotientMap.id]

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ IsQuotientMap (⇑h ∘ ⇑h.symm)

Tactic:
simp only [self_comp_symm, IsQuotientMap.id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n)

Proof state:
s n : Nat
⊢ range' s n = map (fun x => s + x) (range n)

Tactic:
rw [range_eq_range', map_add_range']

Result:
s n : Nat
⊢ range' s n = range' (s + 0) n

Proof state:
s n : Nat
⊢ range' s n = range' (s + 0) n

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem norm_integral_min_max (f : ℝ → E) :
    ‖∫ x in min a b..max a b, f x ∂μ‖ = ‖∫ x in a..b, f x ∂μ‖

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
⊢ ‖∫ (x : ℝ) in a ⊓ b..a ⊔ b, f x ∂μ‖ = ‖∫ (x : ℝ) in a..b, f x ∂μ‖

Tactic:
cases le_total a b <;> simp [*, integral_symm a b]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_eq_cons_digits_div {b n : ℕ} (h : 1 < b) (w : n ≠ 0) :
    digits b n = (n % b) :: digits b (n / b)

Proof state:
b n : ℕ
h : 1 < b
w : n ≠ 0
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
rcases b with (_ | _ | b)

Result:
case zero
n : ℕ
w : n ≠ 0
h : 1 < 0
⊢ digits 0 n = n % 0 :: digits 0 (n / 0)

case succ.zero
n : ℕ
w : n ≠ 0
h : 1 < 0 + 1
⊢ (0 + 1).digits n = n % (0 + 1) :: (0 + 1).digits (n / (0 + 1))

case succ.succ
n : ℕ
w : n ≠ 0
b : ℕ
h : 1 < b + 1 + 1
⊢ (b + 1 + 1).digits n = n % (b + 1 + 1) :: (b + 1 + 1).digits (n / (b + 1 + 1))

Proof state:
case succ.succ.zero
b : ℕ
h : 1 < b + 1 + 1
w : 0 ≠ 0
⊢ (b + 1 + 1).digits 0 = 0 % (b + 1 + 1) :: (b + 1 + 1).digits (0 / (b + 1 + 1))

Tactic:
norm_num at w

Result:
no goals

Proof state:
case succ.succ
n : ℕ
w : n ≠ 0
b : ℕ
h : 1 < b + 1 + 1
⊢ (b + 1 + 1).digits n = n % (b + 1 + 1) :: (b + 1 + 1).digits (n / (b + 1 + 1))

Tactic:
rcases n with (_ | n)

Result:
case succ.succ.zero
b : ℕ
h : 1 < b + 1 + 1
w : 0 ≠ 0
⊢ (b + 1 + 1).digits 0 = 0 % (b + 1 + 1) :: (b + 1 + 1).digits (0 / (b + 1 + 1))

case succ.succ.succ
b : ℕ
h : 1 < b + 1 + 1
n : ℕ
w : n + 1 ≠ 0
⊢ (b + 1 + 1).digits (n + 1) = (n + 1) % (b + 1 + 1) :: (b + 1 + 1).digits ((n + 1) / (b + 1 + 1))

Proof state:
case zero
n : ℕ
w : n ≠ 0
h : 1 < 0
⊢ digits 0 n = n % 0 :: digits 0 (n / 0)

Tactic:
rw [digits_zero_succ' w, Nat.mod_zero, Nat.div_zero, Nat.digits_zero_zero]

Result:
no goals

Proof state:
case succ.succ.succ
b : ℕ
h : 1 < b + 1 + 1
n : ℕ
w : n + 1 ≠ 0
⊢ (b + 1 + 1).digits (n + 1) = (n + 1) % (b + 1 + 1) :: (b + 1 + 1).digits ((n + 1) / (b + 1 + 1))

Tactic:
simp only [digits_add_two_add_one, ne_eq]

Result:
no goals

Proof state:
case succ.zero
n : ℕ
w : n ≠ 0
h : 1 < 0 + 1
⊢ (0 + 1).digits n = n % (0 + 1) :: (0 + 1).digits (n / (0 + 1))

Tactic:
norm_num at h

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem kunion_kerase {a} :
    ∀ {l₁ l₂ : List (Sigma β)}, kunion (kerase a l₁) (kerase a l₂) = kerase a (kunion l₁ l₂)
  | [], _ => rfl
  | s :: _, l => by by_cases h : a = s.1 <;> simp [h, kerase_comm a s.1 l, kunion_kerase]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

Tactic:
by_cases h : a = s.1 <;> simp [h, kerase_comm a s.1 l, kunion_kerase]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
    xs.findIdx? p = (xs.findFinIdx? p).map (·.val)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ findIdx? p xs = Option.map (fun x => ↑x) (findFinIdx? p xs)

Tactic:
simp [findIdx?, findFinIdx?]

Result:
α : Type u_1
xs : List α
p : α → Bool
⊢ findIdx?.go p xs 0 = Option.map (fun x => ↑x) (findFinIdx?.go p xs xs 0 ⋯)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ findIdx?.go p xs 0 = Option.map (fun x => ↑x) (findFinIdx?.go p xs xs 0 ⋯)

Tactic:
rw [findIdx?_go_eq_map_findFinIdx?_go_val]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_lt_rpow_of_neg (hx : 0 < x) (hxy : x < y) (hz : z < 0) : y ^ z < x ^ z

Proof state:
case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
positivity

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ y ^ z < x ^ z

Tactic:
rw [← inv_lt_inv₀, ← rpow_neg, ← rpow_neg]

Result:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ x ^ (-z) < y ^ (-z)

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
all_goals positivity

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
⊢ y ^ z < x ^ z

Tactic:
have := hx.trans hxy

Result:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ y ^ z < x ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ x ^ (-z) < y ^ (-z)

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
on_goal 1 => refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)

Result:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Proof state:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ x ^ (-z) < y ^ (-z)

Tactic:
refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)

Result:
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem natDegree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).natDegree = (q * p).natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.leadingCoeff * p.leadingCoeff ≠ 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
by_cases h : q = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).natDegree = (q * p).natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_add (a : α) (f f' : α →₀ M) : erase a (f + f') = erase a f + erase a f'

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : ¬s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

Tactic:
rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]

Result:
no goals

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

Tactic:
rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

Tactic:
by_cases hs : s = a

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

case neg
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : ¬s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
⊢ erase a (f + f') = erase a f + erase a f'

Tactic:
ext s

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
⊢ (erase a (f + f')) s = (erase a f + erase a f') s
-- Mathlib/Data/Multiset/DershowitzManna.lean
private lemma acc_oneStep_cons_of_acc_lt (ha : Acc LT.lt a) :
    ∀ {M}, Acc OneStep M → Acc OneStep (a ::ₘ M)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
ha : Acc LT.lt a
⊢ ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (a ::ₘ M)

Tactic:
induction' ha with a _ ha

Result:
case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
⊢ ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (a ::ₘ M)

Proof state:
case intro.intro.intro.inr.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ x ∈ N, x < a
⊢ Acc Multiset.OneStep (M + N)

Tactic:
induction N using Multiset.induction with
| empty =>
  simpa using .intro _ hM
| @cons b N ihN =>
  simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢
  obtain ⟨hba, hN⟩ := hN
  exact ha _ hba <| ihN hN

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M : Multiset α
hM : Acc Multiset.OneStep M
⊢ Acc Multiset.OneStep (a ::ₘ M)

Tactic:
induction' hM with M hM ihM

Result:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
⊢ Acc Multiset.OneStep (a ::ₘ M)
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem coeff_pow_eq_ite_of_natDegree_le_of_le {o : ℕ}
    (pn : natDegree p ≤ n) (mno : m * n ≤ o) :
    coeff (p ^ m) o = if o = m * n then (coeff p n) ^ m else 0

Proof state:
case inl
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0

Tactic:
simpa only [ite_true] using coeff_pow_of_natDegree_le pn

Result:
no goals

Proof state:
case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt <|
  lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)

Result:
no goals

Proof state:
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
rcases eq_or_ne o (m * n) with rfl | h

Result:
case inl
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0

case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
-- Mathlib/Probability/Process/Filtration.lean
theorem ext {f g : Filtration ι m} (h : (f : ι → MeasurableSpace Ω) = g) : f = g

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f g : Filtration ι m
h : ↑f = ↑g
⊢ f = g

Tactic:
cases f

Result:
case mk
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
g : Filtration ι m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ } = ↑g
⊢ { seq := seq✝, mono' := mono'✝, le' := le'✝ } = g

Proof state:
case mk
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
g : Filtration ι m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ } = ↑g
⊢ { seq := seq✝, mono' := mono'✝, le' := le'✝ } = g

Tactic:
cases g

Result:
case mk.mk
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
seq✝¹ : ι → MeasurableSpace Ω
mono'✝¹ : Monotone seq✝¹
le'✝¹ : ∀ (i : ι), seq✝¹ i ≤ m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ }
⊢ { seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = { seq := seq✝, mono' := mono'✝, le' := le'✝ }

Proof state:
case mk.mk
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
seq✝¹ : ι → MeasurableSpace Ω
mono'✝¹ : Monotone seq✝¹
le'✝¹ : ∀ (i : ι), seq✝¹ i ≤ m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ }
⊢ { seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = { seq := seq✝, mono' := mono'✝, le' := le'✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem sum_card_orderOf_eq_card_pow_eq_one [Fintype G] [DecidableEq G] (hn : n ≠ 0) :
    (∑ m ∈ divisors n,
        (Finset.univ.filter fun x : G => orderOf x = m).card) =
      (Finset.univ.filter fun x : G => x ^ n = 1).card

Proof state:
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∑ m ∈ n.divisors, (Finset.filter (fun x => orderOf x = m) Finset.univ).card =
    (Finset.filter (fun x => x ^ n = 1) Finset.univ).card

Tactic:
refine (Finset.card_biUnion ?_).symm.trans ?_

Result:
case refine_1
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∀ x ∈ n.divisors,
    ∀ y ∈ n.divisors,
      x ≠ y →
        Disjoint (Finset.filter (fun x_1 => orderOf x_1 = x) Finset.univ)
          (Finset.filter (fun x => orderOf x = y) Finset.univ)

case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (n.divisors.biUnion fun m => Finset.filter (fun x => orderOf x = m) Finset.univ).card =
    (Finset.filter (fun x => x ^ n = 1) Finset.univ).card

Proof state:
case refine_1
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∀ x ∈ n.divisors,
    ∀ y ∈ n.divisors,
      x ≠ y →
        Disjoint (Finset.filter (fun x_1 => orderOf x_1 = x) Finset.univ)
          (Finset.filter (fun x => orderOf x = y) Finset.univ)

Tactic:
simp +contextual [disjoint_iff, Finset.ext_iff]

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (n.divisors.biUnion fun m => Finset.filter (fun x => orderOf x = m) Finset.univ).card =
    (Finset.filter (fun x => x ^ n = 1) Finset.univ).card

Tactic:
congr

Result:
case refine_2.e_s
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (n.divisors.biUnion fun m => Finset.filter (fun x => orderOf x = m) Finset.univ) =
    Finset.filter (fun x => x ^ n = 1) Finset.univ

Proof state:
case refine_2.e_s.h
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
a✝ : G
⊢ (a✝ ∈ n.divisors.biUnion fun m => Finset.filter (fun x => orderOf x = m) Finset.univ) ↔
    a✝ ∈ Finset.filter (fun x => x ^ n = 1) Finset.univ

Tactic:
simp [hn, orderOf_dvd_iff_pow_eq_one]

Result:
no goals

Proof state:
case refine_2.e_s
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (n.divisors.biUnion fun m => Finset.filter (fun x => orderOf x = m) Finset.univ) =
    Finset.filter (fun x => x ^ n = 1) Finset.univ

Tactic:
ext

Result:
case refine_2.e_s.h
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
a✝ : G
⊢ (a✝ ∈ n.divisors.biUnion fun m => Finset.filter (fun x => orderOf x = m) Finset.univ) ↔
    a✝ ∈ Finset.filter (fun x => x ^ n = 1) Finset.univ
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative
of the Riemann zeta function on its domain of convergence `re s > 1`. -/
lemma LSeries_vonMangoldt_eq_deriv_riemannZeta_div {s : ℂ} (hs : 1 < s.re) :
    L ↗Λ s = - deriv riemannZeta s / riemannZeta s

Proof state:
s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
⊢ L (fun n => ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ deriv (L 1) s = deriv riemannZeta s

Tactic:
refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_

Result:
s : ℂ
hs : 1 < s.re
⊢ ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1

Proof state:
s : ℂ
hs : 1 < s.re
⊢ ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1

Tactic:
exact ⟨{z | 1 < z.re}, (isOpen_lt continuous_const continuous_re).mem_nhds hs,
  fun _ ↦ LSeries_one_eq_riemannZeta⟩

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
suffices deriv (L 1) s = deriv riemannZeta s by
  rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]

Result:
s : ℂ
hs : 1 < s.re
⊢ deriv (L 1) s = deriv riemannZeta s
-- Mathlib/Analysis/Seminorm.lean
theorem smul_closedBall_subset {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} :
    k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r)

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x => k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r

Tactic:
rw [Seminorm.mem_closedBall_zero] at hy

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : p y ≤ r
h : (fun x => k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : p y ≤ r
h : (fun x => k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r

Tactic:
gcongr

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
⊢ k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r)

Tactic:
rintro x ⟨y, hy, h⟩

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x => k • x) y = x
⊢ x ∈ p.closedBall 0 (‖k‖ * r)

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x => k • x) y = x
⊢ x ∈ p.closedBall 0 (‖k‖ * r)

Tactic:
rw [Seminorm.mem_closedBall_zero, ← h, map_smul_eq_mul]

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x => k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodyLT'_volume :
    volume (convexBodyLT' K f w₀) = convexBodyLT'Factor K * ∏ w, (f w) ^ (mult w)

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume (Set.Ioo (-1) 1 ×ˢ Set.Ioo (-↑B ^ 2) (↑B ^ 2)) = 4 * ↑B ^ 2

Tactic:
simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
  ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
  ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]

Result:
no goals

Proof state:
case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀)) = 4 * ↑(f ↑w₀) ^ 2

Tactic:
simpa only [ite_true] using vol_box (f w₀)

Result:
no goals