harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem hasStrictDerivAt_abs {x : ℝ} (hx : x ≠ 0) :
    HasStrictDerivAt (|·|) (SignType.sign x : ℝ) x

Proof state:
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (fun x => |x|) (↑(SignType.sign x)) x

Tactic:
simpa [hx] using hasStrictDerivAt_abs_pos hx

Result:
no goals

Proof state:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x => |x|) (↑(SignType.sign x)) x

Tactic:
simpa [hx] using hasStrictDerivAt_abs_neg hx

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt (fun x => |x|) (↑(SignType.sign x)) x

Tactic:
obtain hx | hx := hx.lt_or_lt

Result:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x => |x|) (↑(SignType.sign x)) x

case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (fun x => |x|) (↑(SignType.sign x)) x
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem sup_aux (f g : E →ₗ.[R] F)
    (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) :
    ∃ fg : ↥(f.domain ⊔ g.domain) →ₗ[R] F,
      ∀ (x : f.domain) (y : g.domain) (z : ↥(f.domain ⊔ g.domain)),
        (x : E) + y = ↑z → fg z = f x + g y

Proof state:
case w.refine_1.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z => ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = fg ⟨z₁, hz₁⟩ + fg ⟨z₂, hz₂⟩

Tactic:
rw [← add_assoc, add_right_comm (f _), ← map_add, add_assoc, ← map_add]

Result:
case w.refine_1.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z => ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = ↑f (⟨x ⟨z₁, hz₁⟩, ⋯⟩ + ⟨x ⟨z₂, hz₂⟩, ⋯⟩) + ↑g (⟨y ⟨z₁, hz₁⟩, ⋯⟩ + ⟨y ⟨z₂, hz₂⟩, ⋯⟩)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem mono_snd_of_is_pullback_of_mono {t : PullbackCone f g} (ht : IsLimit t) [Mono f] :
    Mono t.snd

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.fst = k ≫ t.fst

Tactic:
rw [← cancel_mono f, Category.assoc, Category.assoc, condition]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.snd ≫ g = k ≫ t.snd ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.snd ≫ g = k ≫ t.snd ≫ g

Tactic:
apply reassoc_of% i

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
⊢ Mono t.snd

Tactic:
refine ⟨fun {W} h k i => IsLimit.hom_ext ht ?_ i⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.fst = k ≫ t.fst
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_symm_of_eq_add {n a b : ℕ} (h : n = a + b) : Nat.choose n a = Nat.choose n b

Proof state:
n a b : ℕ
h : n = a + b
⊢ n.choose (n - b) = n.choose b

Tactic:
exact choose_symm (h ▸ le_add_left _ _)

Result:
no goals

Proof state:
n a b : ℕ
h : n = a + b
this : n.choose (n - b) = n.choose b
⊢ n.choose a = n.choose b

Tactic:
rw [h, Nat.add_sub_cancel_right] at this

Result:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b

Proof state:
n a b : ℕ
h : n = a + b
⊢ n.choose a = n.choose b

Tactic:
suffices choose n (n - b) = choose n b by
  rw [h, Nat.add_sub_cancel_right] at this; rwa [h]

Result:
n a b : ℕ
h : n = a + b
⊢ n.choose (n - b) = n.choose b

Proof state:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b

Tactic:
rwa [h]

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
lemma sum_mul_Ico_le_integral_of_monotone_antitone
    (hab : a ≤ b) (hf : MonotoneOn f (Icc a b)) (hg : AntitoneOn g (Icc (a - 1) (b - 1)))
    (fpos : 0 ≤ f a) (gpos : 0 ≤ g (b - 1)) :
    ∑ i ∈ Finset.Ico a b, f i * g i ≤ ∫ x in a..b, f x * g (x - 1)

Proof state:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
have I0 : (i : ℝ) ≤ b - 1 := by
  simp only [le_sub_iff_add_le]
  norm_cast
  omega

Result:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
⊢ ↑i + 1 ≤ ↑b

Tactic:
norm_cast

Result:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
⊢ i + 1 ≤ b

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ a ≤ i + 1

Tactic:
omega

Result:
no goals

Proof state:
case h.h₂
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ g ↑i ≤ g (x - 1)

Tactic:
apply hg

Result:
case h.h₂.x
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ x - 1 ∈ Icc (↑a - 1) (↑b - 1)

case h.h₂.x
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑i ∈ Icc (↑a - 1) (↑b - 1)

case h.h₂.a
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ x - 1 ≤ ↑i
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma map_single (r : relations.R) :
    relations.map (Finsupp.single r 1) = relations.relation r

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.map (Finsupp.single r 1) = relations.relation r

Tactic:
simp [map]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem two_le_natDegree_iff (int : IsIntegral A x) :
    2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
int : IsIntegral A x
⊢ 2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range

Tactic:
rw [iff_not_comm, ← natDegree_eq_one_iff, not_le]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
int : IsIntegral A x
⊢ (minpoly A x).natDegree = 1 ↔ (minpoly A x).natDegree < 2

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
int : IsIntegral A x
⊢ (minpoly A x).natDegree = 1 ↔ (minpoly A x).natDegree < 2

Tactic:
exact ⟨fun h ↦ h.trans_lt one_lt_two, fun h ↦ by linarith only [minpoly.natDegree_pos int, h]⟩

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
int : IsIntegral A x
h : (minpoly A x).natDegree < 2
⊢ (minpoly A x).natDegree = 1

Tactic:
linarith only [minpoly.natDegree_pos int, h]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma even_or_odd [NoZeroDivisors S] : ψ.Even ∨ ψ.Odd

Proof state:
S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NoZeroDivisors S
⊢ ψ (-1) ^ 2 = 1

Tactic:
rw [← map_pow _, neg_one_sq, map_one]

Result:
no goals

Proof state:
S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NoZeroDivisors S
⊢ ψ.Even ∨ ψ.Odd

Tactic:
suffices ψ (-1) ^ 2 = 1 by convert sq_eq_one_iff.mp this

Result:
S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NoZeroDivisors S
⊢ ψ (-1) ^ 2 = 1

Proof state:
S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NoZeroDivisors S
this : ψ (-1) ^ 2 = 1
⊢ ψ.Even ∨ ψ.Odd

Tactic:
convert sq_eq_one_iff.mp this

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
lemma IsInvertible.inverse_comp_of_left {g : M₂ →L[R] M₃} {f : M →L[R] M₂}
    (hg : g.IsInvertible) : (g ∘L f).inverse = f.inverse ∘L g.inverse

Proof state:
case intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
N : M₂ ≃L[R] M₃
⊢ ((↑N).comp f).inverse = f.inverse.comp (↑N).inverse

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
⊢ (g.comp f).inverse = f.inverse.comp g.inverse

Tactic:
rcases hg with ⟨N, rfl⟩

Result:
case intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
N : M₂ ≃L[R] M₃
⊢ ((↑N).comp f).inverse = f.inverse.comp (↑N).inverse
-- Mathlib/RingTheory/Frobenius.lean
lemma restrict_injective [Q.IsPrime] :
    Function.Injective H.restrict

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Function.Injective ⇑H.restrict

Tactic:
rw [injective_iff_map_eq_zero]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ ∀ (a : S ⧸ Q), H.restrict a = 0 → a = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ ∀ (a : S ⧸ Q), H.restrict a = 0 → a = 0

Tactic:
intro x hx

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
x : S ⧸ Q
hx : H.restrict x = 0
⊢ x = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
x : S ⧸ Q
hx : H.restrict x = 0
⊢ x = 0

Tactic:
simpa [restrict_apply, H.card_pos.ne'] using hx

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem isCaratheodory_compl : IsCaratheodory m s₁ → IsCaratheodory m s₁ᶜ

Proof state:
α : Type u
m : OuterMeasure α
s₁ : Set α
⊢ m.IsCaratheodory s₁ → m.IsCaratheodory s₁ᶜ

Tactic:
simp [IsCaratheodory, diff_eq, add_comm]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma iSup_basicOpen_eq_top_iff {ι : Type*} {f : ι → R} :
    (⨆ i : ι, PrimeSpectrum.basicOpen (f i)) = ⊤ ↔ Ideal.span (Set.range f) = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ (zeroLocus (⋃ i, {f i}))ᶜ = Set.univ ↔ Ideal.span (Set.range f) = ⊤

Tactic:
rw [← PrimeSpectrum.zeroLocus_empty_iff_eq_top, compl_involutive.eq_iff]

Result:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ zeroLocus (⋃ i, {f i}) = Set.univᶜ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ ⨆ i, basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤

Tactic:
rw [SetLike.ext'_iff, Opens.coe_iSup]

Result:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ ⋃ i, ↑(basicOpen (f i)) = ↑⊤ ↔ Ideal.span (Set.range f) = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ ⋃ i, ↑(basicOpen (f i)) = ↑⊤ ↔ Ideal.span (Set.range f) = ⊤

Tactic:
simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Opens.coe_top, ← Set.compl_iInter,
  ← PrimeSpectrum.zeroLocus_iUnion]

Result:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ (zeroLocus (⋃ i, {f i}))ᶜ = Set.univ ↔ Ideal.span (Set.range f) = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_1
f : ι → R
⊢ zeroLocus (⋃ i, {f i}) = Set.univᶜ ↔ zeroLocus ↑(Ideal.span (Set.range f)) = ∅

Tactic:
simp only [Set.iUnion_singleton_eq_range,  Set.compl_univ, PrimeSpectrum.zeroLocus_span]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w

Proof state:
w : Nat
x : BitVec w
⊢ -x = ~~~x + 1#w

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
⊢ (-x).toNat = (~~~x + 1#w).toNat

Proof state:
case a
w : Nat
x : BitVec w
⊢ (-x).toNat = (~~~x + 1#w).toNat

Tactic:
simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]

Result:
case a
w : Nat
x : BitVec w
⊢ (2 ^ w - x.toNat) % 2 ^ w = (2 ^ w - 1 - x.toNat + 1) % 2 ^ w

Proof state:
case a
w : Nat
x : BitVec w
⊢ (2 ^ w - x.toNat) % 2 ^ w = (2 ^ w - 1 - x.toNat + 1) % 2 ^ w

Tactic:
congr

Result:
case a.e_a
w : Nat
x : BitVec w
⊢ 2 ^ w - x.toNat = 2 ^ w - 1 - x.toNat + 1

Proof state:
w : Nat
x : BitVec w
hx : x.toNat < 2 ^ w
⊢ 1 ≤ 2 ^ w - x.toNat

Tactic:
omega

Result:
no goals

Proof state:
case a.e_a
w : Nat
x : BitVec w
⊢ 2 ^ w - x.toNat = 2 ^ w - 1 - x.toNat + 1

Tactic:
have hx : x.toNat < 2^w := x.isLt

Result:
case a.e_a
w : Nat
x : BitVec w
hx : x.toNat < 2 ^ w
⊢ 2 ^ w - x.toNat = 2 ^ w - 1 - x.toNat + 1

Proof state:
case a.e_a
w : Nat
x : BitVec w
hx : x.toNat < 2 ^ w
⊢ 2 ^ w - x.toNat = 2 ^ w - 1 - x.toNat + 1

Tactic:
rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, ← Nat.sub_sub, Nat.sub_add_cancel (by omega)]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem linearProjOfIsCompl_of_proj (f : E →ₗ[R] p) (hf : ∀ x : p, f x = x) :
    p.linearProjOfIsCompl (ker f) (isCompl_of_proj hf) = f

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ p.linearProjOfIsCompl (ker f) ⋯ = f

Tactic:
ext x

Result:
case h.a
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ ↑((p.linearProjOfIsCompl (ker f) ⋯) x) = ↑(f x)

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ x ∈ p ⊔ ker f

Tactic:
simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]

Result:
no goals

Proof state:
case h.a
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ ↑((p.linearProjOfIsCompl (ker f) ⋯) x) = ↑(f x)

Tactic:
have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]

Result:
case h.a
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
this : x ∈ p ⊔ ker f
⊢ ↑((p.linearProjOfIsCompl (ker f) ⋯) x) = ↑(f x)

Proof state:
case h.a
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
this : x ∈ p ⊔ ker f
⊢ ↑((p.linearProjOfIsCompl (ker f) ⋯) x) = ↑(f x)

Tactic:
rcases mem_sup'.1 this with ⟨x, y, rfl⟩

Result:
case h.a.intro.intro
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : ↥p
y : ↥(ker f)
this : ↑x + ↑y ∈ p ⊔ ker f
⊢ ↑((p.linearProjOfIsCompl (ker f) ⋯) (↑x + ↑y)) = ↑(f (↑x + ↑y))

Proof state:
case h.a.intro.intro
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : ↥p
y : ↥(ker f)
this : ↑x + ↑y ∈ p ⊔ ker f
⊢ ↑((p.linearProjOfIsCompl (ker f) ⋯) (↑x + ↑y)) = ↑(f (↑x + ↑y))

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_eq_sInf (ω : Ω) : hitting u s ⊥ ⊤ ω = sInf {i : ι | u i ω ∈ s}

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ sInf {i | u i ω ∈ s} = ⊤

Tactic:
rw [sInf_eq_top]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ∀ a ∈ {i | u i ω ∈ s}, a = ⊤

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ∀ a ∈ {i | u i ω ∈ s}, a = ⊤

Tactic:
simp only [Set.mem_univ, true_and] at h_nmem_s

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), u x ω ∉ s
⊢ ∀ a ∈ {i | u i ω ∈ s}, a = ⊤

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), u x ω ∉ s
⊢ ∀ a ∈ {i | u i ω ∈ s}, a = ⊤

Tactic:
exact fun i hi_mem_s => absurd hi_mem_s (h_nmem_s i)

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ⊤ = sInf {i | u i ω ∈ s}

Tactic:
symm

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ sInf {i | u i ω ∈ s} = ⊤

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
⊢ (∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)) → ⊤ = sInf {i | u i ω ∈ s}

Tactic:
intro h_nmem_s

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ⊤ = sInf {i | u i ω ∈ s}

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
⊢ hitting u s ⊥ ⊤ ω = sInf {i | u i ω ∈ s}

Tactic:
simp only [hitting, Set.mem_Icc, bot_le, le_top, and_self_iff, exists_true_left, Set.Icc_bot,
  Set.Iic_top, Set.univ_inter, ite_eq_left_iff, not_exists]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
⊢ (∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)) → ⊤ = sInf {i | u i ω ∈ s}
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_sum {ι : Type*} (f : ι → R → R) (a : A) (s : Finset ι)
    (hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
⊢ cfc (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (f i) a

Tactic:
have hf' : ContinuousOn (∑ i : s, f i) (spectrum R a) := by
  rw [sum_coe_sort s, hsum]
  exact continuousOn_finset_sum s fun i hi => hf i hi

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝
ha : p a
hsum : s.sum f = fun z => ∑ i ∈ s, f i z
hf' : ContinuousOn (∑ i : { x // x ∈ s }, f ↑i) (spectrum R a)
⊢ cfc (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (f i) a