harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_mul_aleph0 {m : ℕ∞} (hm : m ≠ 0) : ↑m * ℵ₀ = ℵ₀

Proof state:
case top
hm : ⊤ ≠ 0
⊢ ↑⊤ * ℵ₀ = ℵ₀

Tactic:
exact aleph0_mul_aleph0

Result:
no goals

Proof state:
case coe
m : ℕ
hm : ↑m ≠ 0
⊢ ↑↑m * ℵ₀ = ℵ₀

Tactic:
rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]

Result:
no goals

Proof state:
m : ℕ∞
hm : m ≠ 0
⊢ ↑m * ℵ₀ = ℵ₀

Tactic:
induction m with
| top => exact aleph0_mul_aleph0
| coe m => rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualBasis_apply_self (i j : ι) : b.dualBasis i (b j) =
    if j = i then 1 else 0

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ (b.dualBasis i) (b j) = if j = i then 1 else 0

Tactic:
convert b.toDual_apply i j using 2

Result:
case h.e'_3.h₁.a
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ j = i ↔ i = j

Proof state:
case h.e'_3.h₁.a
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ j = i ↔ i = j

Tactic:
rw [@eq_comm _ j i]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem forall_mem_image {f : α → β} {s : Set α} {p : β → Prop} :
    (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem d_comp_eqToHom {i j j' : ι} (rij : c.Rel i j) (rij' : c.Rel i j') :
    C.d i j' ≫ eqToHom (congr_arg C.X (c.next_eq rij' rij)) = C.d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j j' : ι
rij : c.Rel i j
rij' : c.Rel i j'
⊢ C.d i j' ≫ eqToHom ⋯ = C.d i j

Tactic:
obtain rfl := c.next_eq rij rij'

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : c.Rel i j
⊢ C.d i j ≫ eqToHom ⋯ = C.d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : c.Rel i j
⊢ C.d i j ≫ eqToHom ⋯ = C.d i j

Tactic:
simp only [eqToHom_refl, comp_id]

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem ofLE_refl : ofLE (le_refl A) = id

Proof state:
case h.mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ ofLE ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
⊢ ofLE ⋯ = id

Tactic:
ext ⟨⟩

Result:
case h.mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ ofLE ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem lcm_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
    s₁.lcm f = s₂.lcm g

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.lcm f = s₁.lcm g

Tactic:
exact Finset.fold_congr hfg

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.lcm f = s₂.lcm g

Tactic:
subst hs

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.lcm f = s₁.lcm g
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_coord_change_source_mem_nhdsWithin' {x : M} (hxf : x ∈ f.source)
    (hxf' : x ∈ f'.source) :
    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] f.extend I x

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range ↑I] ↑(f.extend I) x

Tactic:
apply extend_coord_change_source_mem_nhdsWithin

Result:
case hx
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f.extend I) x ∈ ((f.extend I).symm ≫ f'.extend I).source

Proof state:
case hx
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f.extend I) x ∈ ((f.extend I).symm ≫ f'.extend I).source

Tactic:
rw [← extend_image_source_inter]

Result:
case hx
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f.extend I) x ∈ ↑(f.extend I) '' (f.source ∩ f'.source)

Proof state:
case hx
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f.extend I) x ∈ ↑(f.extend I) '' (f.source ∩ f'.source)

Tactic:
exact mem_image_of_mem _ ⟨hxf, hxf'⟩

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq {n : ℕ}
    (h : FiniteMultiplicity a b) : emultiplicity a b = n ↔ multiplicity a b = n

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑n ↔ multiplicity a b = n

Tactic:
simp [h.emultiplicity_eq_multiplicity]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem map_eq_nil {β : Type*} (f : α → β) (s : Cycle α) : map f s = nil ↔ s = nil :=
  Quotient.inductionOn' s (by simp)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Cycle α
⊢ ∀ (a : List α), map f (Quotient.mk'' a) = nil ↔ Quotient.mk'' a = nil

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem coeff_p_one [CharP R p] : (p : 𝕎 R).coeff 1 = 1

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ (↑p).coeff 1 = 1

Tactic:
rw [coeff_p, if_pos rfl]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem DecEq_eq [DecidableEq α] :
    List.instBEq = @instBEqOfDecidableEq (List α) instDecidableEqList :=
  congr_arg BEq.mk <| by
    funext l₁ l₂
    show (l₁ == l₂) = _
    rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ == l₂) = decide (l₁ = l₂)

Tactic:
rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]

Result:
no goals

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁.beq l₂ = decide (l₁ = l₂)

Tactic:
show (l₁ == l₂) = _

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ == l₂) = decide (l₁ = l₂)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ List.beq = fun a b => decide (a = b)

Tactic:
funext l₁ l₂

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁.beq l₂ = decide (l₁ = l₂)
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma CWComplex.union [CWComplex C] : ⋃ (n : ℕ) (j : cell C n), closedCell n j = C

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ∅ ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Tactic:
rw [empty_union] at this

Result:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Tactic:
exact this

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Tactic:
have := RelCWComplex.union' (C := C) (D := ∅)

Result:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ∅ ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C
-- Mathlib/CategoryTheory/Equivalence.lean
theorem invFunIdAssoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
    (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ (𝟙 (F.obj X) ≫ F.map (e.counitIso.inv.app X)) ≫ 𝟙 (F.obj (e.functor.obj (e.inverse.obj X))) =
    F.map (e.counitInv.app X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)

Tactic:
dsimp [invFunIdAssoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ (𝟙 (F.obj X) ≫ F.map (e.counitIso.inv.app X)) ≫ 𝟙 (F.obj (e.functor.obj (e.inverse.obj X))) =
    F.map (e.counitInv.app X)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
@[reassoc (attr := simp)]
lemma pushout_inr_inv_inl_of_right_isIso :
    pushout.inr f g ≫ inv (pushout.inl f g) = inv g ≫ f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inr f g ≫ inv (pushout.inl f g) = inv g ≫ f

Tactic:
rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
    {f : Option β → Option β} (h : (k == k') = false) :
    (Const.alter m k f).contains k' = m.contains k'

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : (k == k') = false
⊢ (alter m k f).contains k' = m.contains k'

Tactic:
simp only [contains_alter, h, Bool.false_eq_true, reduceIte]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
    (replicate n a).filterMap f = replicate n b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
n : Nat
f : α → Option β
h : f a = some b
⊢ filterMap f (replicate n a) = replicate n b

Tactic:
simp [filterMap_replicate, h]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_eq_toNNReal_iff {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
    toNNReal r = toNNReal p ↔ r = p

Proof state:
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ r.toNNReal = p.toNNReal ↔ r = p

Tactic:
simp [← coe_inj, coe_toNNReal, hr, hp]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem count_sum [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} :
    count a (map f m).sum = sum (m.map fun b => count a <| f b) :=
  Multiset.induction_on m (by simp) (by simp)

Proof state:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ ∀ (a_1 : β) (s : Multiset β),
    count a (map f s).sum = (map (fun b => count a (f b)) s).sum →
      count a (map f (a_1 ::ₘ s)).sum = (map (fun b => count a (f b)) (a_1 ::ₘ s)).sum

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
m : Multiset β
f : β → Multiset α
a : α
⊢ count a (map f 0).sum = (map (fun b => count a (f b)) 0).sum

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_lf {x : PGame} : 0 ⧏ x ↔ ∃ i, ∀ j, 0 ⧏ (x.moveLeft i).moveRight j

Proof state:
x : PGame
⊢ ((∃ i,
        (∀ (i' : LeftMoves 0), moveLeft 0 i' ⧏ x.moveLeft i) ∧
          ∀ (j : (x.moveLeft i).RightMoves), 0 ⧏ (x.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (moveRight 0 j).LeftMoves), (moveRight 0 j).moveLeft i ⧏ x) ∧
          ∀ (j' : x.RightMoves), moveRight 0 j ⧏ x.moveRight j') ↔
    ∃ i, ∀ (j : (x.moveLeft i).RightMoves), 0 ⧏ (x.moveLeft i).moveRight j

Tactic:
simp

Result:
no goals

Proof state:
x : PGame
⊢ 0 ⧏ x ↔ ∃ i, ∀ (j : (x.moveLeft i).RightMoves), 0 ⧏ (x.moveLeft i).moveRight j

Tactic:
rw [lf_def]

Result:
x : PGame
⊢ ((∃ i,
        (∀ (i' : LeftMoves 0), moveLeft 0 i' ⧏ x.moveLeft i) ∧
          ∀ (j : (x.moveLeft i).RightMoves), 0 ⧏ (x.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (moveRight 0 j).LeftMoves), (moveRight 0 j).moveLeft i ⧏ x) ∧
          ∀ (j' : x.RightMoves), moveRight 0 j ⧏ x.moveRight j') ↔
    ∃ i, ∀ (j : (x.moveLeft i).RightMoves), 0 ⧏ (x.moveLeft i).moveRight j
-- Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean
@[simp] lemma sup'_eq_zero (hs) : s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedAddCommMonoid α
inst✝ : CanonicallyOrderedAdd α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp [sup'_eq_sup]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsLE_inv {a : H} : Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)

Tactic:
simpa only [inv_inv] using @tendsto_inv_nhdsLE _ _ _ _ a⁻¹

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem mul_inv_mul_mul_mem_range_inl : (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂ ∈ S.inl.range

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
⊢ (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂ ∈ S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
  mul_assoc, inv_mul_cancel]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_add_le (w : InfinitePlace K) (x y : mixedSpace K) :
    normAtPlace w (x + y) ≤ normAtPlace w x + normAtPlace w y

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (normAtPlace w) (x + y) ≤ (normAtPlace w) x + (normAtPlace w) y

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x + y).1 ⟨w, hw⟩‖ else ‖(x + y).2 ⟨w, ⋯⟩‖) ≤
    (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) + if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x + y).1 ⟨w, hw⟩‖ else ‖(x + y).2 ⟨w, ⋯⟩‖) ≤
    (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) + if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs <;> exact norm_add_le _ _

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem neg_mem_closedBall_zero {r : ℝ} {x : E} : -x ∈ closedBall p 0 r ↔ x ∈ closedBall p 0 r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -x ∈ p.closedBall 0 r ↔ x ∈ p.closedBall 0 r

Tactic:
simp only [mem_closedBall_zero, map_neg_eq_map]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem GammaIntegral_conj (s : ℂ) : GammaIntegral (conj s) = conj (GammaIntegral s)

Proof state:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) = (starRingEnd ℂ) (↑(rexp (-x)) * ↑x ^ (s - 1))

Tactic:
rw [RingHom.map_mul, conj_ofReal, cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)),
  cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), ← exp_conj, RingHom.map_mul, ←
  ofReal_log (le_of_lt hx), conj_ofReal, RingHom.map_sub, RingHom.map_one]

Result:
no goals

Proof state:
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) =
    ∫ (x : ℝ) in Ioi 0, (starRingEnd ℂ) (↑(rexp (-x)) * ↑x ^ (s - 1))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Result:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) = (starRingEnd ℂ) (↑(rexp (-x)) * ↑x ^ (s - 1))

Proof state:
s : ℂ
⊢ ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral

Tactic:
rw [GammaIntegral, GammaIntegral, ← integral_conj]

Result:
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) =
    ∫ (x : ℝ) in Ioi 0, (starRingEnd ℂ) (↑(rexp (-x)) * ↑x ^ (s - 1))
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelπ_apply_dom_eq_zero {X Y : SemiNormedGrp.{u}} {f : X ⟶ Y} (x : X) :
    (explicitCokernelπ f) (f x) = 0 :=
  show (f ≫ explicitCokernelπ f) x = 0 by rw [comp_explicitCokernelπ]; rfl

Proof state:
X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
⊢ (ConcreteCategory.hom 0) x = 0

Tactic:
rfl

Result:
no goals

Proof state:
X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
⊢ (ConcreteCategory.hom (f ≫ explicitCokernelπ f)) x = 0

Tactic:
rw [comp_explicitCokernelπ]

Result:
X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
⊢ (ConcreteCategory.hom 0) x = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β k → β k} :
    (m.modify k f).getKey! k = if m.contains k then k else default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
inst✝ : Inhabited α
k : α
f : β k → β k
⊢ (m.modify k f).getKey! k = if m.contains k = true then k else default

Tactic:
simp_to_model [modify] using List.getKey!_modifyKey_self

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mem_graph_iff {c : α × M} {f : α →₀ M} : c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0

Proof state:
case mk
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
fst✝ : α
snd✝ : M
⊢ (fst✝, snd✝) ∈ f.graph ↔ f (fst✝, snd✝).1 = (fst✝, snd✝).2 ∧ (fst✝, snd✝).2 ≠ 0

Tactic:
exact mk_mem_graph_iff

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
c : α × M
f : α →₀ M
⊢ c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0

Tactic:
cases c

Result:
case mk
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
fst✝ : α
snd✝ : M
⊢ (fst✝, snd✝) ∈ f.graph ↔ f (fst✝, snd✝).1 = (fst✝, snd✝).2 ∧ (fst✝, snd✝).2 ≠ 0
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_eq_zero : logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Proof state:
b x : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
simp_rw [logb, div_eq_zero_iff, log_eq_zero]

Result:
b x : ℝ
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Proof state:
b x : ℝ
⊢ (x = 0 ∨ x = 1 ∨ x = -1) ∨ b = 0 ∨ b = 1 ∨ b = -1 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
tauto

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean
lemma epi_π_app_zero_of_epi [HasSheafify (coherentTopology C) (Type v)]
    [Balanced (Sheaf (coherentTopology C) (Type v))]
    [(coherentTopology C).WEqualsLocallyBijective (Type v)]
    {F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)}
    {c : Cone F} (hc : IsLimit c)
    (hF : ∀ n, Epi (F.map (homOfLE (Nat.le_succ n)).op)) : Epi (c.π.app ⟨0⟩)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preregular C
inst✝⁴ : FinitaryExtensive C
inst✝³ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
inst✝² : HasSheafify (coherentTopology C) (Type v)
inst✝¹ : Balanced (Sheaf (coherentTopology C) (Type v))
inst✝ : (coherentTopology C).WEqualsLocallyBijective (Type v)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (op 0))

Tactic:
simp_rw [← Sheaf.isLocallySurjective_iff_epi'] at hF ⊢

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preregular C
inst✝⁴ : FinitaryExtensive C
inst✝³ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
inst✝² : HasSheafify (coherentTopology C) (Type v)
inst✝¹ : Balanced (Sheaf (coherentTopology C) (Type v))
inst✝ : (coherentTopology C).WEqualsLocallyBijective (Type v)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
⊢ Sheaf.IsLocallySurjective (c.π.app (op 0))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preregular C
inst✝⁴ : FinitaryExtensive C
inst✝³ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
inst✝² : HasSheafify (coherentTopology C) (Type v)
inst✝¹ : Balanced (Sheaf (coherentTopology C) (Type v))
inst✝ : (coherentTopology C).WEqualsLocallyBijective (Type v)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
⊢ Sheaf.IsLocallySurjective (c.π.app (op 0))

Tactic:
exact isLocallySurjective_π_app_zero_of_isLocallySurjective_map hc hF h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_le_laverage_pos (hμ : μ ≠ 0) (hf : AEMeasurable f μ) :
    0 < μ {x | f x ≤ ⨍⁻ a, f a ∂μ}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
⊢ 0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}

Tactic:
simpa using
  measure_le_setLaverage_pos (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _) hf.restrict

Result:
no goals