harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
@[reassoc (attr := simp)]
lemma map_ofInv_hom_id (s : Y ⟶ X) (hs : W s) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    (ofInv s hs).map L hL ≫ L.map s = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ (ofInv s hs).map L hL ≫ L.map s = 𝟙 (L.obj X)

Tactic:
simp [map]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (ofInv s hs).map L hL ≫ L.map s = 𝟙 (L.obj X)

Tactic:
letI := hL _ hs

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ (ofInv s hs).map L hL ≫ L.map s = 𝟙 (L.obj X)
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isSuccPrelimit_iff : ¬ IsSuccPrelimit a ↔ ∃ b, ¬ IsMax b ∧ succ b = a

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ ¬IsMax b ∧ succ b = a → b ⋖ a

Tactic:
rintro ⟨h, rfl⟩

Result:
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
h : ¬IsMax b
⊢ b ⋖ succ b

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
⊢ ¬IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a

Tactic:
rw [not_isSuccPrelimit_iff_exists_covBy]

Result:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
⊢ (∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a

Proof state:
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
h : ¬IsMax b
⊢ b ⋖ succ b

Tactic:
exact covBy_succ_of_not_isMax h

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
⊢ (∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a

Tactic:
refine exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (CovBy.succ_eq hba)⟩, ?_⟩

Result:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ ¬IsMax b ∧ succ b = a → b ⋖ a
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem IsNormal.fp_iff_deriv (H : IsNormal f) {a} : f a = a ↔ ∃ o, deriv f o = a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a = a ↔ ∃ o, deriv f o = a

Tactic:
rw [← H.le_iff_eq, H.le_iff_deriv]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a.lcm b).factorization = a.factorization ⊔ b.factorization

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization

Tactic:
ext1

Result:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ (a.factorization + b.factorization) a✝ = (a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization) a✝

Proof state:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ (a.factorization + b.factorization) a✝ = (a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization) a✝

Tactic:
exact (min_add_max _ _).symm

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.lcm b).factorization = a.factorization ⊔ b.factorization

Tactic:
rw [← add_right_inj (a.gcd b).factorization, ←
  factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
  factorization_gcd ha hb, factorization_mul ha hb]

Result:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem restrict_dirac [MeasurableSingletonClass α] [Decidable (a ∈ s)] :
    (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ (dirac a).restrict s = if a ∈ s then dirac a else 0

Tactic:
split_ifs with has

Result:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a

case neg
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Proof state:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a

Tactic:
apply restrict_eq_self_of_ae_mem

Result:
case pos.hs
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s

Proof state:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Tactic:
rw [restrict_eq_zero, dirac_apply, indicator_of_not_mem has]

Result:
no goals

Proof state:
case pos.hs
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ ∀ᵐ (x : α) ∂dirac a, x ∈ s

Tactic:
rwa [ae_dirac_eq]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem sqrt : @Primrec' 1 fun v => v.head.sqrt

Proof state:
case neg
n : ℕ
IH : Nat.rec 0 (fun x y => if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
h : ¬n + 1 < (n.sqrt + 1) * (n.sqrt + 1)
⊢ n.sqrt + 1 = (n + 1).sqrt

Tactic:
exact
  Nat.eq_sqrt.2 ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩

Result:
no goals
-- Mathlib/Data/Fintype/Fin.lean
theorem Ioi_succ (i : Fin n) : Ioi i.succ = (Ioi i).map (Fin.succEmb _)

Proof state:
case h.mpr
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ (∃ a, i✝ < a ∧ (succEmb n) a = i) → i✝.succ < i

Tactic:
rintro ⟨i, hi, rfl⟩

Result:
case h.mpr.intro.intro
n : ℕ
i✝ i : Fin n
hi : i✝ < i
⊢ i✝.succ < (succEmb n) i

Proof state:
case h
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i✝.succ < i ↔ ∃ a, i✝ < a ∧ (succEmb n) a = i

Tactic:
constructor

Result:
case h.mp
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i✝.succ < i → ∃ a, i✝ < a ∧ (succEmb n) a = i

case h.mpr
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ (∃ a, i✝ < a ∧ (succEmb n) a = i) → i✝.succ < i

Proof state:
n : ℕ
i : Fin n
⊢ Ioi i.succ = map (succEmb n) (Ioi i)

Tactic:
ext i

Result:
case h
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i ∈ Ioi i✝.succ ↔ i ∈ map (succEmb n) (Ioi i✝)

Proof state:
case h.mp
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i✝.succ < i → ∃ a, i✝ < a ∧ (succEmb n) a = i

Tactic:
refine cases ?_ ?_ i

Result:
case h.mp.refine_1
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i✝.succ < 0 → ∃ a, i✝ < a ∧ (succEmb n) a = 0

case h.mp.refine_2
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ ∀ (i : Fin n), i✝.succ < i.succ → ∃ a, i✝ < a ∧ (succEmb n) a = i.succ

Proof state:
case h.mp.refine_2
n : ℕ
i✝¹ : Fin n
i✝ : Fin (n + 1)
i : Fin n
hi : i✝¹.succ < i.succ
⊢ ∃ a, i✝¹ < a ∧ (succEmb n) a = i.succ

Tactic:
exact ⟨i, succ_lt_succ_iff.mp hi, rfl⟩

Result:
no goals

Proof state:
case h.mpr.intro.intro
n : ℕ
i✝ i : Fin n
hi : i✝ < i
⊢ i✝.succ < (succEmb n) i

Tactic:
simpa

Result:
no goals

Proof state:
case h.mp.refine_1
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i✝.succ < 0 → ∃ a, i✝ < a ∧ (succEmb n) a = 0

Tactic:
rintro ⟨⟨⟩⟩

Result:
no goals

Proof state:
case h.mp.refine_2
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ ∀ (i : Fin n), i✝.succ < i.succ → ∃ a, i✝ < a ∧ (succEmb n) a = i.succ

Tactic:
intro i hi

Result:
case h.mp.refine_2
n : ℕ
i✝¹ : Fin n
i✝ : Fin (n + 1)
i : Fin n
hi : i✝¹.succ < i.succ
⊢ ∃ a, i✝¹ < a ∧ (succEmb n) a = i.succ

Proof state:
case h
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i ∈ Ioi i✝.succ ↔ i ∈ map (succEmb n) (Ioi i✝)

Tactic:
simp only [mem_filter, mem_Ioi, mem_map, mem_univ, Function.Embedding.coeFn_mk, exists_true_left]

Result:
case h
n : ℕ
i✝ : Fin n
i : Fin (n + 1)
⊢ i✝.succ < i ↔ ∃ a, i✝ < a ∧ (succEmb n) a = i
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem exists_sSupIndep_isCompl_sSup_atoms (h : sSup { a : α | IsAtom a } = ⊤) (b : α) :
    ∃ s : Set α, sSupIndep s ∧
    IsCompl b (sSup s) ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a

Proof state:
case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x

Tactic:
exact ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) (l : List α) :
    (l.modifyTailIdx f n).modifyTailIdx g n = l.modifyTailIdx (g ∘ f) n

Proof state:
α : Type u_1
f g : List α → List α
n : Nat
l : List α
⊢ modifyTailIdx (fun l => modifyTailIdx g 0 (f l)) n l = modifyTailIdx (g ∘ f) n l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
f g : List α → List α
n : Nat
l : List α
⊢ modifyTailIdx g n (modifyTailIdx f n l) = modifyTailIdx (g ∘ f) n l

Tactic:
rw [modifyTailIdx_modifyTailIdx_le n n l (Nat.le_refl n), Nat.sub_self]

Result:
α : Type u_1
f g : List α → List α
n : Nat
l : List α
⊢ modifyTailIdx (fun l => modifyTailIdx g 0 (f l)) n l = modifyTailIdx (g ∘ f) n l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_concat_false : concat 0#w false = 0#(w + 1)

Proof state:
w : Nat
⊢ (0#w).concat false = 0#(w + 1)

Tactic:
ext

Result:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ ((0#w).concat false).getLsbD i✝ = (0#(w + 1)).getLsbD i✝

Proof state:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ ((0#w).concat false).getLsbD i✝ = (0#(w + 1)).getLsbD i✝

Tactic:
simp [getLsbD_concat]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_le_iff_le_sin' {x y : ℝ} (hy : y ∈ Ico (-(π / 2)) (π / 2)) :
    arcsin x ≤ y ↔ x ≤ sin y

Proof state:
case inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : x ≤ -1
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
simp [arcsin_of_le_neg_one hx₁, hy.1, hx₁.trans (neg_one_le_sin _)]

Result:
no goals

Proof state:
case inr.inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
simp [arcsin_of_one_le hx₂.le, hy.2.not_le, (sin_le_one y).trans_lt hx₂]

Result:
no goals

Proof state:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
rcases le_total x (-1) with hx₁ | hx₁

Result:
case inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : x ≤ -1
⊢ arcsin x ≤ y ↔ x ≤ sin y

case inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
⊢ arcsin x ≤ y ↔ x ≤ sin y

Proof state:
case inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
rcases lt_or_le 1 x with hx₂ | hx₂

Result:
case inr.inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ arcsin x ≤ y ↔ x ≤ sin y

case inr.inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin x ≤ y ↔ x ≤ sin y

Proof state:
case inr.inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
exact arcsin_le_iff_le_sin ⟨hx₁, hx₂⟩ (mem_Icc_of_Ico hy)

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma SMulPosReflectLT.lift [SMulPosReflectLT α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b)
    (zero : f 0 = 0) : SMulPosReflectLT α β where
  elim b hb a₁ a₂ h

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLT α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
zero : True
hb : 0 ≤ f b
h : a₁ • f b < a₂ • f b
⊢ a₁ < a₂

Tactic:
exact lt_of_smul_lt_smul_right h hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ < a₂

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLT α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
zero : True
hb : 0 ≤ f b
h : a₁ • f b < a₂ • f b
⊢ a₁ < a₂
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem aecover_restrict_of_ae_imp {s : Set α} {φ : ι → Set α} (hs : MeasurableSet s)
    (ae_eventually_mem : ∀ᵐ x ∂μ, x ∈ s → ∀ᶠ n in l, x ∈ φ n)
    (measurable : ∀ n, MeasurableSet <| φ n) : AECover (μ.restrict s) l φ where
  ae_eventually_mem

Proof state:
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
s : Set α
φ : ι → Set α
hs : MeasurableSet s
ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n
measurable : ∀ (n : ι), MeasurableSet (φ n)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ∀ᶠ (i : ι) in l, x ∈ φ i

Tactic:
rwa [ae_restrict_iff' hs]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem invariant_orthogonalComplement_eigenspace (hT : T.IsSymmetric) (μ : 𝕜)
    (v : E) (hv : v ∈ (eigenspace T μ)ᗮ) : T v ∈ (eigenspace T μ)ᗮ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
⊢ T v ∈ (eigenspace T μ)ᗮ

Tactic:
intro w hw

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ inner w (T v) = 0

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ T w = μ • w

Tactic:
rwa [mem_eigenspace_iff] at hw

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
this : T w = μ • w
⊢ inner w (T v) = 0

Tactic:
simp [← hT w, this, inner_smul_left, hv w hw]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ inner w (T v) = 0

Tactic:
have : T w = (μ : 𝕜) • w := by rwa [mem_eigenspace_iff] at hw

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
this : T w = μ • w
⊢ inner w (T v) = 0
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_map_dvd {H : Type*} [Monoid H] (ψ : G →* H) (x : G) :
    orderOf (ψ x) ∣ orderOf x

Proof state:
case h
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ x ^ orderOf x = 1

Tactic:
rw [← map_pow, pow_orderOf_eq_one]

Result:
case h
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ 1 = 1

Proof state:
case h
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ 1 = 1

Tactic:
apply map_one

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ orderOf (ψ x) ∣ orderOf x

Tactic:
apply orderOf_dvd_of_pow_eq_one

Result:
case h
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ x ^ orderOf x = 1
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
lemma iteratedDeriv_comp_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) :
    iteratedDeriv n (fun x ↦ f (-x)) a = (-1 : 𝕜) ^ n • iteratedDeriv n f (-a)

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ iteratedDeriv 0 (fun x => f (-x)) a = (-1) ^ 0 • iteratedDeriv 0 f (-a)

Tactic:
simp only [iteratedDeriv_zero, pow_zero, one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
a : 𝕜
⊢ iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)

Tactic:
induction' n with n ih generalizing a

Result:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ iteratedDeriv 0 (fun x => f (-x)) a = (-1) ^ 0 • iteratedDeriv 0 f (-a)

case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
ih : ∀ (a : 𝕜), iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)
a : 𝕜
⊢ iteratedDeriv (n + 1) (fun x => f (-x)) a = (-1) ^ (n + 1) • iteratedDeriv (n + 1) f (-a)

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
ih : ∀ (a : 𝕜), iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)
a : 𝕜
ih' : (iteratedDeriv n fun x => f (-x)) = fun x => (-1) ^ n • iteratedDeriv n f (-x)
⊢ iteratedDeriv (n + 1) (fun x => f (-x)) a = (-1) ^ (n + 1) • iteratedDeriv (n + 1) f (-a)

Tactic:
rw [iteratedDeriv_succ, iteratedDeriv_succ, ih', pow_succ', neg_mul, one_mul,
  deriv_comp_neg (f := fun x ↦ (-1 : 𝕜) ^ n • iteratedDeriv n f x), deriv_const_smul',
  neg_smul]

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
ih : ∀ (a : 𝕜), iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)
a : 𝕜
⊢ iteratedDeriv (n + 1) (fun x => f (-x)) a = (-1) ^ (n + 1) • iteratedDeriv (n + 1) f (-a)

Tactic:
have ih' : iteratedDeriv n (fun x ↦ f (-x)) = fun x ↦ (-1 : 𝕜) ^ n • iteratedDeriv n f (-x) :=
  funext ih

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ
ih : ∀ (a : 𝕜), iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)
a : 𝕜
ih' : (iteratedDeriv n fun x => f (-x)) = fun x => (-1) ^ n • iteratedDeriv n f (-x)
⊢ iteratedDeriv (n + 1) (fun x => f (-x)) a = (-1) ^ (n + 1) • iteratedDeriv (n + 1) f (-a)
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem IsHilbertSum.hasSum_linearIsometryEquiv_symm (hV : IsHilbertSum 𝕜 G V)
    (w : lp G 2) : HasSum (fun i => V i (w i)) (hV.linearIsometryEquiv.symm w)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : IsHilbertSum 𝕜 G V
w : ↥(lp G 2)
⊢ HasSum (fun i => (V i) (↑w i)) (hV.linearIsometryEquiv.symm w)

Tactic:
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.hasSum_linearIsometry]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudo_exact_of_exact {S : ShortComplex C} (hS : S.Exact) :
    ∀ b, S.g b = 0 → ∃ a, S.f a = b :=
  fun b' =>
    Quotient.inductionOn b' fun b hb => by
      have hb' : b.hom ≫ S.g = 0 := (pseudoZero_iff _).1 hb
      -- By exactness, `b` factors through `im f = ker g` via some `c`.
      obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' hS.isLimitImage _ hb'
      -- We compute the pullback of the map into the image and `c`.
      -- The pseudoelement induced by the first pullback map will be our preimage.
      use pullback.fst (Abelian.factorThruImage S.f) c
      -- It remains to show that the image of this element under `f` is pseudo-equal to `b`.
      apply Quotient.sound
      refine ⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _,
              pullback.snd _ _, inferInstance, inferInstance, ?_⟩
      -- Now we can verify that the diagram commutes.
      calc
        𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫ pullback.fst _ _ ≫ S.f =
          pullback.fst _ _ ≫ S.f :=
          Category.id_comp _
        _ = pullback.fst _ _ ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Tactic:
congr

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem order_one [MulZeroOneClass R] : order (1 : HahnSeries Γ R) = 0

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
exact order_single one_ne_zero

Result:
no goals

Proof state:
case inl
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Subsingleton R
⊢ order 1 = 0

Tactic:
rw [Subsingleton.elim (1 : HahnSeries Γ R) 0, order_zero]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
⊢ order 1 = 0

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Subsingleton R
⊢ order 1 = 0

case inr
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Nontrivial R
⊢ order 1 = 0
-- Mathlib/Data/Finsupp/Order.lean
theorem support_sup [DecidableEq ι] (f g : ι →₀ α) : (f ⊔ g).support = f.support ∪ g.support

Proof state:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬f a✝ ⊔ g a✝ = ⊥ ↔ ¬f a✝ = ⊥ ∨ ¬g a✝ = ⊥

Tactic:
rw [_root_.sup_eq_bot_iff, not_and_or]

Result:
no goals

Proof state:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support

Tactic:
simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne, ← bot_eq_zero]

Result:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ ¬f a✝ ⊔ g a✝ = ⊥ ↔ ¬f a✝ = ⊥ ∨ ¬g a✝ = ⊥

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
ext

Result:
case h
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support