harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
/-- If elements `p,q` of `FreeAddMonoid (R × Π i, s i)` lift elements `x,y` of `⨂[R] i, s i`
respectively, then `p + q` lifts `x + y`.
-/
lemma lifts_add {x y : ⨂[R] i, s i} {p q : FreeAddMonoid (R × Π i, s i)}
    (hp : p ∈ lifts x) (hq : q ∈ lifts y) : p + q ∈ lifts (x + y)

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts
hq : q ∈ y.lifts
⊢ p + q ∈ (x + y).lifts

Tactic:
simp only [lifts, Set.mem_setOf_eq, AddCon.coe_add]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts
hq : q ∈ y.lifts
⊢ ↑p + ↑q = x + y

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts
hq : q ∈ y.lifts
⊢ ↑p + ↑q = x + y

Tactic:
rw [hp, hq]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_right_anti₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) : Antitone fun n : ℤ ↦ a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
⊢ Antitone fun n => a ^ n

Tactic:
refine antitone_int_of_succ_le fun n ↦ ?_

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ (n + 1) ≤ a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ (n + 1) ≤ a ^ n

Tactic:
rw [zpow_add_one₀ ha₀.ne']

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ n * a ≤ a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ n * a ≤ a ^ n

Tactic:
exact mul_le_of_le_one_right (zpow_nonneg ha₀.le _) ha₁

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_set {l : Array α} {i : Nat} {h : i < l.size} {a : α} :
    (l.set i a).mapIdx f = (l.mapIdx f).set i (f i a) (by simpa)

Proof state:
α : Type ?u.121168
f : Nat → α → ?m.121230
l : Array α
i : Nat
h : i < l.size
a : α
⊢ i < (mapIdx f l).size

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : Array α
i : Nat
h : i < l.size
a : α
⊢ mapIdx f (l.set i a h) = (mapIdx f l).set i (f i a) ⋯

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : List α
h : i < { toList := l }.size
⊢ mapIdx f ({ toList := l }.set i a h) = (mapIdx f { toList := l }).set i (f i a) ⋯

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : List α
h : i < { toList := l }.size
⊢ mapIdx f ({ toList := l }.set i a h) = (mapIdx f { toList := l }).set i (f i a) ⋯

Tactic:
simp [List.mapIdx_set]

Result:
no goals
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem subset_set_biUnion_of_mem {s : Finset α} {f : α → Set β} {x : α} (h : x ∈ s) :
    f x ⊆ ⋃ y ∈ s, f y :=
  show f x ≤ ⨆ y ∈ s, f y from le_iSup_of_le x <| by simp only [h, iSup_pos, le_refl]

Proof state:
α : Type u_2
β : Type u_3
s : Finset α
f : α → Set β
x : α
h : x ∈ s
⊢ f x ≤ ⨆ (_ : x ∈ s), f x

Tactic:
simp only [h, iSup_pos, le_refl]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem add_mul_left_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (y + x * z)

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + x * z) x

Tactic:
exact h.symm.add_mul_left_left z

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)

Tactic:
rw [isCoprime_comm]

Result:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + x * z) x
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightUnshift_smul {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) (x : R) :
    (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
x : R
⊢ (rightShiftLinearEquiv R K L n a n' hn).symm (x • γ) = x • γ.rightUnshift n hn

Tactic:
apply map_smul

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
x : R
⊢ (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

Tactic:
change (rightShiftLinearEquiv  R K L n a n' hn).symm (x • γ) = _

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
x : R
⊢ (rightShiftLinearEquiv R K L n a n' hn).symm (x • γ) = x • γ.rightUnshift n hn
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem _root_.Real.tendsto_toNNReal_atTop_iff {l : Filter α} {f : α → ℝ} :
    Tendsto (fun x ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x => (f x).toNNReal) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← Real.comap_toNNReal_atTop, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem natAbs_det_basis_change {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ S)
    (I : Ideal S) (bI : Basis ι ℤ I) : (b.det ((↑) ∘ bI)).natAbs = Ideal.absNorm I

Proof state:
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis ι ℤ ↥I
e : S ≃ₗ[ℤ] ↥I := b.equiv bI (Equiv.refl ι)
⊢ (b.det (⇑(↑ℤ (Submodule.subtype I)) ∘ ⇑bI)).natAbs = (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ ↑e)).natAbs

Tactic:
rw [Basis.det_comp_basis]

Result:
no goals

Proof state:
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis ι ℤ ↥I
e : S ≃ₗ[ℤ] ↥I := b.equiv bI (Equiv.refl ι)
⊢ (b.det (Subtype.val ∘ ⇑bI)).natAbs = absNorm I

Tactic:
calc
  (b.det ((Submodule.subtype I).restrictScalars ℤ ∘ bI)).natAbs =
      (LinearMap.det ((Submodule.subtype I).restrictScalars ℤ ∘ₗ (e : S →ₗ[ℤ] I))).natAbs := by
    rw [Basis.det_comp_basis]
  _ = _ := natAbs_det_equiv I e

Result:
no goals

Proof state:
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis ι ℤ ↥I
⊢ (b.det (Subtype.val ∘ ⇑bI)).natAbs = absNorm I

Tactic:
let e := b.equiv bI (Equiv.refl _)

Result:
S : Type u_1
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Free ℤ S
inst✝² : Module.Finite ℤ S
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ S
I : Ideal S
bI : Basis ι ℤ ↥I
e : S ≃ₗ[ℤ] ↥I := b.equiv bI (Equiv.refl ι)
⊢ (b.det (Subtype.val ∘ ⇑bI)).natAbs = absNorm I
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsCoprime.prod_left_iff : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x

Tactic:
rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]

Result:
no goals

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
x✝ : I
⊢ x✝ ∈ ∅ → IsCoprime (s x✝) x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x

Tactic:
classical
refine Finset.induction_on t (iff_of_true isCoprime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]

Result:
no goals

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x

Tactic:
refine Finset.induction_on t (iff_of_true isCoprime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_

Result:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
-- Mathlib/LinearAlgebra/Coevaluation.lean
theorem contractLeft_assoc_coevaluation' :
    (contractLeft K V).lTensor _ ∘ₗ
        (TensorProduct.assoc K _ _ _).toLinearMap ∘ₗ (coevaluation K V).rTensor V =
      (TensorProduct.rid K _).symm.toLinearMap ∘ₗ (TensorProduct.lid K _).toLinearMap

Proof state:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((∑ i : ↑(Basis.ofVectorSpaceIndex K V),
            (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i) ⊗ₜ[K]
          (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Tactic:
rw [TensorProduct.sum_tmul, map_sum]

Result:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      (∑ x : ↑(Basis.ofVectorSpaceIndex K V),
        (TensorProduct.assoc K V (Dual K V) V)
          (((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x) ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Proof state:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1 else 0) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Tactic:
simp only [Finset.mem_univ, if_true]

Result:
no goals

Proof state:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) =
    (TensorProduct.rid K V).symm ((TensorProduct.lid K V) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))

Tactic:
rw [lid_tmul, one_smul, rid_symm_apply]

Result:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
-- Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
theorem iSup_eigenspace_inf_eigenspace_of_commute (hB : B.IsSymmetric) (hAB : Commute A B) :
    (⨆ γ, eigenspace A α ⊓ eigenspace B γ) = eigenspace A α

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ γ, eigenspace A α ⊓ eigenspace B γ = eigenspace A α

Tactic:
conv_rhs => rw [← (eigenspace A α).map_subtype_top]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ γ, eigenspace A α ⊓ eigenspace B γ = map (eigenspace A α).subtype ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hB : B.IsSymmetric
hAB : Commute A B
⊢ map (eigenspace A α).subtype (⨆ i, (genEigenspace (B.restrict ⋯) i) 1) = map (eigenspace A α).subtype ⊤

Tactic:
congr 1

Result:
case e_p
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ i, (genEigenspace (B.restrict ⋯) i) 1 = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ γ, eigenspace A α ⊓ eigenspace B γ = map (eigenspace A α).subtype ⊤

Tactic:
simp only [← genEigenspace_eq_eigenspace (f := B), ← Submodule.map_iSup,
  (eigenspace A α).inf_genEigenspace _ (mapsTo_genEigenspace_of_comm hAB α 1)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hB : B.IsSymmetric
hAB : Commute A B
⊢ map (eigenspace A α).subtype (⨆ i, (genEigenspace (B.restrict ⋯) i) 1) = map (eigenspace A α).subtype ⊤

Proof state:
case e_p
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ i, (genEigenspace (B.restrict ⋯) i) 1 = ⊤

Tactic:
simpa only [genEigenspace_eq_eigenspace, Submodule.orthogonal_eq_bot_iff]
  using orthogonalComplement_iSup_eigenspaces_eq_bot <|
    hB.restrict_invariant <| mapsTo_genEigenspace_of_comm hAB α 1

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem norm_mk_lt' (S : AddSubgroup M) (m : M) {ε : ℝ} (hε : 0 < ε) :
    ∃ s ∈ S, ‖m + s‖ < ‖mk' S m‖ + ε

Proof state:
case right
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ ‖m + (-m + n)‖ < ‖(mk' S) m‖ + ε

Tactic:
rwa [add_neg_cancel_left]

Result:
no goals

Proof state:
case intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : (mk' S) n = (mk' S) m
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ ∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε

Tactic:
erw [eq_comm, QuotientAddGroup.eq] at hn

Result:
case intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ ∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
⊢ ∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε

Tactic:
obtain ⟨n : M, hn : mk' S n = mk' S m, hn' : ‖n‖ < ‖mk' S m‖ + ε⟩ :=
  norm_mk_lt (QuotientAddGroup.mk' S m) hε

Result:
case intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : (mk' S) n = (mk' S) m
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ ∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε

Proof state:
case intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ ∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε

Tactic:
use -m + n, hn

Result:
case right
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ ‖m + (-m + n)‖ < ‖(mk' S) m‖ + ε
-- Mathlib/Algebra/PresentedMonoid/Basic.lean
theorem ext {M : Type*} [Monoid M] (rels : FreeMonoid α → FreeMonoid α → Prop)
    {φ ψ : PresentedMonoid rels →* M} (hx : ∀ (x : α), φ (.of rels x) = ψ (.of rels x)) :
    φ = ψ

Proof state:
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ ⇑φ ∘ of rels = ⇑ψ ∘ of rels

Tactic:
ext

Result:
case h
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
x✝ : α
⊢ (⇑φ ∘ of rels) x✝ = (⇑ψ ∘ of rels) x✝

Proof state:
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ φ = ψ

Tactic:
apply MonoidHom.eq_of_eqOn_denseM (closure_range_of _)

Result:
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ EqOn (⇑φ) (⇑ψ) (range (of rels))

Proof state:
case h
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
x✝ : α
⊢ (⇑φ ∘ of rels) x✝ = (⇑ψ ∘ of rels) x✝

Tactic:
rw [Function.comp_apply]

Result:
case h
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
x✝ : α
⊢ φ (of rels x✝) = (⇑ψ ∘ of rels) x✝

Proof state:
case h
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
x✝ : α
⊢ φ (of rels x✝) = (⇑ψ ∘ of rels) x✝

Tactic:
exact hx _

Result:
no goals

Proof state:
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ EqOn (⇑φ) (⇑ψ) (range (of rels))

Tactic:
apply eqOn_range.mpr

Result:
α : Type u_2
M : Type u_3
inst✝ : Monoid M
rels : FreeMonoid α → FreeMonoid α → Prop
φ ψ : PresentedMonoid rels →* M
hx : ∀ (x : α), φ (of rels x) = ψ (of rels x)
⊢ ⇑φ ∘ of rels = ⇑ψ ∘ of rels
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_const_sub (v : V) (v₁ v₂ v₃ : V) : ∠ (v - v₁) (v - v₂) (v - v₃) = ∠ v₁ v₂ v₃

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
v v₁ v₂ v₃ : V
⊢ ∠ (v - v₁) (v - v₂) (v - v₃) = ∠ v₁ v₂ v₃

Tactic:
simpa only [vsub_eq_sub] using angle_const_vsub v v₁ v₂ v₃

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n

Proof state:
case succ
a b n✝ : Nat
ih : (a * b) ^ n✝ = a ^ n✝ * b ^ n✝
⊢ (a * b) ^ (n✝ + 1) = a ^ (n✝ + 1) * b ^ (n✝ + 1)

Tactic:
rw [Nat.pow_succ, Nat.pow_succ, Nat.pow_succ, Nat.mul_mul_mul_comm, ih]

Result:
no goals

Proof state:
case zero
a b : Nat
⊢ (a * b) ^ 0 = a ^ 0 * b ^ 0

Tactic:
rw [Nat.pow_zero, Nat.pow_zero, Nat.pow_zero, Nat.mul_one]

Result:
no goals

Proof state:
a b n : Nat
⊢ (a * b) ^ n = a ^ n * b ^ n

Tactic:
induction n with
| zero => rw [Nat.pow_zero, Nat.pow_zero, Nat.pow_zero, Nat.mul_one]
| succ _ ih => rw [Nat.pow_succ, Nat.pow_succ, Nat.pow_succ, Nat.mul_mul_mul_comm, ih]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem zpow_smul_mod_minimalPeriod (n : ℤ) :
    a ^ (n % (minimalPeriod (a • ·) b : ℤ)) • b = a ^ n • b

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ (n % ↑(minimalPeriod (fun x => a • x) b)) • b = a ^ n • b

Tactic:
rw [← period_eq_minimalPeriod, zpow_mod_period_smul]

Result:
no goals
-- Mathlib/RingTheory/Trace/Quotient.lean
lemma comap_map_eq_map_of_isLocalization_algebraMapSubmonoid :
    (Ideal.map (algebraMap R Sₚ) p).comap (algebraMap S Sₚ) = pS

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β : R
hβ : (Ideal.Quotient.mk p) β = ((Ideal.Quotient.mk p) α)⁻¹
⊢ ∃ β, ∃ γ ∈ p, β * α = 1 + γ

Tactic:
refine ⟨β, β * α - 1, ?_, ?_⟩

Result:
case intro.refine_1
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β : R
hβ : (Ideal.Quotient.mk p) β = ((Ideal.Quotient.mk p) α)⁻¹
⊢ β * α - 1 ∈ p

case intro.refine_2
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β : R
hβ : (Ideal.Quotient.mk p) β = ((Ideal.Quotient.mk p) α)⁻¹
⊢ β * α = 1 + (β * α - 1)
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem treesOfNumNodesEq_succ (n : ℕ) :
    treesOfNumNodesEq (n + 1) =
      (antidiagonal n).biUnion fun ij =>
        pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Proof state:
n : ℕ
⊢ treesOfNumNodesEq (n + 1) =
    (antidiagonal n).biUnion fun ij => pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
rw [treesOfNumNodesEq]

Result:
n : ℕ
⊢ ((antidiagonal n).attach.biUnion fun ijh => pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) =
    (antidiagonal n).biUnion fun ij => pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Proof state:
case h
n : ℕ
a✝ : Tree Unit
⊢ (a✝ ∈
      (antidiagonal n).attach.biUnion fun ijh =>
        pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) ↔
    a✝ ∈ (antidiagonal n).biUnion fun ij => pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ ((antidiagonal n).attach.biUnion fun ijh => pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) =
    (antidiagonal n).biUnion fun ij => pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
ext

Result:
case h
n : ℕ
a✝ : Tree Unit
⊢ (a✝ ∈
      (antidiagonal n).attach.biUnion fun ijh =>
        pairwiseNode (treesOfNumNodesEq (↑ijh).1) (treesOfNumNodesEq (↑ijh).2)) ↔
    a✝ ∈ (antidiagonal n).biUnion fun ij => pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)