harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_apply_zero (n : ℕ) :
    (expSeries 𝕂 𝔸 n fun _ => (0 : 𝔸)) = Pi.single (f := fun _ => 𝔸) 0 1 n

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n

Tactic:
rcases n with - | n

Result:
case zero
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (↑0!)⁻¹ • 0 ^ 0 = Pi.single 0 1 0

case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑(n + 1)!)⁻¹ • 0 ^ (n + 1) = Pi.single 0 1 (n + 1)

Proof state:
case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑(n + 1)!)⁻¹ • 0 ^ (n + 1) = Pi.single 0 1 (n + 1)

Tactic:
rw [zero_pow (Nat.succ_ne_zero _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]

Result:
no goals

Proof state:
case zero
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (↑0!)⁻¹ • 0 ^ 0 = Pi.single 0 1 0

Tactic:
rw [pow_zero, Nat.factorial_zero, Nat.cast_one, inv_one, one_smul, Pi.single_eq_same]

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x => 0) = Pi.single 0 1 n

Tactic:
rw [expSeries_apply_eq]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem isOpen_Ico_zero : IsOpen (Ico 0 b)

Proof state:
b : ℝ≥0∞
⊢ IsOpen (Ico 0 b)

Tactic:
rw [ENNReal.Ico_eq_Iio]

Result:
b : ℝ≥0∞
⊢ IsOpen (Iio b)

Proof state:
b : ℝ≥0∞
⊢ IsOpen (Iio b)

Tactic:
exact isOpen_Iio

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
lemma SigmaFinite.withDensity_of_ne_top [SigmaFinite μ] {f : α → ℝ≥0∞}
    (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) : SigmaFinite (μ.withDensity f)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : f =ᶠ[ae μ] fun x => ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity f)

Tactic:
rw [withDensity_congr_ae this]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : f =ᶠ[ae μ] fun x => ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity fun x => ↑(f x).toNNReal)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : f =ᶠ[ae μ] fun x => ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity fun x => ↑(f x).toNNReal)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ SigmaFinite (μ.withDensity f)

Tactic:
have : f =ᵐ[μ] fun x ↦ (f x).toNNReal := hf_ne_top.mono fun x hx ↦ (ENNReal.coe_toNNReal hx).symm

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : f =ᶠ[ae μ] fun x => ↑(f x).toNNReal
⊢ SigmaFinite (μ.withDensity f)
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[simp]
lemma SpecTensorTo_SpecOfPoint (t : ↑(pullback f g)) :
    (Triplet.ofPoint t).SpecTensorTo.base (SpecOfPoint t) = t

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ (ConcreteCategory.hom (Triplet.ofPoint t).SpecTensorTo.base) (SpecOfPoint t) = t

Tactic:
simp [SpecOfPoint, ← Scheme.comp_base_apply, ofPointTensor_SpecTensorTo]

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
theorem CharZero.of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
n m : ℕ
h : ↑n = ↑m
x : M
hx : x ≠ 0
⊢ n = m

Tactic:
replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
n m : ℕ
x : M
hx : x ≠ 0
h : ↑n • x = ↑m • x
⊢ n = m

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
n m : ℕ
h : ↑n = ↑m
x : M
hx : x ≠ 0
⊢ ↑n • x = ↑m • x

Tactic:
simp [← Nat.cast_smul_eq_nsmul R, h]

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
n m : ℕ
x : M
hx : x ≠ 0
h : ↑n • x = ↑m • x
⊢ n = m

Tactic:
simpa using smul_left_injective ℤ hx h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
n m : ℕ
h : ↑n = ↑m
⊢ n = m

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
n m : ℕ
h : ↑n = ↑m
x : M
hx : x ≠ 0
⊢ n = m

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
⊢ CharZero R

Tactic:
refine ⟨fun {n m h} ↦ ?_⟩

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors ℤ M
n m : ℕ
h : ↑n = ↑m
⊢ n = m
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem IsOpenMap.coverPreserving (hf : IsOpenMap f) :
    CoverPreserving (Opens.grothendieckTopology X) (Opens.grothendieckTopology Y) hf.functor

Proof state:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) hf.functor

Tactic:
constructor

Result:
case cover_preserve
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
⊢ ∀ {U : Opens ↑X} {S : Sieve U},
    S ∈ (Opens.grothendieckTopology ↑X) U →
      Sieve.functorPushforward hf.functor S ∈ (Opens.grothendieckTopology ↑Y) (hf.functor.obj U)

Proof state:
case cover_preserve.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑X
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hx : x ∈ ↑U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ (ConcreteCategory.hom f) x ∈ U_1

Tactic:
obtain ⟨V, i, hV, hxV⟩ := hU x hx

Result:
case cover_preserve.intro.intro.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑X
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ (ConcreteCategory.hom f) x ∈ U_1

Proof state:
case cover_preserve.intro.intro.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑X
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ (ConcreteCategory.hom f) x ∈ U_1

Tactic:
exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩

Result:
no goals

Proof state:
case cover_preserve
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
⊢ ∀ {U : Opens ↑X} {S : Sieve U},
    S ∈ (Opens.grothendieckTopology ↑X) U →
      Sieve.functorPushforward hf.functor S ∈ (Opens.grothendieckTopology ↑Y) (hf.functor.obj U)

Tactic:
rintro U S hU _ ⟨x, hx, rfl⟩

Result:
case cover_preserve.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑X
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hx : x ∈ ↑U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ (ConcreteCategory.hom f) x ∈ U_1
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem nullMeasurableSet_eq_fun {E} [TopologicalSpace E] [MetrizableSpace E] {f g : α → E}
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
    NullMeasurableSet { x | f x = g x } μ

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {x | f x = g x}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Result:
case h
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} x = {x | f x = g x} x

Proof state:
case h
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x) = (f x = g x)

Tactic:
simp only [hfx, hgx]

Result:
no goals

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {x | f x = g x} μ

Tactic:
apply
  (hf.stronglyMeasurable_mk.measurableSet_eq_fun
        hg.stronglyMeasurable_mk).nullMeasurableSet.congr

Result:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {x | f x = g x}

Proof state:
case h
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} x = {x | f x = g x} x

Tactic:
change (hf.mk f x = hg.mk g x) = (f x = g x)

Result:
case h
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x) = (f x = g x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_and (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
    decide (p ∧ q) = (p && q)

Proof state:
case isTrue
p✝ q : Prop
dpq : Decidable (p✝ ∧ q)
dq : Decidable q
p : p✝
⊢ decide (p✝ ∧ q) = (decide p✝ && decide q)

Tactic:
simp [p]

Result:
no goals

Proof state:
p q : Prop
dpq : Decidable (p ∧ q)
dp : Decidable p
dq : Decidable q
⊢ decide (p ∧ q) = (decide p && decide q)

Tactic:
cases dp with | _ p => simp [p]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_basis_not_at_node (hi : i ∈ s) (hxi : x ≠ v i) :
    eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)

Tactic:
rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
  nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
  mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
protected lemma inv_pos : 0 < z⁻¹ ↔ 0 < z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z⁻¹⁻¹

Tactic:
exact RCLike.inv_pos_of_pos h

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z⁻¹ ↔ 0 < z

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

Result:
K : Type u_1
inst✝ : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z

Tactic:
rw [← inv_inv z]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z⁻¹⁻¹
-- Mathlib/Data/Finset/MulAntidiagonal.lean
theorem support_mulAntidiagonal_subset_mul : { a | (mulAntidiagonal hs ht a).Nonempty } ⊆ s * t :=
  fun a ⟨b, hb⟩ => by
  rw [mem_mulAntidiagonal] at hb
  exact ⟨b.1, hb.1, b.2, hb.2⟩

Proof state:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x✝ : a ∈ {a | (mulAntidiagonal hs ht a).Nonempty}
b : α × α
hb : b ∈ mulAntidiagonal hs ht a
⊢ a ∈ s * t

Tactic:
rw [mem_mulAntidiagonal] at hb

Result:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x✝ : a ∈ {a | (mulAntidiagonal hs ht a).Nonempty}
b : α × α
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a
⊢ a ∈ s * t

Proof state:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x✝ : a ∈ {a | (mulAntidiagonal hs ht a).Nonempty}
b : α × α
hb : b.1 ∈ s ∧ b.2 ∈ t ∧ b.1 * b.2 = a
⊢ a ∈ s * t

Tactic:
exact ⟨b.1, hb.1, b.2, hb.2⟩

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
lemma pi_norm_le_sum_norm (x : C⋆ᵐᵒᵈ (Π i, E i)) : ‖x‖ ≤ ∑ i, ‖x i‖

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ∑ i : ι, ‖⟪x i, x i⟫_A‖ = ∑ i : ι, ‖x i‖ ^ 2

Tactic:
simp only [norm_sq_eq]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ 0 ≤ ∑ i : ι, ‖x i‖

Tactic:
positivity

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ ≤ ∑ i : ι, ‖x i‖

Tactic:
refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2

Result:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ ^ 2 ≤ (∑ i : ι, ‖x i‖) ^ 2

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ ^ 2 ≤ (∑ i : ι, ‖x i‖) ^ 2

Tactic:
calc ‖x‖ ^ 2 ≤ ∑ i, ‖⟪x i, x i⟫_A‖ := pi_norm_sq x ▸ norm_sum_le _ _
  _ = ∑ i, ‖x i‖ ^ 2 := by simp only [norm_sq_eq]
  _ ≤ (∑ i, ‖x i‖) ^ 2 := sum_sq_le_sq_sum_of_nonneg (fun _ _ ↦ norm_nonneg _)

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma _root_.Irreducible.maximalIdeal_pow_eq_closedBall_pow [IsDiscreteValuationRing 𝒪[K]]
    {ϖ : 𝒪[K]} (h : Irreducible ϖ) (n : ℕ) :
    ((𝓂[K] ^ n : Ideal 𝒪[K]) : Set 𝒪[K]) = Metric.closedBall 0 (‖ϖ‖ ^ n)

Proof state:
K : Type u_1
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
n : ℕ
⊢ ↑(𝓂[K] ^ n) = Metric.closedBall 0 (‖ϖ‖ ^ n)

Tactic:
have : ‖ϖ‖ ^ n = ‖ϖ ^ n‖ := by simp

Result:
K : Type u_1
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
n : ℕ
this : ‖ϖ‖ ^ n = ‖ϖ ^ n‖
⊢ ↑(𝓂[K] ^ n) = Metric.closedBall 0 (‖ϖ‖ ^ n)

Proof state:
K : Type u_1
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
n : ℕ
this : ‖ϖ‖ ^ n = ‖ϖ ^ n‖
⊢ ↑(𝓂[K] ^ n) = Metric.closedBall 0 (‖ϖ‖ ^ n)

Tactic:
rw [this, ← coe_span_singleton_eq_closedBall, ← Ideal.span_singleton_pow, ← h.maximalIdeal_eq]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
n : ℕ
⊢ ‖ϖ‖ ^ n = ‖ϖ ^ n‖

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma isClosed_sUnion (hS : ∀ s ∈ S, IsClosed s) : IsClosed (⋃₀ S)

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
hS : ∀ s ∈ S, IsClosed s
⊢ IsClosed (⋃₀ S)

Tactic:
simp only [← isOpen_compl_iff, compl_sUnion] at hS ⊢

Result:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen sᶜ
⊢ IsOpen (⋂₀ (compl '' S))

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen sᶜ
⊢ IsOpen (⋂₀ (compl '' S))

Tactic:
exact isOpen_sInter <| forall_mem_image.2 hS

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
theorem imageSieve_app {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : ToType (F.obj (op U))) :
    imageSieve f (f.app _ s) = ⊤

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (F.obj (op U))
V : C
i : V ⟶ U
⊢ (imageSieve f ((ConcreteCategory.hom (f.app (op U))) s)).arrows i ↔ ⊤.arrows i

Tactic:
simp only [Sieve.top_apply, iff_true, imageSieve_apply]

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (F.obj (op U))
V : C
i : V ⟶ U
⊢ ∃ t,
    (ConcreteCategory.hom (f.app (op V))) t =
      (ConcreteCategory.hom (G.map i.op)) ((ConcreteCategory.hom (f.app (op U))) s)

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (F.obj (op U))
V : C
i : V ⟶ U
⊢ ∃ t,
    (ConcreteCategory.hom (f.app (op V))) t =
      (ConcreteCategory.hom (G.map i.op)) ((ConcreteCategory.hom (f.app (op U))) s)

Tactic:
exact ⟨F.map i.op s, NatTrans.naturality_apply f i.op s⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (F.obj (op U))
⊢ imageSieve f ((ConcreteCategory.hom (f.app (op U))) s) = ⊤

Tactic:
ext V i

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (F.obj (op U))
V : C
i : V ⟶ U
⊢ (imageSieve f ((ConcreteCategory.hom (f.app (op U))) s)).arrows i ↔ ⊤.arrows i
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem map_iff [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β]
    [BorelSpace β] (f : α ≃ₜ β) :
    InnerRegular (Measure.map f μ) ↔ InnerRegular μ

Proof state:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
⊢ (map (⇑f) μ).InnerRegular ↔ μ.InnerRegular

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ.InnerRegular

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ.InnerRegular

Tactic:
convert h.map f.symm

Result:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Proof state:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm) (map (⇑f) μ)

Tactic:
rw [map_map f.symm.continuous.measurable f.continuous.measurable]

Result:
case h.e'_4
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).InnerRegular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem eq_of_comp_left_eq' (f g : X ⟶ Y)
    (w : (fun {Z} (h : Y ⟶ Z) => f ≫ h) = fun {Z} (h : Y ⟶ Z) => g ≫ h) : f = g :=
  eq_of_comp_left_eq @fun Z h => by convert congr_fun (congr_fun w Z) h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
convert congr_fun (congr_fun w Z) h

Result:
no goals
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem nmul_le {F α : Type*} [Ring α] [FunLike F α ℝ] [AddGroupSeminormClass F α ℝ]
    {f : F} (hna : IsNonarchimedean f) {n : ℕ} {a : α} : f (n * a) ≤ f a

Proof state:
F : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (n • a) ≤ f a

Tactic:
exact nsmul_le hna

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (↑n * a) ≤ f a

Tactic:
rw [← nsmul_eq_mul]

Result:
F : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : AddGroupSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (n • a) ≤ f a