harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_eq_iff_det_pos (e₁ e₂ : Basis ι R M) :
    e₁.orientation = e₂.orientation ↔ 0 < e₁.det e₂ :=
  calc
    e₁.orientation = e₂.orientation ↔ SameRay R e₁.det e₂.det := ray_eq_iff _ _
    _ ↔ SameRay R (e₁.det e₂ • e₂.det) e₂.det

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e₁ e₂ : Basis ι R M
⊢ SameRay R e₁.det e₂.det ↔ SameRay R (e₁.det ⇑e₂ • e₂.det) e₂.det

Tactic:
rw [← e₁.det.eq_smul_basis_det e₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
⊢ (#[a] == #[b]) = true → (a == b) = true

Tactic:
intro h

Result:
α : Type u_1
inst✝ : BEq α
a b : α
h : (#[a] == #[b]) = true
⊢ (a == b) = true

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
h : (#[a] == #[b]) = true
⊢ (a == b) = true

Tactic:
have : isEqv #[a] #[b] BEq.beq = true := h

Result:
α : Type u_1
inst✝ : BEq α
a b : α
h : (#[a] == #[b]) = true
this : #[a].isEqv #[b] BEq.beq = true
⊢ (a == b) = true

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
h : (#[a] == #[b]) = true
this : (a == b) = true
⊢ (a == b) = true

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
h : (#[a] == #[b]) = true
this : #[a].isEqv #[b] BEq.beq = true
⊢ (a == b) = true

Tactic:
simp [isEqv, isEqvAux] at this

Result:
α : Type u_1
inst✝ : BEq α
a b : α
h : (#[a] == #[b]) = true
this : (a == b) = true
⊢ (a == b) = true
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sup_le {a b c : CauSeq α abs} (ha : a ≤ c) (hb : b ≤ c) : a ⊔ b ≤ c

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≤ c

Tactic:
refine le_of_le_of_eq (Or.inr ?_) hb

Result:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≈ b

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c

Tactic:
obtain hb | hb := hb

Result:
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b ≤ c

case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b ≈ c
⊢ a ⊔ b ≤ c

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
obtain ha | ha := ha

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a < c
⊢ a ⊔ b ≤ c

case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c

Proof state:
case inl.inl
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b < c
⊢ a ⊔ b ≤ c

Tactic:
exact Or.inl (CauSeq.sup_lt ha hb)

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≤ c
ha : a ≈ c
⊢ a ⊔ b ≤ c

Tactic:
replace hb := le_of_le_of_eq hb (Setoid.symm ha)

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≤ c

Tactic:
refine le_of_le_of_eq (Or.inr ?_) ha

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≈ a

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a < c
hb : b ≈ c
⊢ a ⊔ b ≤ c

Tactic:
replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)

Result:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≤ c

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : b ≈ c
ha : a ≤ b
⊢ a ⊔ b ≈ b

Tactic:
exact CauSeq.sup_eq_right ha

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
ha : a ≈ c
hb : b ≤ a
⊢ a ⊔ b ≈ a

Tactic:
exact CauSeq.sup_eq_left hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
    l₁.findIdx p ≤ l₂.findIdx p

Proof state:
case intro.isFalse
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
h✝ : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p l₁ ≤ findIdx p t + l₁.length

Tactic:
simp_all [findIdx_eq_length_of_false]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ findIdx p l₁ ≤ findIdx p l₂

Tactic:
obtain ⟨t, rfl⟩ := h

Result:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
⊢ findIdx p l₁ ≤ findIdx p (l₁ ++ t)

Proof state:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
⊢ findIdx p l₁ ≤ findIdx p (l₁ ++ t)

Tactic:
simp only [findIdx_append, findIdx_lt_length]

Result:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
⊢ findIdx p l₁ ≤ if ∃ x, x ∈ l₁ ∧ p x = true then findIdx p l₁ else findIdx p t + l₁.length

Proof state:
case intro.isTrue
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
h✝ : ∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p l₁ ≤ findIdx p l₁

Tactic:
exact Nat.le_refl ..

Result:
no goals

Proof state:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
⊢ findIdx p l₁ ≤ if ∃ x, x ∈ l₁ ∧ p x = true then findIdx p l₁ else findIdx p t + l₁.length

Tactic:
split

Result:
case intro.isTrue
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
h✝ : ∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p l₁ ≤ findIdx p l₁

case intro.isFalse
α : Type u_1
l₁ : List α
p : α → Bool
t : List α
h✝ : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p l₁ ≤ findIdx p t + l₁.length

Proof state:
α : Type u_1
l₁ l₂ : List α
p : α → Bool
h : l₁ <+: l₂
⊢ findIdx p l₁ ≤ findIdx p l₂

Tactic:
rw [IsPrefix] at h

Result:
α : Type u_1
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ findIdx p l₁ ≤ findIdx p l₂
-- Mathlib/AlgebraicGeometry/PointsPi.lean
lemma eq_bot_of_comp_quotientMk_eq_sigmaSpec (I : Ideal (Π i, R i))
    (f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (.of ((Π i, R i) ⧸ I)))
    (hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R) :
    I = ⊥

Proof state:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i => Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
⊢ I = ⊥

Tactic:
refine le_bot_iff.mp fun x hx ↦ ?_

Result:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i => Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
⊢ x ∈ ⊥

Proof state:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i => Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
⊢ x ∈ ⊥

Tactic:
ext i

Result:
case h
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i => Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
i : ι
⊢ x i = 0 i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_inj : map f = map g ↔ f = g

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ map f = map g → f = g

Tactic:
intro h

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
⊢ f = g

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : f = g
⊢ map f = map g

Tactic:
subst h

Result:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f = map f

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ f = g → map f = map g

Tactic:
intro h

Result:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : f = g
⊢ map f = map g

Proof state:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
a : α✝¹
⊢ f a = g a

Tactic:
replace h := congrFun h #[a]

Result:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
a : α✝¹
h : map f #[a] = map g #[a]
⊢ f a = g a

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f = map f

Tactic:
rfl

Result:
no goals

Proof state:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
a : α✝¹
h : map f #[a] = map g #[a]
⊢ f a = g a

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
⊢ f = g

Tactic:
ext a

Result:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
a : α✝¹
⊢ f a = g a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ map f = map g ↔ f = g

Tactic:
constructor

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ map f = map g → f = g

case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ f = g → map f = map g
-- Mathlib/RingTheory/DualNumber.lean
lemma isNilpotent_iff_eps_dvd [DivisionSemiring R] {x : R[ε]} :
    IsNilpotent x ↔ ε ∣ x

Proof state:
R : Type u_1
inst✝ : DivisionSemiring R
x : R[ε]
⊢ IsNilpotent x ↔ ε ∣ x

Tactic:
simp only [isNilpotent_iff_isNilpotent_fst, isNilpotent_iff_eq_zero, fst_eq_zero_iff_eps_dvd]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem union_ae_eq_right_of_ae_eq_empty (h : s =ᵐ[μ] (∅ : Set α)) : (s ∪ t : Set α) =ᵐ[μ] t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ s ∪ t =ᶠ[ae μ] t

Tactic:
convert ae_eq_set_union h (ae_eq_refl t)

Result:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ t = ∅ ∪ t

Proof state:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] ∅
⊢ t = ∅ ∪ t

Tactic:
rw [empty_union]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_tail (l : List α) (h : l.tail ≠ []) :
    (tail l).getLast h = l.getLast (ne_nil_of_tail_ne_nil h)

Proof state:
case e_i
α : Type u_1
l : List α
h : l.tail ≠ []
⊢ l.length - 1 - 1 + 1 = l.length - 1

Tactic:
match l with
| _ :: _ :: l => simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l.tail ≠ []
⊢ l.tail.getLast h = l.getLast ⋯

Tactic:
simp only [getLast_eq_getElem, length_tail, getElem_tail]

Result:
α : Type u_1
l : List α
h : l.tail ≠ []
⊢ l[l.length - 1 - 1 + 1] = l[l.length - 1]

Proof state:
α : Type u_1
l✝ : List α
head✝¹ head✝ : α
l : List α
h : (head✝¹ :: head✝ :: l).tail ≠ []
⊢ (head✝¹ :: head✝ :: l).length - 1 - 1 + 1 = (head✝¹ :: head✝ :: l).length - 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l.tail ≠ []
⊢ l[l.length - 1 - 1 + 1] = l[l.length - 1]

Tactic:
congr

Result:
case e_i
α : Type u_1
l : List α
h : l.tail ≠ []
⊢ l.length - 1 - 1 + 1 = l.length - 1
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem iterate_toEnd_mem_lowerCentralSeries (x : L) (m : M) (k : ℕ) :
    (toEnd R L M x)^[k] m ∈ lowerCentralSeries R L M k

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
m : M
⊢ (⇑((toEnd R L M) x))^[0] m ∈ lowerCentralSeries R L M 0

Tactic:
simp only [Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
m : M
k : ℕ
⊢ (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k

Tactic:
induction k with
| zero => simp only [Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]
| succ k ih =>
  simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ',
    toEnd_apply_apply]
  exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k
⊢ ⁅x, (⇑((toEnd R L M) x))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M k⁆

Tactic:
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k
⊢ (⇑((toEnd R L M) x))^[k + 1] m ∈ lowerCentralSeries R L M (k + 1)

Tactic:
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ',
  toEnd_apply_apply]

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k
⊢ ⁅x, (⇑((toEnd R L M) x))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M k⁆
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
theorem IsSelfAdjoint.mem_spectrum_eq_re {a : A} (ha : IsSelfAdjoint a) {z : ℂ}
    (hz : z ∈ spectrum ℂ a) : z = z.re

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : NormedSpace.exp ℂ (I • z) ∈ σ ℂ (NormedSpace.exp ℂ (I • a))
⊢ z = ↑z.re

Tactic:
exact Complex.ext (ofReal_re _) <| by
  simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_exp, Real.exp_eq_one_iff,
    smul_eq_mul, I_mul, neg_eq_zero] using
    spectrum.subset_circle_of_unitary hu this

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
⊢ z = ↑z.re

Tactic:
let Iu := Units.mk0 I I_ne_zero

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ z = ↑z.re

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ NormedSpace.exp ℂ (I • z) ∈ σ ℂ (NormedSpace.exp ℂ (I • a))

Tactic:
simpa only [Units.smul_def, Units.val_mk0] using
  spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ z = ↑z.re

Tactic:
have hu := exp_mem_unitary_of_mem_skewAdjoint ℂ (ha.smul_mem_skewAdjoint conj_I)

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
⊢ z = ↑z.re

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : NormedSpace.exp ℂ (I • z) ∈ σ ℂ (NormedSpace.exp ℂ (I • a))
⊢ z.im = (↑z.re).im

Tactic:
simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_exp, Real.exp_eq_one_iff,
  smul_eq_mul, I_mul, neg_eq_zero] using
  spectrum.subset_circle_of_unitary hu this

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ z = ↑z.re

Tactic:
have : NormedSpace.exp ℂ (I • z) ∈ spectrum ℂ (NormedSpace.exp ℂ (I • a)) := by
  simpa only [Units.smul_def, Units.val_mk0] using
    spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
hu : NormedSpace.exp ℂ (I • a) ∈ unitary A
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : NormedSpace.exp ℂ (I • z) ∈ σ ℂ (NormedSpace.exp ℂ (I • a))
⊢ z = ↑z.re
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMin.hasDerivAt_eq_zero (h : IsLocalMin f a) (hf : HasDerivAt f f' a) : f' = 0

Proof state:
f : ℝ → ℝ
f' a : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ f' = 0

Tactic:
simpa using DFunLike.congr_fun (h.hasFDerivAt_eq_zero (hasDerivAt_iff_hasFDerivAt.1 hf)) 1

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
theorem LinearMap.comp_id_moduleCat
    {R} [Ring R] {G : ModuleCat.{u} R} {H : Type u} [AddCommGroup H] [Module R H] (f : G →ₗ[R] H) :
    f.comp (𝟙 G : G ⟶ G).hom = f

Proof state:
R : Type u_1
inst✝² : Ring R
G : ModuleCat R
H : Type u
inst✝¹ : AddCommGroup H
inst✝ : Module R H
f : ↑G →ₗ[R] H
⊢ f ∘ₗ Hom.hom (𝟙 G) = f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_add : (p + q).eval₂ f x = p.eval₂ f x + q.eval₂ f x

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ((p + q).sum fun e a => f a * x ^ e) = (p.sum fun e a => f a * x ^ e) + q.sum fun e a => f a * x ^ e

Tactic:
apply sum_add_index <;> simp [add_mul]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q

Tactic:
simp only [eval₂_eq_sum]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ((p + q).sum fun e a => f a * x ^ e) = (p.sum fun e a => f a * x ^ e) + q.sum fun e a => f a * x ^ e
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma pow_eq_zero : ∀ {n}, a ^ n = 0 → a = 0
  | 0, ha => by simpa using congr_arg (a * ·) ha
  | n + 1, ha => by rw [pow_succ, mul_eq_zero] at ha; exact ha.elim pow_eq_zero id

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
a : M₀
inst✝ : NoZeroDivisors M₀
n : ℕ
ha : a ^ (n + 1) = 0
⊢ a = 0

Tactic:
rw [pow_succ, mul_eq_zero] at ha

Result:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
a : M₀
inst✝ : NoZeroDivisors M₀
n : ℕ
ha : a ^ n = 0 ∨ a = 0
⊢ a = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
a : M₀
inst✝ : NoZeroDivisors M₀
n : ℕ
ha : a ^ n = 0 ∨ a = 0
⊢ a = 0

Tactic:
exact ha.elim pow_eq_zero id

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma max_mul_mul_le_max_mul_max [PosMulMono α] [MulPosMono α] (b c : α) (ha : 0 ≤ a) (hd : 0 ≤ d) :
    max (a * b) (d * c) ≤ max a c * max d b :=
  have ba : b * a ≤ max d b * max c a :=
    mul_le_mul (le_max_right d b) (le_max_right c a) ha (le_trans hd (le_max_left d b))
  have cd : c * d ≤ max a c * max b d :=
    mul_le_mul (le_max_right a c) (le_max_right b d) hd (le_trans ha (le_max_left a c))
  max_le (by simpa [mul_comm, max_comm] using ba) (by simpa [mul_comm, max_comm] using cd)

Proof state:
α : Type u
inst✝³ : CommSemiring α
inst✝² : LinearOrder α
a d : α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
b c : α
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ (d ⊔ b) * (c ⊔ a)
cd : c * d ≤ (a ⊔ c) * (b ⊔ d)
⊢ d * c ≤ (a ⊔ c) * (d ⊔ b)

Tactic:
simpa [mul_comm, max_comm] using cd

Result:
no goals

Proof state:
α : Type u
inst✝³ : CommSemiring α
inst✝² : LinearOrder α
a d : α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
b c : α
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ (d ⊔ b) * (c ⊔ a)
cd : c * d ≤ (a ⊔ c) * (b ⊔ d)
⊢ a * b ≤ (a ⊔ c) * (d ⊔ b)

Tactic:
simpa [mul_comm, max_comm] using ba

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Support.lean
theorem support_deriv_subset : support (deriv f) ⊆ tsupport f

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∉ tsupport f → x ∉ support (deriv f)

Tactic:
intro h2x

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h2x : x ∉ tsupport f
⊢ x ∉ support (deriv f)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ support (deriv f) ⊆ tsupport f

Tactic:
intro x

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∈ support (deriv f) → x ∈ tsupport f

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∈ support (deriv f) → x ∈ tsupport f

Tactic:
rw [← not_imp_not]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∉ tsupport f → x ∉ support (deriv f)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h2x : f =ᶠ[nhds x] 0
⊢ x ∉ support (deriv f)

Tactic:
exact nmem_support.mpr (h2x.deriv_eq.trans (deriv_const x 0))

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h2x : x ∉ tsupport f
⊢ x ∉ support (deriv f)

Tactic:
rw [not_mem_tsupport_iff_eventuallyEq] at h2x

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h2x : f =ᶠ[nhds x] 0
⊢ x ∉ support (deriv f)
-- Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
theorem orbit_fixingSubgroup_compl_subset {s : Set α} {a : α} (a_in_s : a ∈ s) :
    MulAction.orbit (fixingSubgroup M sᶜ) a ⊆ s

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
⊢ orbit (↥(fixingSubgroup M sᶜ)) a ⊆ s

Tactic:
intro b b_in_orbit

Result:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
⊢ b ∈ s

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : ⟨g, g_fixing⟩ • a = b
⊢ b ∈ s

Tactic:
rw [Submonoid.mk_smul] at g_eq

Result:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : g • a = b
⊢ b ∈ s

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
⊢ b ∈ s

Tactic:
let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit

Result:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : ⟨g, g_fixing⟩ • a = b
⊢ b ∈ s

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : g • a = b
⊢ b ∈ s

Tactic:
rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing

Result:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
⊢ b ∈ s

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
⊢ b ∈ s

Tactic:
rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]

Result:
no goals