harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean
lemma cfc_unitary_iff (f : R → R) (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ Set.EqOn (fun x => star (f x) * f x) 1 (spectrum R a) ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ cfc f a ∈ unitary A ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

Tactic:
simp only [unitary, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_setOf_eq]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ star (cfc f a) * cfc f a = 1 ∧ cfc f a * star (cfc f a) = 1 ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ star (cfc f a) * cfc f a = 1 ∧ cfc f a * star (cfc f a) = 1 ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

Tactic:
rw [← IsStarNormal.cfc_map (p := p) f a |>.star_comm_self |>.eq, and_self, ← cfc_one R a,
  ← cfc_star, ← cfc_mul .., cfc_eq_cfc_iff_eqOn]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ Set.EqOn (fun x => star (f x) * f x) 1 (spectrum R a) ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1
-- Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
theorem smul_finprod_perm [Finite G] (b : β) (g : G) :
    (g • ∏ᶠ h : G, h • b) = ∏ᶠ h : G, h • b

Proof state:
β : Type u_2
inst✝³ : CommMonoid β
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G β
inst✝ : Finite G
b : β
g : G
⊢ g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b

Tactic:
cases nonempty_fintype G

Result:
case intro
β : Type u_2
inst✝³ : CommMonoid β
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G β
inst✝ : Finite G
b : β
g : G
val✝ : Fintype G
⊢ g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b

Proof state:
case intro
β : Type u_2
inst✝³ : CommMonoid β
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G β
inst✝ : Finite G
b : β
g : G
val✝ : Fintype G
⊢ g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b

Tactic:
simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]

Result:
no goals
-- Mathlib/FieldTheory/KrullTopology.lean
theorem IntermediateField.fixingSubgroup_isOpen {K L : Type*} [Field K] [Field L] [Algebra K L]
    (E : IntermediateField K L) [FiniteDimensional K E] :
    IsOpen (E.fixingSubgroup : Set (L ≃ₐ[K] L))

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L
⊢ IsOpen ↑E.fixingSubgroup

Tactic:
have h_nhd := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L
h_nhd : E.fixingSubgroup.carrier ∈ 𝓝 1
⊢ IsOpen ↑E.fixingSubgroup

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L
h_nhd : E.fixingSubgroup.carrier ∈ 𝓝 1
⊢ IsOpen ↑E.fixingSubgroup

Tactic:
exact Subgroup.isOpen_of_mem_nhds _ h_nhd

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
⊢ IsOpen ↑E.fixingSubgroup

Tactic:
have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L :=
  ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L
⊢ IsOpen ↑E.fixingSubgroup
-- Mathlib/Algebra/Group/End.lean
theorem ofSubtype_subtypePerm {f : Perm α} (h₁ : ∀ x, p x ↔ p (f x)) (h₂ : ∀ x, f x ≠ x → p x) :
    ofSubtype (subtypePerm f h₁) = f :=
  Equiv.ext fun x => by
    by_cases hx : p x
    · exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx
    · rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
        Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]
      exact not_not.mp fun h => hx (h₂ x (Ne.symm h))

Proof state:
case pos
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (f x)
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx

Result:
no goals

Proof state:
case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (f x)
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
  Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]

Result:
case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (f x)
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ x = f x

Proof state:
case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (f x)
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ x = f x

Tactic:
exact not_not.mp fun h => hx (h₂ x (Ne.symm h))

Result:
no goals

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (f x)
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
by_cases hx : p x

Result:
case pos
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (f x)
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (f x)
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_add_uIcc : (fun x => a + x) '' [[b, c]] = [[a + b, a + c]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) '' [[b, c]] = [[a + b, a + c]]

Tactic:
simp [add_comm]

Result:
no goals
-- Mathlib/FieldTheory/Isaacs.lean
theorem nonempty_algHom_of_minpoly_eq
    (h : ∀ x : E, ∃ y : K, minpoly F x = minpoly F y) :
    Nonempty (E →ₐ[F] K) :=
  nonempty_algHom_of_exist_roots fun x ↦ have ⟨y, hy⟩ := h x; ⟨y, by rw [hy, minpoly.aeval]⟩

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, minpoly F x = minpoly F y
x : E
y : K
hy : minpoly F x = minpoly F y
⊢ (aeval y) (minpoly F x) = 0

Tactic:
rw [hy, minpoly.aeval]

Result:
no goals
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem eq_pow_order_mul_iterate_dslope (hp : HasFPowerSeriesAt f p z₀) :
    ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • (swap dslope z₀)^[p.order] f z

Proof state:
case h.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • p.coeff n) (f x)
this : ∀ k < p.order, p.coeff k = 0
s : E
hs1 : (x - z₀) ^ p.order • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • p.coeff (m + p.order)) s
⊢ f x = (x - z₀) ^ p.order • (swap dslope z₀)^[p.order] f x

Tactic:
convert hs1.symm

Result:
case h.e'_3.h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • p.coeff n) (f x)
this : ∀ k < p.order, p.coeff k = 0
s : E
hs1 : (x - z₀) ^ p.order • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • p.coeff (m + p.order)) s
⊢ (swap dslope z₀)^[p.order] f x = s
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : ¬dom c i
this : Decidable (dom c i)
⊢ getElem? c i = none

Tactic:
rw [getElem?_def]

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : ¬dom c i
this : Decidable (dom c i)
⊢ (if h : dom c i then some (getElem c i h) else none) = none

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : ¬dom c i
this : Decidable (dom c i)
⊢ (if h : dom c i then some (getElem c i h) else none) = none

Tactic:
exact dif_neg h

Result:
no goals

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : ¬dom c i
⊢ getElem? c i = none

Tactic:
have : Decidable (dom c i) := .isFalse h

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝¹ : GetElem? cont idx elem dom
inst✝ : LawfulGetElem cont idx elem dom
c : cont
i : idx
h : ¬dom c i
this : Decidable (dom c i)
⊢ getElem? c i = none
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_mul_goldConj : φ * ψ = -1

Proof state:
⊢ 1 ^ 2 - √5 ^ 2 = -(2 * 2)

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ φ * ψ = -1

Tactic:
field_simp

Result:
⊢ (1 + √5) * (1 - √5) = -(2 * 2)

Proof state:
⊢ (1 + √5) * (1 - √5) = -(2 * 2)

Tactic:
rw [← sq_sub_sq]

Result:
⊢ 1 ^ 2 - √5 ^ 2 = -(2 * 2)
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma withDensity_rnDeriv_eq_zero_iff_apply_eq_zero (κ η : Kernel α γ) [IsFiniteKernel κ]
    [IsFiniteKernel η] (a : α) :
    withDensity η (rnDeriv κ η) a = 0
      ↔ withDensity η (rnDeriv κ η) a (mutuallySingularSetSlice κ η a)ᶜ = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) univ = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ ((η.withDensity (κ.rnDeriv η)) a) univ = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
rw [← Measure.measure_univ_eq_zero]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) univ = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ ((η.withDensity (κ.rnDeriv η)) a) univ = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
  withDensity_rnDeriv_mutuallySingularSetSlice, zero_add]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/AlgebraicCard.lean
theorem cardinalMk_le_mul : #{ x : A // IsAlgebraic R x } ≤ #R[X] * ℵ₀

Proof state:
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀

Tactic:
exact cardinalMk_lift_le_mul R A

Result:
no goals

Proof state:
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀

Tactic:
rw [← lift_id #_, ← lift_id #R[X]]

Result:
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ lift.{u, u} #R[X] * ℵ₀
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
theorem charpoly_reindex (e : n ≃ m)
    (M : Matrix n n R) : (reindex e e M).charpoly = M.charpoly

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
e : n ≃ m
M : Matrix n n R
⊢ ((reindex e e) M).charmatrix.det = M.charmatrix.det

Tactic:
rw [charmatrix_reindex, Matrix.det_reindex_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
e : n ≃ m
M : Matrix n n R
⊢ ((reindex e e) M).charpoly = M.charpoly

Tactic:
unfold Matrix.charpoly

Result:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
e : n ≃ m
M : Matrix n n R
⊢ ((reindex e e) M).charmatrix.det = M.charmatrix.det
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem gcd_dedup (s : Multiset α) : (dedup s).gcd = s.gcd :=
  Multiset.induction_on s (by simp) fun a s IH ↦ by
    by_cases h : a ∈ s <;> simp [IH, h]
    unfold gcd
    rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
    apply (associated_normalize _).gcd_eq_left

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)) = GCDMonoid.gcd (normalize a) (fold GCDMonoid.gcd 0 (s.erase a))

Tactic:
apply (associated_normalize _).gcd_eq_left

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
by_cases h : a ∈ s <;> simp [IH, h]

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ s.gcd = GCDMonoid.gcd a s.gcd

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ (dedup 0).gcd = gcd 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ s.gcd = GCDMonoid.gcd a s.gcd

Tactic:
unfold gcd

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ fold GCDMonoid.gcd 0 s = GCDMonoid.gcd a (fold GCDMonoid.gcd 0 s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)) = GCDMonoid.gcd (normalize a) (fold GCDMonoid.gcd 0 (s.erase a))
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem emod_lt (a : ℤ) {b : ℤ} (H : b ≠ 0) : a % b < |b|

Proof state:
a b : ℤ
H : b ≠ 0
⊢ a % b < |b|

Tactic:
rw [← emod_abs]

Result:
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|

Proof state:
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|

Tactic:
exact emod_lt_of_pos _ (abs_pos.2 H)

Result:
no goals
-- Mathlib/Algebra/Order/Chebyshev.lean
theorem MonovaryOn.sum_smul_sum_le_card_smul_sum (hfg : MonovaryOn f g s) :
    (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i

Tactic:
classical
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn
rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]
exact sum_le_card_nsmul _ _ _ fun n _ ↦
  hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i) ≤ #(range #s) • ∑ i ∈ s, f i • g i

Tactic:
exact sum_le_card_nsmul _ _ _ fun n _ ↦
  hfg.sum_smul_comp_perm_le_sum_smul fun x hx ↦ hs fun h ↦ hx <| IsFixedPt.perm_pow h _

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i

Tactic:
rw [← card_range #s, sum_smul_sum_eq_sum_perm hσ]

Result:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i) ≤ #(range #s) • ∑ i ∈ s, f i • g i

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i

Tactic:
obtain ⟨σ, hσ, hs⟩ := s.countable_toSet.exists_cycleOn

Result:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem dvd_mul {x m n : ℕ} : x ∣ m * n ↔ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x

Proof state:
x m n : ℕ
⊢ x ∣ m * n ↔ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x

Tactic:
constructor

Result:
case mp
x m n : ℕ
⊢ x ∣ m * n → ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x

case mpr
x m n : ℕ
⊢ (∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x) → x ∣ m * n

Proof state:
case mp
x m n : ℕ
⊢ x ∣ m * n → ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x

Tactic:
intro h

Result:
case mp
x m n : ℕ
h : x ∣ m * n
⊢ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x

Proof state:
case mpr
x m n : ℕ
⊢ (∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x) → x ∣ m * n

Tactic:
rintro ⟨y, z, hy, hz, rfl⟩

Result:
case mpr.intro.intro.intro.intro
m n y z : ℕ
hy : y ∣ m
hz : z ∣ n
⊢ y * z ∣ m * n

Proof state:
case mpr.intro.intro.intro.intro
m n y z : ℕ
hy : y ∣ m
hz : z ∣ n
⊢ y * z ∣ m * n

Tactic:
exact mul_dvd_mul hy hz

Result:
no goals

Proof state:
case mp
x m n : ℕ
h : x ∣ m * n
⊢ ∃ y z, y ∣ m ∧ z ∣ n ∧ y * z = x

Tactic:
obtain ⟨⟨⟨y, hy⟩, ⟨z, hz⟩⟩, rfl⟩ := prod_dvd_and_dvd_of_dvd_prod h

Result:
case mp.mk.mk.mk.mk
m n y : ℕ
hy : y ∣ m
z : ℕ
hz : z ∣ n
h : ↑(⟨y, hy⟩, ⟨z, hz⟩).1 * ↑(⟨y, hy⟩, ⟨z, hz⟩).2 ∣ m * n
⊢ ∃ y_1 z_1, y_1 ∣ m ∧ z_1 ∣ n ∧ y_1 * z_1 = ↑(⟨y, hy⟩, ⟨z, hz⟩).1 * ↑(⟨y, hy⟩, ⟨z, hz⟩).2

Proof state:
case mp.mk.mk.mk.mk
m n y : ℕ
hy : y ∣ m
z : ℕ
hz : z ∣ n
h : ↑(⟨y, hy⟩, ⟨z, hz⟩).1 * ↑(⟨y, hy⟩, ⟨z, hz⟩).2 ∣ m * n
⊢ ∃ y_1 z_1, y_1 ∣ m ∧ z_1 ∣ n ∧ y_1 * z_1 = ↑(⟨y, hy⟩, ⟨z, hz⟩).1 * ↑(⟨y, hy⟩, ⟨z, hz⟩).2

Tactic:
exact ⟨y, z, hy, hz, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_three (R : Type*) [Ring R] : cyclotomic 3 R = X ^ 2 + X + 1

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 3 R = X ^ 2 + X + 1

Tactic:
simp [cyclotomic_prime, sum_range_succ']

Result:
no goals