harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma exp_llr (μ ν : Measure α) [SigmaFinite μ] :
    (fun x ↦ exp (llr μ ν x))
      =ᵐ[ν] fun x ↦ if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
by_cases h_zero : μ.rnDeriv ν x = 0

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
h_zero : μ.rnDeriv ν x = 0
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
h_zero : ¬μ.rnDeriv ν x = 0
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ (fun x => rexp (llr μ ν x)) =ᶠ[ae ν] fun x => if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
h_zero : ¬μ.rnDeriv ν x = 0
⊢ 0 < (μ.rnDeriv ν x).toReal

Tactic:
exact ENNReal.toReal_pos h_zero hx.ne

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
h_zero : ¬μ.rnDeriv ν x = 0
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
rw [llr, exp_log, if_neg h_zero]

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
h_zero : ¬μ.rnDeriv ν x = 0
⊢ 0 < (μ.rnDeriv ν x).toReal

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ⊤
h_zero : μ.rnDeriv ν x = 0
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Tactic:
simp only [llr, h_zero, ENNReal.zero_toReal, log_zero, exp_zero, ite_true]

Result:
no goals
-- Mathlib/Logic/Embedding/Set.lean
theorem Equiv.asEmbedding_range {α β : Sort _} {p : β → Prop} (e : α ≃ Subtype p) :
    Set.range e.asEmbedding = setOf p :=
  Set.ext fun x ↦ ⟨fun ⟨y, h⟩ ↦ h ▸ Subtype.coe_prop (e y), fun hs ↦ ⟨e.symm ⟨x, hs⟩, by simp⟩⟩

Proof state:
α : Sort u_1
β : Type u_2
p : β → Prop
e : α ≃ Subtype p
x : β
hs : x ∈ setOf p
⊢ e.asEmbedding (e.symm ⟨x, hs⟩) = x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
theorem hasFiniteLimits_of_hasFiniteLimits_of_size
    (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasLimitsOfShape J C) :
    HasFiniteLimits C where
  out := fun J hJ hhJ => by
    haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
    have l : @Equivalence J (ULiftHom (ULift J)) hJ
                          (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
      @ULiftHomULiftCategory.equiv J hJ
    apply @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
      (@Equivalence.symm J hJ (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasLimitsOfShape J C

Tactic:
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ

Result:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
⊢ HasLimitsOfShape J C

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
⊢ HasLimitsOfShape J C

Tactic:
have l : @Equivalence J (ULiftHom (ULift J)) hJ
                      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
  @ULiftHomULiftCategory.equiv J hJ

Result:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
l : J ≌ ULiftHom (ULift.{?u.1084, 0} J)
⊢ HasLimitsOfShape J C

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
l : J ≌ ULiftHom (ULift.{?u.1084, 0} J)
⊢ HasLimitsOfShape J C

Tactic:
apply @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J))
  (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
  (@Equivalence.symm J hJ (ULiftHom (ULift J))
  (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Completeness.lean
/-- In a complete normed additive group, every absolutely convergent series converges in the
space. -/
lemma NormedAddCommGroup.summable_imp_tendsto_of_complete [CompleteSpace E] (u : ℕ → E)
    (hu : Summable (‖u ·‖)) : ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
u : ℕ → E
hu : Summable fun x => ‖u x‖
⊢ ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)

Tactic:
refine cauchySeq_tendsto_of_complete <| cauchySeq_of_summable_dist ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
u : ℕ → E
hu : Summable fun x => ‖u x‖
⊢ Summable fun n => dist (∑ i ∈ range n, u i) (∑ i ∈ range n.succ, u i)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
u : ℕ → E
hu : Summable fun x => ‖u x‖
⊢ Summable fun n => dist (∑ i ∈ range n, u i) (∑ i ∈ range n.succ, u i)

Tactic:
simp [dist_eq_norm, sum_range_succ, hu]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_addCases_left {n' : ℕ} {motive : Fin (n + n') → Sort*} (m : ℕ) (h : m ≤ n)
    (u : (i : Fin n) → motive (castAdd n' i)) (v : (i : Fin n') → motive (natAdd n i)) :
      take m (Nat.le_add_right_of_le h) (addCases u v) = take m h u

Proof state:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
this : ↑i < n
⊢ u ((castLE ⋯ i).castLT ⋯) = u (castLE h i)

Tactic:
congr

Result:
no goals

Proof state:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
⊢ take m ⋯ (fun i => addCases u v i) i = take m h u i

Tactic:
have : i < n := Nat.lt_of_lt_of_le i.isLt h

Result:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
this : ↑i < n
⊢ take m ⋯ (fun i => addCases u v i) i = take m h u i

Proof state:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
this : ↑i < n
⊢ take m ⋯ (fun i => addCases u v i) i = take m h u i

Tactic:
simp only [take, addCases, this, coe_castLE, ↓reduceDIte]

Result:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
this : ↑i < n
⊢ u ((castLE ⋯ i).castLT ⋯) = u (castLE h i)

Proof state:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take m ⋯ fun i => addCases u v i) = take m h u

Tactic:
ext i

Result:
case h
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
⊢ take m ⋯ (fun i => addCases u v i) i = take m h u i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (insertEntryIfNew k v l).length = if containsKey k l then l.length else l.length + 1

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (insertEntryIfNew k v l).length = if containsKey k l = true then l.length else l.length + 1

Tactic:
simp [insertEntryIfNew, Bool.apply_cond List.length]

Result:
no goals
-- Mathlib/Data/Erased.lean
theorem out_mk {α} (a : α) : (mk a).out = a

Proof state:
α : Sort u_1
a : α
h : ∃ a_1, (fun x => a_1 = x) = (mk a).val := (mk a).property
this : (fun x => Classical.choose h = x) = (mk a).val
⊢ Classical.choose h = a

Tactic:
exact cast (congr_fun this a).symm rfl

Result:
no goals

Proof state:
α : Sort u_1
a : α
h : ∃ a_1, (fun x => a_1 = x) = (mk a).val := (mk a).property
⊢ (mk a).out = a

Tactic:
show Classical.choose h = a

Result:
α : Sort u_1
a : α
h : ∃ a_1, (fun x => a_1 = x) = (mk a).val := (mk a).property
⊢ Classical.choose h = a

Proof state:
α : Sort u_1
a : α
h : ∃ a_1, (fun x => a_1 = x) = (mk a).val := (mk a).property
⊢ Classical.choose h = a

Tactic:
have := Classical.choose_spec h

Result:
α : Sort u_1
a : α
h : ∃ a_1, (fun x => a_1 = x) = (mk a).val := (mk a).property
this : (fun x => Classical.choose h = x) = (mk a).val
⊢ Classical.choose h = a

Proof state:
α : Sort u_1
a : α
⊢ (mk a).out = a

Tactic:
let h := (mk a).2

Result:
α : Sort u_1
a : α
h : ∃ a_1, (fun x => a_1 = x) = (mk a).val := (mk a).property
⊢ (mk a).out = a
-- Mathlib/Data/Ordmap/Ordset.lean
theorem pos_size_of_mem [LE α] [DecidableRel (α := α) (· ≤ ·)] {x : α} {t : Ordnode α} (h : Sized t)
    (h_mem : x ∈ t) : 0 < size t

Proof state:
case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
h : nil.Sized
h_mem : x ∈ nil
⊢ 0 < nil.size

Tactic:
contradiction

Result:
no goals

Proof state:
case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size

Tactic:
simp [h.1]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordnode α
h : t.Sized
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
cases t

Result:
case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
h : nil.Sized
h_mem : x ∈ nil
⊢ 0 < nil.size

case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_filterₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → Bool} (h : Raw.WFImp m.1) : IsHashSelf (m.filterₘ f).1.buckets

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp✝ : p ∈ (AssocList.filter f l).toList
hp : p ∈ List.filter (fun p => f p.fst p.snd) l.toList
⊢ containsKey p.fst l.toList = true

Tactic:
obtain ⟨hp, -⟩ := mem_filter.1 hp

Result:
case intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp✝¹ : p ∈ (AssocList.filter f l).toList
hp✝ : p ∈ List.filter (fun p => f p.fst p.snd) l.toList
hp : p ∈ l.toList
⊢ containsKey p.fst l.toList = true

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
⊢ IsHashSelf (m.filterₘ f).val.buckets

Tactic:
refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_)

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.filter f l).toList
⊢ containsKey p.fst l.toList = true

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.filter f l).toList
⊢ containsKey p.fst l.toList = true

Tactic:
have hp := AssocList.toList_filter.mem_iff.1 hp

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp✝ : p ∈ (AssocList.filter f l).toList
hp : p ∈ List.filter (fun p => f p.fst p.snd) l.toList
⊢ containsKey p.fst l.toList = true

Proof state:
case intro
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : ReflBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp✝¹ : p ∈ (AssocList.filter f l).toList
hp✝ : p ∈ List.filter (fun p => f p.fst p.snd) l.toList
hp : p ∈ l.toList
⊢ containsKey p.fst l.toList = true

Tactic:
exact containsKey_of_mem hp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_neg_of_neg_of_pos {a b : Int} (ha : a < 0) (hb : 0 < b) : a * b < 0

Proof state:
a b : Int
ha : a < 0
hb : 0 < b
⊢ a * b < 0

Tactic:
have h : a * b < 0 * b := Int.mul_lt_mul_of_pos_right ha hb

Result:
a b : Int
ha : a < 0
hb : 0 < b
h : a * b < 0 * b
⊢ a * b < 0

Proof state:
a b : Int
ha : a < 0
hb : 0 < b
h : a * b < 0 * b
⊢ a * b < 0

Tactic:
rwa [Int.zero_mul] at h

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem ball {p : α → Prop} {a b : α} : (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b

Proof state:
case inl
α : Type u_1
p : α → Prop
b c : α
h : p c ∧ p b
hc : c ∈ s(c, b)
⊢ p c

Tactic:
exact h.1

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
a b : α
⊢ (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b

Tactic:
refine ⟨fun h => ⟨h _ <| mem_mk_left _ _, h _ <| mem_mk_right _ _⟩, fun h c hc => ?_⟩

Result:
α : Type u_1
p : α → Prop
a b : α
h : p a ∧ p b
c : α
hc : c ∈ s(a, b)
⊢ p c

Proof state:
α : Type u_1
p : α → Prop
a b : α
h : p a ∧ p b
c : α
hc : c ∈ s(a, b)
⊢ p c

Tactic:
obtain rfl | rfl := Sym2.mem_iff.1 hc

Result:
case inl
α : Type u_1
p : α → Prop
b c : α
h : p c ∧ p b
hc : c ∈ s(c, b)
⊢ p c

case inr
α : Type u_1
p : α → Prop
a c : α
h : p a ∧ p c
hc : c ∈ s(a, c)
⊢ p c

Proof state:
case inr
α : Type u_1
p : α → Prop
a c : α
h : p a ∧ p c
hc : c ∈ s(a, c)
⊢ p c

Tactic:
exact h.2

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
theorem normedMk_eq_zero_iff : normedMk (M := M) = 0 ↔ ∀ (x : M), ‖x‖ = 0

Proof state:
case mpr.H
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
x : M
⊢ normedMk x = 0 x

Tactic:
simpa [← norm_eq_zero] using h x

Result:
no goals

Proof state:
case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
⊢ normedMk = 0

Tactic:
ext x

Result:
case mpr.H
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
x : M
⊢ normedMk x = 0 x

Proof state:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = normedMk x

Tactic:
simp

Result:
no goals

Proof state:
case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ (∀ (x : M), ‖x‖ = 0) → normedMk = 0

Tactic:
intro h

Result:
case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
⊢ normedMk = 0

Proof state:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ normedMk = 0 → ∀ (x : M), ‖x‖ = 0

Tactic:
intro h x

Result:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ ‖x‖ = 0

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ 0 x = 0

Tactic:
simp only [zero_apply]

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ ‖x‖ = 0

Tactic:
rw [SeparationQuotient.mk_eq_zero_iff.mp]

Result:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ mk x = 0

Proof state:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = 0

Tactic:
rw [← this]

Result:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = normedMk x

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ normedMk x = 0

Tactic:
rw [h]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ 0 x = 0

Proof state:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ mk x = 0

Tactic:
have : normedMk x = 0 := by
  rw [h]
  simp only [zero_apply]

Result:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = 0

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ normedMk = 0 ↔ ∀ (x : M), ‖x‖ = 0

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ normedMk = 0 → ∀ (x : M), ‖x‖ = 0

case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ (∀ (x : M), ‖x‖ = 0) → normedMk = 0
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_sub {R : Type u} [Ring R] (a b : R[X]) :
    (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

Proof state:
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

Tactic:
rw [sub_eq_add_neg, ← toFinsupp_neg, ← toFinsupp_add]

Result:
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp

Proof state:
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem unit_smul_eq_zero (u : (𝓞 K)ˣ) (x : mixedSpace K) :
    u • x = 0 ↔ x = 0

Proof state:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
⊢ u • x = 0

Tactic:
rw [h, smul_zero]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x ≠ 0
⊢ u • x ≠ 0

Tactic:
obtain ⟨w, h⟩ := exists_normAtPlace_ne_zero_iff.mpr h

Result:
case intro
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ u • x ≠ 0

Proof state:
case intro
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ u • x ≠ 0

Tactic:
refine exists_normAtPlace_ne_zero_iff.mp ⟨w, ?_⟩

Result:
case intro
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) (u • x) ≠ 0

Proof state:
case intro
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) (u • x) ≠ 0

Tactic:
rw [unitSMul_smul, map_mul]

Result:
case intro
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) * (normAtPlace w) x ≠ 0

Proof state:
case intro
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) * (normAtPlace w) x ≠ 0

Tactic:
exact mul_ne_zero (by simp) h

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ u • x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, smul_zero]⟩

Result:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : u • x = 0
⊢ x = 0

Proof state:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : u • x = 0
⊢ x = 0

Tactic:
contrapose! h

Result:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x ≠ 0
⊢ u • x ≠ 0

Proof state:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_fiberwise (f : β → ℝ≥0∞) (g : β → γ) :
    ∑' x, ∑' b : g ⁻¹' {x}, f b = ∑' i, f i

Proof state:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
⊢ ∑' (x : γ) (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : β), f i

Tactic:
apply HasSum.tsum_eq

Result:
case ha
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
⊢ HasSum (fun b => ∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1) (∑' (i : β), f i)

Proof state:
case ha
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
⊢ HasSum (fun b => ∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1) (∑' (i : β), f i)

Tactic:
apply (equiv.hasSum_iff.mpr ENNReal.summable.hasSum).sigma

Result:
case ha
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
⊢ ∀ (b : γ), HasSum (fun c => (f ∘ ⇑equiv) ⟨b, c⟩) (∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1)

Proof state:
case ha
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
⊢ ∀ (b : γ), HasSum (fun c => (f ∘ ⇑equiv) ⟨b, c⟩) (∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1)

Tactic:
exact fun _ ↦ ENNReal.summable.hasSum_iff.mpr rfl

Result:
no goals

Proof state:
case ha
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
⊢ HasSum (fun b => ∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1) (∑' (i : β), f i)

Tactic:
let equiv := Equiv.sigmaFiberEquiv g

Result:
case ha
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
⊢ HasSum (fun b => ∑' (b_1 : ↑(g ⁻¹' {b})), f ↑b_1) (∑' (i : β), f i)