harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/Bitwise.lean
theorem bitwise_xor : bitwise xor = Int.xor

Proof state:
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!x ^^ !y) = (x ^^ y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !x ^^ !y) = xor

Tactic:
funext x y

Result:
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!x ^^ !y) = (x ^^ y)

Proof state:
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x ^^ y)) = (x ^^ y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
⊢ bitwise xor = Int.xor

Tactic:
funext m n

Result:
case h.h
m n : ℤ
⊢ bitwise xor m n = m.xor n

Proof state:
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(x ^^ !y)) = (x ^^ y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x ^^ y)) m n = Nat.bitwise xor m n

Tactic:
congr

Result:
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x ^^ y)) = xor

Proof state:
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => !x ^^ !y) m n) = ↑(Nat.bitwise xor m n)

Tactic:
congr

Result:
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => !x ^^ !y) = xor

Proof state:
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y => !(x ^^ !y)) m n = Nat.bitwise xor m n

Tactic:
congr

Result:
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun x y => !(x ^^ !y)) = xor

Proof state:
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

Tactic:
rfl

Result:
no goals

Proof state:
case h.h
m n : ℤ
⊢ bitwise xor m n = m.xor n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
  <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, Bool.bne_eq_xor,
    cond_false, cond_true, lor, Nat.ldiff, Bool.and_true, negSucc.injEq, Bool.false_xor,
    Bool.true_xor, Bool.and_false, Nat.land, Bool.not_true, ldiff,
    HOr.hOr, OrOp.or, Nat.lor, Int.xor, HXor.hXor, Xor.xor, Nat.xor]

Result:
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y => !(x ^^ !y)) m n = Nat.bitwise xor m n

case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x ^^ y)) m n = Nat.bitwise xor m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => !x ^^ !y) m n) = ↑(Nat.bitwise xor m n)

Proof state:
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun x y => !(x ^^ !y)) = xor

Tactic:
funext x y

Result:
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(x ^^ !y)) = (x ^^ y)

Proof state:
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x ^^ y)) = xor

Tactic:
funext x y

Result:
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x ^^ y)) = (x ^^ y)
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem stronglyMeasurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
    [h : SecondCountableTopologyEither 𝕜 F] (f : 𝕜 → F) : StronglyMeasurable (deriv f)

Proof state:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)

Tactic:
exact (measurable_deriv f).stronglyMeasurable

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
⊢ StronglyMeasurable (deriv f)

Tactic:
rcases h.out with h𝕜|hF

Result:
case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
h𝕜 : SecondCountableTopology 𝕜
⊢ StronglyMeasurable (deriv f)

case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hF : SecondCountableTopology F
⊢ StronglyMeasurable (deriv f)

Proof state:
case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
h𝕜 : SecondCountableTopology 𝕜
⊢ StronglyMeasurable (deriv f)

Tactic:
exact stronglyMeasurable_iff_measurable_separable.2
  ⟨measurable_deriv f, isSeparable_range_deriv _⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
⊢ StronglyMeasurable (deriv f)

Tactic:
borelize F

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither 𝕜 F
f : 𝕜 → F
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
⊢ StronglyMeasurable (deriv f)
-- Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
theorem coe_ae_eq_Icc : (I : Set (ι → ℝ)) =ᵐ[volume] Box.Icc I

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ (univ.pi fun i => Ioc (I.lower i) (I.upper i)) =ᶠ[ae volume] Box.Icc I

Tactic:
exact Measure.univ_pi_Ioc_ae_eq_Icc

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ ↑I =ᶠ[ae volume] Box.Icc I

Tactic:
rw [coe_eq_pi]

Result:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ (univ.pi fun i => Ioc (I.lower i) (I.upper i)) =ᶠ[ae volume] Box.Icc I
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem mk_set_nat : #(Set ℕ) = 𝔠

Proof state:
⊢ #(Set ℕ) = 𝔠

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_lt_fib_succ {n : ℕ} (hn : 2 ≤ n) : fib n < fib (n + 1)

Proof state:
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ fib (2 + n) < fib (2 + n + 1)

Tactic:
rw [← tsub_pos_iff_lt, add_comm 2, add_right_comm, fib_add_two, add_tsub_cancel_right, fib_pos]

Result:
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < n + 1

Proof state:
n : ℕ
hn : 2 ≤ n
⊢ fib n < fib (n + 1)

Tactic:
rcases exists_add_of_le hn with ⟨n, rfl⟩

Result:
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ fib (2 + n) < fib (2 + n + 1)

Proof state:
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < n + 1

Tactic:
exact succ_pos n

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_div_const (f : ℝ → ℂ) (s a : ℂ) : mellin (fun t => f t / a) s = mellin f s / a

Proof state:
f : ℝ → ℂ
s a : ℂ
⊢ mellin (fun t => f t / a) s = mellin f s / a

Tactic:
simp_rw [mellin, smul_eq_mul, ← mul_div_assoc, integral_div]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem xgcdAux_rec {r s t r' s' t'} (h : 0 < r) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Proof state:
case intro
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ r.succ.xgcdAux s t r' s' t' = (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t

Tactic:
simp [xgcdAux]

Result:
no goals

Proof state:
r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t

Tactic:
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'

Result:
case intro
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ r.succ.xgcdAux s t r' s' t' = (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W.negY Q * P z) :
    W.dblY P / W.dblZ P = W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblY P / W.dblZ P =
    (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
      ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz hx hy,
  dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_eq_self {s} : filter p s = s ↔ ∀ a ∈ s, p a :=
  Quot.inductionOn s fun _l =>
    Iff.trans ⟨fun h => (filter_sublist _).eq_of_length (congr_arg card h),
      congr_arg ofList⟩ <| by simp

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b => decide (p b)) _l = _l ↔ ∀ a ∈ Quot.mk (⇑(isSetoid α)) _l, p a

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem Fintype.linearIndependent_iff' [Fintype ι] [DecidableEq ι] :
    LinearIndependent R v ↔
      LinearMap.ker (LinearMap.lsum R (fun _ ↦ R) ℕ fun i ↦ LinearMap.id.smulRight (v i)) = ⊥

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ LinearIndependent R v ↔ LinearMap.ker ((LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.id.smulRight (v i)) = ⊥

Tactic:
simp [Fintype.linearIndependent_iff, LinearMap.ker_eq_bot', funext_iff]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
lemma isBigO_mul_iff_isBigO_div {f g h : α → 𝕜} (hf : ∀ᶠ x in l, f x ≠ 0) :
    (fun x ↦ f x * g x) =O[l] h ↔ g =O[l] (fun x ↦ h x / f x)

Proof state:
case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h x‖

Tactic:
rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖

Tactic:
refine H.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_

Result:
case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h x‖

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x => f x * g x) =O[l] h ↔ g =O[l] fun x => h x / f x

Tactic:
rw [isBigO_iff', isBigO_iff']

Result:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_zero : (0 : Angle).toReal = 0

Proof state:
⊢ toReal 0 = 0

Tactic:
rw [← coe_zero, toReal_coe_eq_self_iff]

Result:
⊢ -π < 0 ∧ 0 ≤ π

Proof state:
⊢ -π < 0 ∧ 0 ≤ π

Tactic:
exact ⟨Left.neg_neg_iff.2 Real.pi_pos, Real.pi_pos.le⟩

Result:
no goals
-- Mathlib/Order/Directed.lean
lemma pi {d : (i : ι) → Set (α i)} (hd : ∀ (i : ι), DirectedOn (r i) (d i)) :
    DirectedOn (fun x y => ∀ i, r i (x i) (y i)) (Set.pi Set.univ d)

Proof state:
ι : Type u_1
α : ι → Type u_2
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
⊢ ∃ z ∈ Set.univ.pi d, (fun x y => ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y => ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
choose f hfd haf hbf using fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)

Result:
ι : Type u_1
α : ι → Type u_2
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
f : (i : ι) → α i
hfd : ∀ (i : ι), f i ∈ d i
haf : ∀ (i : ι), r i (a i) (f i)
hbf : ∀ (i : ι), r i (b i) (f i)
⊢ ∃ z ∈ Set.univ.pi d, (fun x y => ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y => ∀ (i : ι), r i (x i) (y i)) b z

Proof state:
ι : Type u_1
α : ι → Type u_2
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
f : (i : ι) → α i
hfd : ∀ (i : ι), f i ∈ d i
haf : ∀ (i : ι), r i (a i) (f i)
hbf : ∀ (i : ι), r i (b i) (f i)
⊢ ∃ z ∈ Set.univ.pi d, (fun x y => ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y => ∀ (i : ι), r i (x i) (y i)) b z

Tactic:
exact ⟨f, fun i _ => hfd i, haf, hbf⟩

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
⊢ DirectedOn (fun x y => ∀ (i : ι), r i (x i) (y i)) (Set.univ.pi d)

Tactic:
intro a ha b hb

Result:
ι : Type u_1
α : ι → Type u_2
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.univ.pi d
b : (i : ι) → α i
hb : b ∈ Set.univ.pi d
⊢ ∃ z ∈ Set.univ.pi d, (fun x y => ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y => ∀ (i : ι), r i (x i) (y i)) b z
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem pow_p_dvd_int_iff (n : ℕ) (a : ℤ) : (p : ℤ_[p]) ^ n ∣ a ↔ (p ^ n : ℤ) ∣ a

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ ↑a ↔ ↑p ^ n ∣ a

Tactic:
rw [← Nat.cast_pow, ← norm_int_le_pow_iff_dvd, norm_le_pow_iff_mem_span_pow,
  Ideal.mem_span_singleton, Nat.cast_pow]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_sum {ι : Type*} {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (t : SignType)
    (h : ∀ i ∈ s, sign (f i) = t) : sign (∑ i ∈ s, f i) = t

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i < 0
⊢ ∑ i ∈ s, f i < 0

Tactic:
exact Finset.sum_neg h hs

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = zero
⊢ sign (∑ i ∈ s, f i) = zero

Tactic:
simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢

Result:
case zero
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i = 0
⊢ ∑ i ∈ s, f i = 0

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Tactic:
simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢

Result:
case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, 0 < f i
⊢ 0 < ∑ i ∈ s, f i

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, sign (f i) = t
⊢ sign (∑ i ∈ s, f i) = t

Tactic:
cases t

Result:
case zero
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = zero
⊢ sign (∑ i ∈ s, f i) = zero

case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

Tactic:
simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢

Result:
case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i < 0
⊢ ∑ i ∈ s, f i < 0

Proof state:
case zero
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i = 0
⊢ ∑ i ∈ s, f i = 0

Tactic:
exact Finset.sum_eq_zero h

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, 0 < f i
⊢ 0 < ∑ i ∈ s, f i

Tactic:
exact Finset.sum_pos h hs

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean
@[to_additive] lemma exists_one_le_mul_of_le [MulLeftReflectLE α] (h : a ≤ b) :
    ∃ c, 1 ≤ c ∧ a * c = b

Proof state:
case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a : α
inst✝ : MulLeftReflectLE α
c : α
h : a ≤ a * c
⊢ ∃ c_1, 1 ≤ c_1 ∧ a * c_1 = a * c

Tactic:
exact ⟨c, one_le_of_le_mul_right h, rfl⟩

Result:
no goals

Proof state:
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a b : α
inst✝ : MulLeftReflectLE α
h : a ≤ b
⊢ ∃ c, 1 ≤ c ∧ a * c = b

Tactic:
obtain ⟨c, rfl⟩ := exists_mul_of_le h

Result:
case intro
α : Type u
inst✝³ : MulOneClass α
inst✝² : Preorder α
inst✝¹ : ExistsMulOfLE α
a : α
inst✝ : MulLeftReflectLE α
c : α
h : a ≤ a * c
⊢ ∃ c_1, 1 ≤ c_1 ∧ a * c_1 = a * c
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_nonneg_iff [NonnegSpectrumClass R A] (f : R → R) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (a_1 : ↑(spectrum R a)), 0 a_1 ≤ { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } a_1) ↔
    ∀ x ∈ spectrum R a, 0 ≤ f x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.650328) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x

Tactic:
rw [cfc_apply .., cfcHom_nonneg_iff, ContinuousMap.le_def]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (a_1 : ↑(spectrum R a)), 0 a_1 ≤ { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } a_1) ↔
    ∀ x ∈ spectrum R a, 0 ≤ f x
-- Mathlib/LinearAlgebra/Dual.lean
theorem isCompl_dualAnnihilator {W W' : Subspace K V₁} (h : IsCompl W W') :
    IsCompl W.dualAnnihilator W'.dualAnnihilator

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : IsCompl W W'
⊢ IsCompl (dualAnnihilator W) (dualAnnihilator W')

Tactic:
rw [isCompl_iff, disjoint_iff, codisjoint_iff] at h ⊢

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ ⊥ = ⊥ ∧ ⊤ = ⊤

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤

Tactic:
rw [← dualAnnihilator_inf_eq, ← dualAnnihilator_sup_eq, h.1, h.2, dualAnnihilator_top,
  dualAnnihilator_bot]

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ ⊥ = ⊥ ∧ ⊤ = ⊤
-- Mathlib/CategoryTheory/Limits/Shapes/Countable.lean
theorem sequentialFunctor_initial_aux (j : J) : ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j

Proof state:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ ∃ n, sequentialFunctor_obj J n ≤ j

Tactic:
refine ⟨m + 1, ?_⟩

Result:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ sequentialFunctor_obj J (m + 1) ≤ j

Proof state:
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
⊢ ∃ n, sequentialFunctor_obj J n ≤ j

Tactic:
obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j

Result:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ ∃ n, sequentialFunctor_obj J n ≤ j

Proof state:
case intro
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ sequentialFunctor_obj J (m + 1) ≤ j

Tactic:
simpa only [h] using leOfHom (IsCofilteredOrEmpty.cone_objs ((exists_surjective_nat _).choose m)
  (sequentialFunctor_obj J m)).choose_spec.choose

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_left {s t : Multiset α} : Disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t

Proof state:
case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → a ∉ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ ∀ (a : α), a ∉ u

Tactic:
exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

Result:
no goals

Proof state:
case refine_1
α : Type u_1
s t : Multiset α
h : _root_.Disjoint s t
a : α
hs : a ∈ s
ht : a ∈ t
⊢ False

Tactic:
simpa using h (singleton_le.mpr hs) (singleton_le.mpr ht)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → a ∉ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ u ≤ ⊥

Tactic:
rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_not_mem]

Result:
case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → a ∉ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ ∀ (a : α), a ∉ u

Proof state:
α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ {a : α}, a ∈ s → a ∉ t

Tactic:
refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩

Result:
case refine_1
α : Type u_1
s t : Multiset α
h : _root_.Disjoint s t
a : α
hs : a ∈ s
ht : a ∈ t
⊢ False

case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → a ∉ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ u ≤ ⊥