harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Totient.lean
theorem totient_mul_of_prime_of_not_dvd {p n : ℕ} (hp : p.Prime) (h : ¬p ∣ n) :
    (p * n).totient = (p - 1) * n.totient

Proof state:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n

Tactic:
simpa [h] using coprime_or_dvd_of_prime hp n

Result:
no goals

Proof state:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n

Tactic:
rw [totient_mul _, totient_prime hp]

Result:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_lt_conjugate' {a b : R} (hab : a < b) {c : R} (hc : IsRegular c) :
    c * a * star c < c * b * star c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ c * a * star c < c * b * star c

Tactic:
simpa only [star_star] using conjugate_lt_conjugate hab hc.star

Result:
no goals
-- Mathlib/Algebra/Ring/Units.lean
theorem neg_divp (a : α) (u : αˣ) : -(a /ₚ u) = -a /ₚ u

Proof state:
α : Type u
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
u : αˣ
⊢ -(a /ₚ u) = -a /ₚ u

Tactic:
simp only [divp, neg_mul]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.exists_nonzero_eq_adjoin_mul
    {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) :
    ∃ᵉ (t ∈ Algebra.adjoin R {s}) (r ≠ (0 : R)), s * t = algebraMap R S r

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : (aeval s) (q - C (q.coeff 0)) = (aeval s) (X * p)
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)

Tactic:
rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
⊢ ∃ t ∈ Algebra.adjoin R {s}, ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r

Tactic:
have ⟨p, hp⟩ := X_dvd_sub_C (p := q)

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : q - C (q.coeff 0) = X * p
⊢ ∃ t ∈ Algebra.adjoin R {s}, ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : q - C (q.coeff 0) = X * p
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)

Tactic:
apply_fun aeval s at hp

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : (aeval s) (q - C (q.coeff 0)) = (aeval s) (X * p)
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
⊢ ∃ t ∈ Algebra.adjoin R {s}, ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r

Tactic:
have ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
⊢ ∃ t ∈ Algebra.adjoin R {s}, ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : q - C (q.coeff 0) = X * p
⊢ ∃ t ∈ Algebra.adjoin R {s}, ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r

Tactic:
refine ⟨aeval s p, aeval_mem_adjoin_singleton _ _, _, neg_ne_zero.mpr hq0, ?_⟩

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : q - C (q.coeff 0) = X * p
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem prod_top (K : Subgroup G) : K.prod (⊤ : Subgroup N) = K.comap (MonoidHom.fst G N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
x : G × N
⊢ x ∈ K.prod ⊤ ↔ x ∈ comap (MonoidHom.fst G N) K

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem infinite_range_iff {f : α → β} (hi : Injective f) :
    (range f).Infinite ↔ Infinite α

Proof state:
α : Type u
β : Type v
f : α → β
hi : Injective f
⊢ (range f).Infinite ↔ Infinite α

Tactic:
rw [← image_univ, infinite_image_iff hi.injOn, infinite_univ_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_iff_integrableOn_Ioc_of_le (hab : a ≤ b) :
    IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ

Tactic:
rw [intervalIntegrable_iff, uIoc_of_le hab]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem π_arrow (j : J) : π arrows j ≫ arrows _ = base arrows

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
j : J
⊢ π arrows j ≫ arrows j = base arrows

Tactic:
apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term j)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteVerts_inter_verts_set_right_eq :
    G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s

Tactic:
ext <;> simp +contextual [imp_false]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_apply_le (f : α → ℝ≥0∞) (s : Set α) :
    ∫⁻ a in s, f a ∂μ ≤ μ.withDensity f s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable (μ.withDensity f) s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s

Tactic:
calc
∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in t, f a ∂μ :=
  lintegral_mono_set (subset_toMeasurable (withDensity μ f) s)
_ = μ.withDensity f t :=
  (withDensity_apply f (measurableSet_toMeasurable (withDensity μ f) s)).symm
_ = μ.withDensity f s := measure_toMeasurable s

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s

Tactic:
let t := toMeasurable (μ.withDensity f) s

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable (μ.withDensity f) s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s
-- Mathlib/RingTheory/DedekindDomain/Different.lean
@[simp]
lemma dual_le_dual (hI : I ≠ 0) (hJ : J ≠ 0) :
    dual A K I ≤ dual A K J ↔ J ≤ I

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≠ 0

Tactic:
rwa [dual_ne_zero_iff]

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)

Tactic:
rw [le_dual_iff A K hJ, le_dual_iff A K (I := J) (by rwa [dual_ne_zero_iff]), mul_comm]

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ I

Tactic:
nth_rewrite 2 [← dual_dual A K I]

Result:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
hI : I ≠ 0
hJ : J ≠ 0
⊢ dual A K I ≤ dual A K J ↔ J ≤ dual A K (dual A K I)
-- Mathlib/Data/Set/Basic.lean
theorem strictMonoOn_iff_strictMono : StrictMonoOn f s ↔
    StrictMono fun a : s => f a

Proof state:
α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMonoOn f s ↔ StrictMono fun a => f ↑a

Tactic:
simp [StrictMono, StrictMonoOn]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
@[simp] lemma maxGenEigenSpace_toEnd_eq_top [IsNilpotent L M] (x : L) :
    ((toEnd R L M x).maxGenEigenspace 0) = ⊤

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
⊢ m ∈ ((toEnd R L M) x).maxGenEigenspace 0 ↔ m ∈ ⊤

Tactic:
simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, Submodule.mem_top,
  iff_true]

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
⊢ ∃ k, ((toEnd R L M) x ^ k) m = 0

Proof state:
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
k : ℕ
hk : ∀ (x : L), (toEnd R L M) x ^ k = 0
⊢ ∃ k, ((toEnd R L M) x ^ k) m = 0

Tactic:
exact ⟨k, by simp [hk x]⟩

Result:
no goals

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
⊢ ∃ k, ((toEnd R L M) x ^ k) m = 0

Tactic:
obtain ⟨k, hk⟩ := exists_forall_pow_toEnd_eq_zero R L M

Result:
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
k : ℕ
hk : ∀ (x : L), (toEnd R L M) x ^ k = 0
⊢ ∃ k, ((toEnd R L M) x ^ k) m = 0

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
⊢ ((toEnd R L M) x).maxGenEigenspace 0 = ⊤

Tactic:
ext m

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
⊢ m ∈ ((toEnd R L M) x).maxGenEigenspace 0 ↔ m ∈ ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
k : ℕ
hk : ∀ (x : L), (toEnd R L M) x ^ k = 0
⊢ ((toEnd R L M) x ^ k) m = 0

Tactic:
simp [hk x]

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem prod_primeFactors_sdiff_of_squarefree {n : ℕ} (hn : Squarefree n) {t : Finset ℕ}
    (ht : t ⊆ n.primeFactors) :
    ∏ a ∈ (n.primeFactors \ t), a = n / ∏ a ∈ t, a

Proof state:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a

Tactic:
refine symm <| Nat.div_eq_of_eq_mul_left (Finset.prod_pos
  fun p hp => (prime_of_mem_primeFactorsList (List.mem_toFinset.mp (ht hp))).pos) ?_

Result:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = (∏ a ∈ n.primeFactors \ t, a) * ∏ a ∈ t, a

Proof state:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = (∏ a ∈ n.primeFactors \ t, a) * ∏ a ∈ t, a

Tactic:
rw [Finset.prod_sdiff ht, prod_primeFactors_of_squarefree hn]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem congr_pow (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ) :
    congr f g ^ n = congr (f ^ n) (g ^ n)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)

Tactic:
induction n with
| zero => exact congr_refl_refl.symm
| succ n ih => simp_rw [pow_succ, ih, congr_mul]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
⊢ congr f g ^ 0 = congr (f ^ 0) (g ^ 0)

Tactic:
exact congr_refl_refl.symm

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
ih : congr f g ^ n = congr (f ^ n) (g ^ n)
⊢ congr f g ^ (n + 1) = congr (f ^ (n + 1)) (g ^ (n + 1))

Tactic:
simp_rw [pow_succ, ih, congr_mul]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem IsPurelyInseparable.insepDegree_eq [IsPurelyInseparable F E] :
    insepDegree F E = Module.rank F E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsPurelyInseparable F E
⊢ insepDegree F E = Module.rank F E

Tactic:
rw [insepDegree, separableClosure.eq_bot_of_isPurelyInseparable, rank_bot']

Result:
no goals
-- Mathlib/GroupTheory/Perm/Option.lean
theorem Equiv.optionCongr_sign {α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) :
    Perm.sign e.optionCongr = Perm.sign e

Proof state:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ∀ (f : Perm α) (x y : α),
    x ≠ y → Perm.sign (optionCongr f) = Perm.sign f → Perm.sign (optionCongr (swap x y * f)) = Perm.sign (swap x y * f)

Tactic:
intro f x y hne h

Result:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e f : Perm α
x y : α
hne : x ≠ y
h : Perm.sign (optionCongr f) = Perm.sign f
⊢ Perm.sign (optionCongr (swap x y * f)) = Perm.sign (swap x y * f)

Proof state:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e f : Perm α
x y : α
hne : x ≠ y
h : Perm.sign (optionCongr f) = Perm.sign f
⊢ Perm.sign (optionCongr (swap x y * f)) = Perm.sign (swap x y * f)

Tactic:
simp [h, hne, Perm.mul_def, ← Equiv.optionCongr_trans]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ Perm.sign (optionCongr 1) = Perm.sign 1

Tactic:
simp [Perm.one_def]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ Perm.sign (optionCongr e) = Perm.sign e

Tactic:
refine Perm.swap_induction_on e ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ Perm.sign (optionCongr 1) = Perm.sign 1

case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ∀ (f : Perm α) (x y : α),
    x ≠ y → Perm.sign (optionCongr f) = Perm.sign f → Perm.sign (optionCongr (swap x y * f)) = Perm.sign (swap x y * f)
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_enorm_of_ae_nonneg {f : α → ℝ} (h_nonneg : 0 ≤ᵐ[μ] f) :
    ∫⁻ x, ‖f x‖ₑ ∂μ = ∫⁻ x, .ofReal (f x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
apply lintegral_congr_ae

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
⊢ (fun a => ‖f a‖ₑ) =ᶠ[ae μ] fun a => ENNReal.ofReal (f a)

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
x : α
hx : 0 x ≤ f x
⊢ ‖f x‖ₑ = ENNReal.ofReal (f x)

Tactic:
rw [Real.enorm_eq_ofReal hx]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
⊢ (fun a => ‖f a‖ₑ) =ᶠ[ae μ] fun a => ENNReal.ofReal (f a)

Tactic:
filter_upwards [h_nonneg] with x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
x : α
hx : 0 x ≤ f x
⊢ ‖f x‖ₑ = ENNReal.ofReal (f x)
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_eq_top_iff {x : ℝ≥0∞} {y : ℝ} : x ^ y = ⊤ ↔ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y

Proof state:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ y = ⊤ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ⊤ ∧ 0 < y

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Result:
no goals

Proof state:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ⊤ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ⊤ ∧ 0 < y

Tactic:
simp [← coe_rpow_of_ne_zero h, h]

Result:
no goals

Proof state:
case top
y : ℝ
⊢ ⊤ ^ y = ⊤ ↔ ⊤ = 0 ∧ y < 0 ∨ ⊤ = ⊤ ∧ 0 < y

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Result:
no goals

Proof state:
case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = ⊤ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ⊤ ∧ 0 < y

Tactic:
by_cases h : x = 0

Result:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ y = ⊤ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ⊤ ∧ 0 < y

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ⊤ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ⊤ ∧ 0 < y
-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
lemma endEquivAutGalois_π (f : End F) (A : PointedGaloisObject F) :
    F.map (AutGalois.π F A (endEquivAutGalois F f)).hom A.pt = f.app A A.pt

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm (f.app A.obj A.pt)).hom A.pt = f.app A.obj A.pt

Tactic:
erw [evaluationEquivOfIsGalois_symm_fiber]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map
      (↑(((sectionsFunctor (PointedGaloisObject F)).mapIso (autIsoFibers F)).symm.toEquiv
              ((endEquivSectionsFibers F) f))
          A).hom
      A.pt =
    f.app A.obj A.pt

Tactic:
change F.map ((((sectionsFunctor _).map (autIsoFibers F).inv) _).val A).hom A.pt = _

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map (↑((sectionsFunctor (PointedGaloisObject F)).map (autIsoFibers F).inv ((endEquivSectionsFibers F) f)) A).hom
      A.pt =
    f.app A.obj A.pt

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm (↑((endEquivSectionsFibers F) f) A)).hom A.pt = f.app A.obj A.pt

Tactic:
simp only [endEquivSectionsFibers_π]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm (f.app A.obj A.pt)).hom A.pt = f.app A.obj A.pt

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map (↑((sectionsFunctor (PointedGaloisObject F)).map (autIsoFibers F).inv ((endEquivSectionsFibers F) f)) A).hom
      A.pt =
    f.app A.obj A.pt

Tactic:
dsimp [autIsoFibers]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm (↑((endEquivSectionsFibers F) f) A)).hom A.pt = f.app A.obj A.pt

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map ((AutGalois.π F A) ((endEquivAutGalois F) f)).hom A.pt = f.app A.obj A.pt

Tactic:
dsimp [endEquivAutGalois, AutGalois.π_apply]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ F.map
      (↑(((sectionsFunctor (PointedGaloisObject F)).mapIso (autIsoFibers F)).symm.toEquiv
              ((endEquivSectionsFibers F) f))
          A).hom
      A.pt =
    f.app A.obj A.pt
-- Mathlib/Analysis/ConstantSpeed.lean
theorem hasConstantSpeedOnWith_iff_variationOnFromTo_eq :
    HasConstantSpeedOnWith f s l ↔ LocallyBoundedVariationOn f s ∧
      ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), variationOnFromTo f s x y = l * (y - x)

Proof state:
case mp.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ (ENNReal.ofReal (↑l * (y - x))).toReal = ↑l * (y - x)

Tactic:
exact ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr xy))

Result:
no goals

Proof state:
case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal (↑l * (x - y))).toReal = ↑l * (x - y)
⊢ -(↑l * (x - y)) = ↑l * (y - x)

Tactic:
ring

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
@[simp] lemma multinomial_singleton (a : α) (f : α → ℕ) : multinomial {a} f = 1

Proof state:
α : Type u_1
a : α
f : α → ℕ
⊢ (f a + ∑ i ∈ ∅, f i).choose (f a) * multinomial ∅ f = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
f : α → ℕ
⊢ multinomial {a} f = 1

Tactic:
rw [← cons_empty, multinomial_cons]

Result:
α : Type u_1
a : α
f : α → ℕ
⊢ (f a + ∑ i ∈ ∅, f i).choose (f a) * multinomial ∅ f = 1