harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.List.stronglyMeasurable_prod' (l : List (α → M))
    (hl : ∀ f ∈ l, StronglyMeasurable f) : StronglyMeasurable l.prod

Proof state:
case cons
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod
hl : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x
⊢ StronglyMeasurable (f * l.prod)

Tactic:
exact hl.1.mul (ihl hl.2)

Result:
no goals

Proof state:
case nil
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
hl : ∀ f ∈ [], StronglyMeasurable f
⊢ StronglyMeasurable [].prod

Tactic:
exact stronglyMeasurable_one

Result:
no goals

Proof state:
case cons
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod
hl : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x
⊢ StronglyMeasurable (f :: l).prod

Tactic:
rw [List.prod_cons]

Result:
case cons
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod
hl : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x
⊢ StronglyMeasurable (f * l.prod)

Proof state:
case cons
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod
hl : ∀ f_1 ∈ f :: l, StronglyMeasurable f_1
⊢ StronglyMeasurable (f :: l).prod

Tactic:
rw [List.forall_mem_cons] at hl

Result:
case cons
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod
hl : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x
⊢ StronglyMeasurable (f :: l).prod

Proof state:
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
⊢ StronglyMeasurable l.prod

Tactic:
induction' l with f l ihl

Result:
case nil
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
hl : ∀ f ∈ [], StronglyMeasurable f
⊢ StronglyMeasurable [].prod

case cons
α : Type u_1
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, StronglyMeasurable f) → StronglyMeasurable l.prod
hl : ∀ f_1 ∈ f :: l, StronglyMeasurable f_1
⊢ StronglyMeasurable (f :: l).prod
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.image {s : Set α} (f : α → β) (hs : s.Finite) : (f '' s).Finite

Proof state:
α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
this : Finite ↑s
⊢ (f '' s).Finite

Tactic:
apply toFinite

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).Finite

Tactic:
have := hs.to_subtype

Result:
α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
this : Finite ↑s
⊢ (f '' s).Finite
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
@[simp]
lemma inl_rel'_inl_iff (x₁ y₁ : X₁) :
    Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔ x₁ = y₁ ∨
      ∃ (x₀ y₀ : S) (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀

Proof state:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) → x₁ = y₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀

Tactic:
rintro (_|⟨_, _, h⟩)

Result:
case mp.refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ x₁ = x₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ x₁ = f y₀

case mp.inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
⊢ f x₀✝ = f y₀✝ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), f x₀✝ = f x₀ ∧ f y₀✝ = f y₀

Proof state:
case mp.refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ x₁ = x₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ x₁ = f y₀

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
case mpr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl x₁)

Tactic:
apply Rel'.refl

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔ x₁ = y₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀

Tactic:
constructor

Result:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) → x₁ = y₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ (x₁ = y₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀) → Rel' f g (Sum.inl x₁) (Sum.inl y₁)

Proof state:
case mpr.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
w✝¹ w✝ : S
h : g w✝¹ = g w✝
⊢ Rel' f g (Sum.inl (f w✝¹)) (Sum.inl (f w✝))

Tactic:
exact Rel'.inl_inl _ _ h

Result:
no goals

Proof state:
case mp.inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : g x₀✝ = g y₀✝
⊢ f x₀✝ = f y₀✝ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), f x₀✝ = f x₀ ∧ f y₀✝ = f y₀

Tactic:
exact Or.inr ⟨_, _, h, rfl, rfl⟩

Result:
no goals

Proof state:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ (x₁ = y₁ ∨ ∃ x₀ y₀, ∃ (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀) → Rel' f g (Sum.inl x₁) (Sum.inl y₁)

Tactic:
rintro (rfl | ⟨_,_ , h, rfl, rfl⟩)

Result:
case mpr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl x₁)

case mpr.inr.intro.intro.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
w✝¹ w✝ : S
h : g w✝¹ = g w✝
⊢ Rel' f g (Sum.inl (f w✝¹)) (Sum.inl (f w✝))
-- Mathlib/Order/Category/BddOrd.lean
lemma id_apply (X : BddOrd) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : BddOrd
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma edist_bot [DecidableEq V] : (⊥ : SimpleGraph V).edist u v = (if u = v then 0 else ⊤)

Proof state:
V : Type u_1
u v : V
inst✝ : DecidableEq V
⊢ ⊥.edist u v = if u = v then 0 else ⊤

Tactic:
by_cases h : u = v <;> simp [h, edist_bot_of_ne]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.toList_nonEmpty (e : Expr) : e.toList ≠ []

Proof state:
case op
l r : Expr
ih₁ : l.toList ≠ []
rhs_ih✝ : r.toList ≠ []
⊢ ¬l.toList ++ r.toList = []

Tactic:
cases h : l.toList with
| nil => contradiction
| cons => simp [List.append]

Result:
no goals

Proof state:
case var
x✝ : Nat
⊢ (Expr.var x✝).toList ≠ []

Tactic:
simp [Expr.toList]

Result:
no goals

Proof state:
e : Expr
⊢ e.toList ≠ []

Tactic:
induction e with
| var => simp [Expr.toList]
| op l r ih₁ _   =>
  simp [Expr.toList]
  cases h : l.toList with
  | nil => contradiction
  | cons => simp [List.append]

Result:
no goals

Proof state:
case op.nil
l r : Expr
ih₁ : l.toList ≠ []
rhs_ih✝ : r.toList ≠ []
h : l.toList = []
⊢ ¬[] ++ r.toList = []

Tactic:
contradiction

Result:
no goals

Proof state:
case op
l r : Expr
ih₁ : l.toList ≠ []
rhs_ih✝ : r.toList ≠ []
⊢ (l.op r).toList ≠ []

Tactic:
simp [Expr.toList]

Result:
case op
l r : Expr
ih₁ : l.toList ≠ []
rhs_ih✝ : r.toList ≠ []
⊢ ¬l.toList ++ r.toList = []

Proof state:
case op.cons
l r : Expr
ih₁ : l.toList ≠ []
rhs_ih✝ : r.toList ≠ []
head✝ : Nat
tail✝ : List Nat
h : l.toList = head✝ :: tail✝
⊢ ¬head✝ :: tail✝ ++ r.toList = []

Tactic:
simp [List.append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_abs_eq_ite {x : BitVec w} :
  x.abs.toInt =
    if x = intMin w then (intMin w).toInt
    else if x.msb then -x.toInt
    else x.toInt

Proof state:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
hx₂ : x.msb = true
⊢ x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

Tactic:
simp [hx₂, abs_eq, toInt_neg_of_ne_intMin hx]

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
hx : x = intMin w
⊢ x.abs.toInt = if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

Tactic:
by_cases hx₂ : x.msb

Result:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
hx₂ : x.msb = true
⊢ x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
hx₂ : ¬x.msb = true
⊢ x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ x.abs.toInt = if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt

Tactic:
simp [hx]

Result:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
hx₂ : ¬x.msb = true
⊢ x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

Tactic:
simp [hx₂, abs_eq]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.abs.toInt = if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt

Tactic:
by_cases hx : x = intMin w

Result:
case pos
w : Nat
x : BitVec w
hx : x = intMin w
⊢ x.abs.toInt = if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt

case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ x.abs.toInt = if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma d_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₂ = p₃) (p₁ : ι) :
    K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq ⋯).hom = K.d p₁ p₂

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₂ = p₃
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃

Tactic:
subst h

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq ⋯).hom = K.d p₁ p₂
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem add_eq_max_of_ne {f g : PadicSeq p} (hfgne : f.norm ≠ g.norm) :
    (f + g).norm = max f.norm g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    padicNorm p (↑f (stationaryPoint hf)) ⊔ padicNorm p (↑g (stationaryPoint hg))

Tactic:
rw [lift_index_left hf, lift_index_right hg] at hfgne

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (?v1 ⊔ (?v2 ⊔ stationaryPoint hg)))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    padicNorm p (↑f (stationaryPoint hf)) ⊔ padicNorm p (↑g (stationaryPoint hg))

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (?v1 ⊔ (stationaryPoint hf ⊔ ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
⊢ (f + g).norm = f.norm ⊔ g.norm

Tactic:
have h2 : g.norm = 0 := (norm_zero_iff _).2 hg

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
⊢ (f + g).norm = f.norm ⊔ g.norm
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@[to_additive]
lemma IsCyclic.exists_ofOrder_eq_natCard [h : IsCyclic α] : ∃ g : α, orderOf g = Nat.card α

Proof state:
case intro
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ ∃ g, orderOf g = Nat.card α

Tactic:
use g

Result:
case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α

Proof state:
α : Type u_1
inst✝ : Group α
h : IsCyclic α
⊢ ∃ g, orderOf g = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := h.exists_generator

Result:
case intro
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ ∃ g, orderOf g = Nat.card α

Proof state:
case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card ↥⊤ = Nat.card α

Tactic:
exact Nat.card_congr (Equiv.Set.univ α)

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α

Tactic:
rw [← card_zpowers g, (eq_top_iff' (zpowers g)).mpr hg]

Result:
case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card ↥⊤ = Nat.card α
-- Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
lemma Real.summable_log_one_add_of_summable {f : ι → ℝ} (hf : Summable f) :
     Summable (fun i : ι => log (1 + |f i|))

Proof state:
ι : Type u_1
f : ι → ℝ
hf : Summable f
this : Summable fun n => ofRealCLM (log (1 + |f n|))
⊢ Summable fun i => log (1 + |f i|)

Tactic:
convert Complex.reCLM.summable this

Result:
no goals

Proof state:
case h.e'_5.h
ι : Type u_1
f : ι → ℝ
hf : Summable f
x : ι
⊢ ofRealCLM (log (1 + |f x|)) = Complex.log (1 + ofRealCLM ‖f x‖)

Tactic:
rw [ofRealCLM_apply, ofReal_log (by positivity)]

Result:
case h.e'_5.h
ι : Type u_1
f : ι → ℝ
hf : Summable f
x : ι
⊢ Complex.log ↑(1 + |f x|) = Complex.log (1 + ofRealCLM ‖f x‖)

Proof state:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Summable fun n => ofRealCLM (log (1 + |f n|))

Tactic:
convert Complex.summable_log_one_add_of_summable (Complex.ofRealCLM.summable hf.norm) with x

Result:
case h.e'_5.h
ι : Type u_1
f : ι → ℝ
hf : Summable f
x : ι
⊢ ofRealCLM (log (1 + |f x|)) = Complex.log (1 + ofRealCLM ‖f x‖)

Proof state:
case h.e'_5.h
ι : Type u_1
f : ι → ℝ
hf : Summable f
x : ι
⊢ Complex.log ↑(1 + |f x|) = Complex.log (1 + ofRealCLM ‖f x‖)

Tactic:
simp only [ofReal_add, ofReal_one, norm_eq_abs, ofRealCLM_apply]

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℝ
hf : Summable f
x : ι
⊢ 0 ≤ 1 + |f x|

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℝ
hf : Summable f
⊢ Summable fun i => log (1 + |f i|)

Tactic:
have : Summable (fun n ↦ Complex.ofRealCLM (log (1 + |f n|))) := by
  convert Complex.summable_log_one_add_of_summable (Complex.ofRealCLM.summable hf.norm) with x
  rw [ofRealCLM_apply, ofReal_log (by positivity)]
  simp only [ofReal_add, ofReal_one, norm_eq_abs, ofRealCLM_apply]

Result:
ι : Type u_1
f : ι → ℝ
hf : Summable f
this : Summable fun n => ofRealCLM (log (1 + |f n|))
⊢ Summable fun i => log (1 + |f i|)
-- Mathlib/Algebra/Order/Floor.lean
theorem abs_sub_lt_one_of_floor_eq_floor {α : Type*} [LinearOrderedCommRing α] [FloorRing α]
    {a b : α} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
⊢ |a - b| < 1

Tactic:
have : a < ⌊a⌋ + 1 := lt_floor_add_one a

Result:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this : a < ↑⌊a⌋ + 1
⊢ |a - b| < 1

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝ : a < ↑⌊a⌋ + 1
this : b < ↑⌊b⌋ + 1
⊢ |a - b| < 1

Tactic:
have : (⌊a⌋ : α) = ⌊b⌋ := Int.cast_inj.2 h

Result:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝¹ : a < ↑⌊a⌋ + 1
this✝ : b < ↑⌊b⌋ + 1
this : ↑⌊a⌋ = ↑⌊b⌋
⊢ |a - b| < 1

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this : a < ↑⌊a⌋ + 1
⊢ |a - b| < 1

Tactic:
have : b < ⌊b⌋ + 1 := lt_floor_add_one b

Result:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝ : a < ↑⌊a⌋ + 1
this : b < ↑⌊b⌋ + 1
⊢ |a - b| < 1

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝³ : a < ↑⌊a⌋ + 1
this✝² : b < ↑⌊b⌋ + 1
this✝¹ : ↑⌊a⌋ = ↑⌊b⌋
this✝ : ↑⌊a⌋ ≤ a
this : ↑⌊b⌋ ≤ b
⊢ a - b < 1

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝³ : a < ↑⌊a⌋ + 1
this✝² : b < ↑⌊b⌋ + 1
this✝¹ : ↑⌊a⌋ = ↑⌊b⌋
this✝ : ↑⌊a⌋ ≤ a
this : ↑⌊b⌋ ≤ b
⊢ |a - b| < 1

Tactic:
exact abs_sub_lt_iff.2 ⟨by linarith, by linarith⟩

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝³ : a < ↑⌊a⌋ + 1
this✝² : b < ↑⌊b⌋ + 1
this✝¹ : ↑⌊a⌋ = ↑⌊b⌋
this✝ : ↑⌊a⌋ ≤ a
this : ↑⌊b⌋ ≤ b
⊢ b - a < 1

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝¹ : a < ↑⌊a⌋ + 1
this✝ : b < ↑⌊b⌋ + 1
this : ↑⌊a⌋ = ↑⌊b⌋
⊢ |a - b| < 1

Tactic:
have : (⌊a⌋ : α) ≤ a := floor_le a

Result:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝² : a < ↑⌊a⌋ + 1
this✝¹ : b < ↑⌊b⌋ + 1
this✝ : ↑⌊a⌋ = ↑⌊b⌋
this : ↑⌊a⌋ ≤ a
⊢ |a - b| < 1

Proof state:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝² : a < ↑⌊a⌋ + 1
this✝¹ : b < ↑⌊b⌋ + 1
this✝ : ↑⌊a⌋ = ↑⌊b⌋
this : ↑⌊a⌋ ≤ a
⊢ |a - b| < 1

Tactic:
have : (⌊b⌋ : α) ≤ b := floor_le b

Result:
α : Type u_4
inst✝¹ : LinearOrderedCommRing α
inst✝ : FloorRing α
a b : α
h : ⌊a⌋ = ⌊b⌋
this✝³ : a < ↑⌊a⌋ + 1
this✝² : b < ↑⌊b⌋ + 1
this✝¹ : ↑⌊a⌋ = ↑⌊b⌋
this✝ : ↑⌊a⌋ ≤ a
this : ↑⌊b⌋ ≤ b
⊢ |a - b| < 1
-- Mathlib/Algebra/Ring/Idempotent.lean
@[simp]
lemma mul_one_sub_self (h : IsIdempotentElem a) : a * (1 - a) = 0

Proof state:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a * (1 - a) = 0

Tactic:
rw [mul_sub, mul_one, h.eq, sub_self]

Result:
no goals
-- Mathlib/Algebra/Module/PID.lean
theorem exists_smul_eq_zero_and_mk_eq {z : M} (hz : Module.IsTorsionBy R M (p ^ pOrder hM z))
    {k : ℕ} (f : (R ⧸ R ∙ p ^ k) →ₗ[R] M ⧸ R ∙ z) :
    ∃ x : M, p ^ k • x = 0 ∧ Submodule.Quotient.mk (p := span R {z}) x = f 1

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ Submodule.span R {z}
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Tactic:
obtain ⟨a, ha⟩ := p_pow_smul_lift hp hM hz this

Result:
case intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
this : p ^ k • f1.choose ∈ Submodule.span R {z}
a : R
ha : p ^ k • f1.choose = p ^ k • a • z
⊢ ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ f (p ^ k • 1) = 0

Tactic:
convert f.map_zero

Result:
case h.e'_2.h.e'_6
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k • 1 = 0

Proof state:
case h.e'_2.h.e'_6
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}
f1 : ∃ a, Submodule.Quotient.mk a = f 1
⊢ p ^ k ∈ Submodule.span R {p ^ k}

Tactic:
exact Submodule.mem_span_singleton_self _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h))

Proof state:
α : Type ?u.57866
β : Type ?u.57903
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
a : α
h : a ∈ xs.reverse
⊢ a ∈ xs

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).reverse = pmap f xs.reverse ⋯

Tactic:
rw [pmap_reverse]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_neg_one {R : Type*} [Ring R] (n : ℕ) : cast (-1 : ZMod n) = (n - 1 : R)

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑n - 1

Tactic:
rcases n with - | n

Result:
case zero
R : Type u_1
inst✝ : Ring R
⊢ (-1).cast = ↑0 - 1

case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1

Proof state:
case zero
R : Type u_1
inst✝ : Ring R
⊢ (-1).cast = ↑0 - 1

Tactic:
dsimp [ZMod, ZMod.cast]

Result:
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1

Proof state:
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1

Tactic:
rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivativeFinsupp_one : derivativeFinsupp (1 : R[X]) = .single 0 1

Proof state:
R : Type u
inst✝ : Semiring R
⊢ derivativeFinsupp 1 = Finsupp.single 0 1

Tactic:
simpa using derivativeFinsupp_C (1 : R)

Result:
no goals