harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma minpolyDiv_eq_of_isIntegrallyClosed [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
    [Algebra R K] [Algebra K S] [IsScalarTower R K S] [IsFractionRing R K] :
    minpolyDiv R x = minpolyDiv K x

Proof state:
R : Type u_1
K : Type u_3
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
x : S
hx : IsIntegral R x
inst✝⁶ : IsDomain R
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R K
inst✝² : Algebra K S
inst✝¹ : IsScalarTower R K S
inst✝ : IsFractionRing R K
⊢ minpolyDiv R x = minpolyDiv K x

Tactic:
delta minpolyDiv

Result:
R : Type u_1
K : Type u_3
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
x : S
hx : IsIntegral R x
inst✝⁶ : IsDomain R
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R K
inst✝² : Algebra K S
inst✝¹ : IsScalarTower R K S
inst✝ : IsFractionRing R K
⊢ map (algebraMap R S) (minpoly R x) /ₘ (X - C x) = map (algebraMap K S) (minpoly K x) /ₘ (X - C x)

Proof state:
R : Type u_1
K : Type u_3
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
x : S
hx : IsIntegral R x
inst✝⁶ : IsDomain R
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R K
inst✝² : Algebra K S
inst✝¹ : IsScalarTower R K S
inst✝ : IsFractionRing R K
⊢ map (algebraMap R S) (minpoly R x) /ₘ (X - C x) = map (algebraMap K S) (minpoly K x) /ₘ (X - C x)

Tactic:
rw [IsScalarTower.algebraMap_eq R K S, ← map_map,
  ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR

Proof state:
⊢ @zipWith = @zipWithTR

Tactic:
funext α β γ f as bs

Result:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
⊢ zipWith f as bs = zipWithTR f as bs

Proof state:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
⊢ zipWith f as bs = zipWithTR f as bs

Tactic:
exact (go as bs #[]).symm

Result:
no goals

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as✝ : List α
bs✝ : List β
a : α
as : List α
b : β
bs : List β
acc : Array γ
⊢ zipWithTR.go f (a :: as) (b :: bs) acc = acc.toList ++ zipWith f (a :: as) (b :: bs)

Tactic:
simp [zipWithTR.go, zipWith, go as bs]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → β → γ
as : List α
bs : List β
head✝ : α
tail✝ : List α
acc : Array γ
⊢ zipWithTR.go f (head✝ :: tail✝) [] acc = acc.toList ++ zipWith f (head✝ :: tail✝) []

Tactic:
simp [zipWithTR.go, zipWith]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_ofPrime (p : Nat.Primes) :
    (p : ℕ+).factorMultiset = PrimeMultiset.ofPrime p

Proof state:
case a
p : Nat.Primes
⊢ (↑p).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod

Tactic:
rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]

Result:
no goals

Proof state:
case a
p : Nat.Primes
⊢ factorMultisetEquiv.symm (↑p).factorMultiset = factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)

Tactic:
change (p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod

Result:
case a
p : Nat.Primes
⊢ (↑p).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod

Proof state:
p : Nat.Primes
⊢ (↑p).factorMultiset = PrimeMultiset.ofPrime p

Tactic:
apply factorMultisetEquiv.symm.injective

Result:
case a
p : Nat.Primes
⊢ factorMultisetEquiv.symm (↑p).factorMultiset = factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)
-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.algebraMap_intTrace (x : B) :
    algebraMap A K (Algebra.intTrace A B x) = Algebra.trace K L (algebraMap B L x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A B
x : B
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) x)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) :=
  Module.Finite_of_isLocalization A B _ _ A⁰

Result:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra B L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsScalarTower A K L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A B
x : B
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
    (H : ∀ (a : α), a ∈ o → p a) (g : γ) (g' : β → γ) :
    (o.pmap f H).elim g g' =
       o.pelim g (fun a h => g' (f a (H a h)))

Proof state:
α : Type u_1
β : Type u_2
γ : Sort u_3
p : α → Prop
f : (a : α) → p a → β
o : Option α
H : ∀ (a : α), a ∈ o → p a
g : γ
g' : β → γ
⊢ (pmap f o H).elim g g' = o.pelim g fun a h => g' (f a ⋯)

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sup_biSup {p : ι → Prop} {f : ∀ i, p i → α} {a : α} (h : ∃ i, p i) :
    (a ⊔ ⨆ (i) (h : p i), f i h) = ⨆ (i) (h : p i), a ⊔ f i h

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h

Tactic:
simpa only [sup_comm] using @biSup_sup α _ _ p _ _ h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
lemma map_const (μ : Measure α) (c : β) : μ.map (fun _ ↦ c) = (μ Set.univ) • dirac c

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∉ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

Tactic:
rw [if_neg hsc, (Set.indicator_eq_zero_iff_not_mem _).mpr hsc, measure_empty, mul_zero]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (map (fun x => c) μ) s = μ univ * s.indicator 1 c

Tactic:
rw [Measure.map_apply measurable_const hs, Set.preimage_const]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

Tactic:
rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
⊢ map (fun x => c) μ = μ univ • dirac c

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (map (fun x => c) μ) s = (μ univ • dirac c) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (map (fun x => c) μ) s = (μ univ • dirac c) s

Tactic:
simp only [aemeasurable_const, measurable_const, Measure.coe_smul, Pi.smul_apply,
  dirac_apply' _ hs, smul_eq_mul]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (map (fun x => c) μ) s = μ univ * s.indicator 1 c

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

Tactic:
by_cases hsc : c ∈ s

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∈ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
hsc : c ∉ s
⊢ μ (if c ∈ s then univ else ∅) = μ univ * s.indicator 1 c
-- Mathlib/Algebra/Lie/InvariantForm.lean
lemma orthogonal_disjoint
    (Φ : LinearMap.BilinForm R L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : Φ.lieInvariant L)
    -- TODO: replace the following assumption by a typeclass assumption `[HasNonAbelianAtoms]`
    (hL : ∀ I : LieIdeal R L, IsAtom I → ¬IsLieAbelian I)
    (I : LieIdeal R L) (hI : IsAtom I) :
    Disjoint I (orthogonal Φ hΦ_inv I)

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
⊢ I = ⊥

Tactic:
rw [eq_bot_iff, ← lie_eq_self_of_isAtom_of_nonabelian I hI (hL I hI),
    LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⊥

Tactic:
rintro _ ⟨x, y, rfl⟩

Result:
case intro.intro
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x y : ↥I
⊢ ⁅↑x, ↑y⁆ ∈ ↑⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
⊢ I ⊓ orthogonal Φ hΦ_inv I ≤ I ∧ I ⊓ orthogonal Φ hΦ_inv I ≠ I

Tactic:
suffices ¬I ≤ orthogonal Φ hΦ_inv I by simpa

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
⊢ ¬I ≤ orthogonal Φ hΦ_inv I
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[reassoc (attr := simp)]
lemma glueDataObjMap_glueDataObjι {U V : X.affineOpens} (h : U ≤ V) :
    I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h

Proof state:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE h ≫ (↑V).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h

Tactic:
rw [← IsAffineOpen.isoSpec_hom, Iso.hom_inv_id, Category.comp_id]

Result:
no goals

Proof state:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ (↑U).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h

Tactic:
erw [Scheme.Opens.toSpecΓ_SpecMap_map_assoc U.1 V.1 h]

Result:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE h ≫ (↑V).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h

Proof state:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Tactic:
rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom, CommRingCat.ofHom_hom]

Result:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ (↑U).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Tactic:
congr 1

Result:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h

Tactic:
rw [glueDataObjMap, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
  Ideal.quotientMap_comp_mk, CommRingCat.ofHom_comp, Spec.map_comp_assoc, glueDataObjι,
  Category.assoc]

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet
    (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    Integrable (fun ω ↦ |X ω| ^ n * cexp (z * X ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω => ↑|X ω| ^ n * cexp (z * ↑(X ω))) μ

Tactic:
convert integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)

Result:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ ↑|X x✝| ^ n = ↑(|X x✝| ^ ↑n)

Proof state:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ ↑|X x✝| ^ n = ↑(|X x✝| ^ ↑n)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem imaginaryPart_apply_coe (a : A) : (ℑ a : A) = -I • (2 : ℝ)⁻¹ • (a - star a)

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑((skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ) a) = -I • 2⁻¹ • (a - star a)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, skewAdjoint.negISMul_apply_coe,
  skewAdjointPart_apply_coe, invOf_eq_inv, neg_smul]

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℑ a) = -I • 2⁻¹ • (a - star a)

Tactic:
unfold imaginaryPart

Result:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑((skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ) a) = -I • 2⁻¹ • (a - star a)
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem hasLineDerivAt_iff_isLittleO_nhds_zero :
    HasLineDerivAt 𝕜 f f' x v ↔
      (fun t : 𝕜 => f (x + t • v) - f x - t • f') =o[𝓝 0] fun t => t

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
f' : F
x v : E
⊢ HasLineDerivAt 𝕜 f f' x v ↔ (fun t => f (x + t • v) - f x - t • f') =o[𝓝 0] fun t => t

Tactic:
simp only [HasLineDerivAt, hasDerivAt_iff_isLittleO_nhds_zero, zero_add, zero_smul, add_zero]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem iInf_localization_eq_bot : (⨅ v : MaximalSpectrum R,
    Localization.subalgebra.ofField K _ v.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥

Proof state:
case h.mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
hdenom : 1 ∉ denom
⊢ False

Tactic:
rcases denom.exists_le_maximal (denom.ne_top_iff_one.mpr hdenom) with ⟨max, hmax, hle⟩

Result:
case h.mp.intro.intro
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : x ∉ range ⇑(algebraMap R K)
hlocal : ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K x) 1
hdenom : 1 ∉ denom
max : Ideal R
hmax : max.IsMaximal
hle : denom ≤ max
⊢ False

Proof state:
case h.mp.intro.intro.intro.intro.intro
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : max.IsMaximal
n d : R
hd : d ∈ { asIdeal := max, isMaximal := hmax }.asIdeal.primeCompl
hrange : (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∉ range ⇑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) 1
hdenom : 1 ∉ denom
hle : denom ≤ max
⊢ False

Tactic:
exact hd (hle ⟨n, by simp [denom, Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
  (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]⟩)

Result:
no goals

Proof state:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : max.IsMaximal
n d : R
hd : d ∈ { asIdeal := max, isMaximal := hmax }.asIdeal.primeCompl
hrange : (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∉ range ⇑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    (algebraMap R K) n * ((algebraMap R K) d)⁻¹ ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
denom : Ideal R := Submodule.comap (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) 1
hdenom : 1 ∉ denom
hle : denom ≤ max
⊢ (LinearMap.toSpanSingleton R K 1) n = (LinearMap.toSpanSingleton R K ((algebraMap R K) n * ((algebraMap R K) d)⁻¹)) d

Tactic:
simp [denom, Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
(map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invOneSubPow_eq_inv_one_sub_pow :
    invOneSubPow S d =
      (Units.mkOfMulEqOne (1 - X) (mk 1 : S⟦X⟧) <|
        Eq.trans (mul_comm _ _) (mk_one_mul_one_sub_eq_one S))⁻¹ ^ d

Proof state:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ invOneSubPow S (d + 1) = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1))⁻¹

Tactic:
exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <| by
  rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
  exact (invOneSubPow S (d + 1)).inv_val).symm

Result:
no goals

Proof state:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1) * invOneSubPow S (d + 1) = 1

Tactic:
rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]

Result:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ ↑(Units.mkOfMulEqOne (1 - X) (mk 1) ⋯) ^ (d + 1) * ↑(invOneSubPow S (d + 1)) = 1

Proof state:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ invOneSubPow S (d + 1) = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ (d + 1)

Tactic:
rw [inv_pow]

Result:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ invOneSubPow S (d + 1) = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1))⁻¹

Proof state:
S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d

Tactic:
induction d with
| zero => exact Eq.symm <| pow_zero _
| succ d _ =>
    rw [inv_pow]
    exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <| by
      rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
      exact (invOneSubPow S (d + 1)).inv_val).symm

Result:
no goals

Proof state:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ ↑(Units.mkOfMulEqOne (1 - X) (mk 1) ⋯) ^ (d + 1) * ↑(invOneSubPow S (d + 1)) = 1

Tactic:
exact (invOneSubPow S (d + 1)).inv_val

Result:
no goals

Proof state:
case zero
S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ invOneSubPow S 0 = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ 0

Tactic:
exact Eq.symm <| pow_zero _

Result:
no goals