harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfcₙAux_mem_range_inr (f : C(σₙ 𝕜 a, 𝕜)₀) :
    cfcₙAux hp₁ a ha f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Proof state:
case refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ IsClosed ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))

Tactic:
have : Continuous (Unitization.fst (R := 𝕜) (A := A)) :=
  Unitization.uniformEquivProd.continuous.fst

Result:
case refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
this : Continuous Unitization.fst
⊢ IsClosed ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Icc (-(π / 2)) (π / 2)) : 0 ≤ cos x :=
  sin_add_pi_div_two x ▸ sin_nonneg_of_mem_Icc ⟨by linarith [hx.1], by linarith [hx.2]⟩

Proof state:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ x + π / 2 ≤ π

Tactic:
linarith [hx.2]

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ x + π / 2

Tactic:
linarith [hx.1]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem ContMDiffWithinAt.comp {t : Set M'} {g : M' → M''} (x : M)
    (hg : ContMDiffWithinAt I' I'' n g t (f x)) (hf : ContMDiffWithinAt I I' n f s x)
    (st : MapsTo f s t) : ContMDiffWithinAt I I'' n (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : WithTop ℕ∞
t : Set M'
g : M' → M''
x : M
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑(extChartAt I' (f x)).symm)
      (↑(extChartAt I' (f x)).symm ⁻¹' t ∩ range ↑I') (↑(extChartAt I' (f x)) (f x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)
st : MapsTo f s t
⊢ ContinuousWithinAt (g ∘ f) s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
refine ⟨hg.1.comp hf.1 st, ?_⟩

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : WithTop ℕ∞
t : Set M'
g : M' → M''
x : M
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑(extChartAt I' (f x)).symm)
      (↑(extChartAt I' (f x)).symm ⁻¹' t ∩ range ↑I') (↑(extChartAt I' (f x)) (f x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)
st : MapsTo f s t
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑(extChartAt I x).symm)
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
-- Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean
theorem pow_dvd_pow_iff [IsDomain R] [IsIntegrallyClosed R]
    {n : ℕ} (hn : n ≠ 0) {a b : R} : a ^ n ∣ b ^ n ↔ a ∣ b

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
⊢ a ∣ b

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
ha : a = 0
⊢ a ∣ b

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
ha : ¬a = 0
⊢ a ∣ b

Proof state:
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ a ∣ b

Tactic:
refine ⟨k, IsFractionRing.injective R K ?_⟩

Result:
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ (algebraMap R K) b = (algebraMap R K) (a * k)
-- Mathlib/CategoryTheory/Sites/SheafHom.lean
lemma presheafHom_isSheafFor  :
    Presieve.IsSheafFor (presheafHom F G) S.arrows

Proof state:
case hunique.app
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₁.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
hy₂ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
⊢ y₁.app = y₂.app

Tactic:
ext ⟨Y : Over X⟩

Result:
case hunique.app.h.op
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₁.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
hy₂ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
⊢ y₁.app (op Y) = y₂.app (op Y)

Proof state:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
have H := app_cond hG x hx g (𝟙 _) (by simpa using hg)

Result:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g ≫ G.map (𝟙 Y).op = F.map (𝟙 Y).op ≫ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ S.arrows ((Z.hom ≫ φ.left) ≫ Y₁.hom)

Tactic:
simpa using hZ

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
@[simp]
lemma RationalMap.toRationalMap_toPartialMap [IsReduced X] [Y.IsSeparated]
    (f : X ⤏ Y) : f.toPartialMap.toRationalMap = f

Proof state:
case intro
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap

Tactic:
trans (f.toRationalMap.toPartialMap.restrict _
  f.dense_domain f.le_domain_toRationalMap).toRationalMap

Result:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap

X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap = f.toRationalMap

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap = f.toRationalMap

Tactic:
congr 1

Result:
case e_f
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯ = f

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
simpa using f.toPartialMap_toRationalMap_restrict

Result:
no goals

Proof state:
case e_f
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯ = f

Tactic:
exact PartialMap.ext _ f rfl (by simpa using f.toPartialMap_toRationalMap_restrict)

Result:
no goals

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
⊢ f.toPartialMap.toRationalMap = f

Tactic:
obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f

Result:
case intro
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Basic.lean
theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
  match b with
  | 0 => (Nat.mul_one _).symm
  | b+1 => (shiftLeft_eq _ b).trans <| by
    simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]

Proof state:
a b✝ b : Nat
⊢ 2 * a * 2 ^ b = a * 2 ^ (b + 1)

Tactic:
simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
@[simp] protected lemma Prime.primeFactors (hp : p.Prime) : p.primeFactors = {p}

Proof state:
p : ℕ
hp : Prime p
⊢ p.primeFactors = {p}

Tactic:
simp [Nat.primeFactors, primeFactorsList_prime hp]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.Coprime m n) :
    minpoly ℤ μ = minpoly ℤ (μ ^ m)

Proof state:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
hprime : Nat.Prime p
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))

Tactic:
have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)

Result:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))

Proof state:
case refine_1
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
h : IsPrimitiveRoot μ n✝
hn : Nat.Coprime 0 n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ 0)

Tactic:
congr

Result:
case refine_1.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
h : IsPrimitiveRoot μ n✝
hn : Nat.Coprime 0 n✝
⊢ μ = μ ^ 0

Proof state:
case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ : ℕ
⊢ ∀ (x : ℕ), IsUnit x → IsPrimitiveRoot μ n✝ → x.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ x)

Tactic:
intro u hunit _ _

Result:
case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : u.Coprime n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ u)

Proof state:
case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : u.Coprime n✝
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ u)

Tactic:
congr

Result:
case refine_2.e_x
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
h✝ : IsPrimitiveRoot μ n✝
hcop✝ : u.Coprime n✝
⊢ μ = μ ^ u
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem at_two (hp : p ≠ 2) : legendreSym p 2 = χ₈ p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ legendreSym p 2 = χ₈ ↑p

Tactic:
rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ 2 = ↑2

Tactic:
norm_cast

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p 2 = χ₈ ↑p

Tactic:
have : (2 : ZMod p) = (2 : ℤ) := by norm_cast

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ legendreSym p 2 = χ₈ ↑p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (ofList l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (ofList l).get? k' = some (cast ⋯ v)

Tactic:
simp_to_raw using Raw₀.get?_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
@[simp] lemma primeFactors_eq_empty : n.primeFactors = ∅ ↔ n = 0 ∨ n = 1

Proof state:
n : ℕ
⊢ n.primeFactors = ∅ ↔ n = 0 ∨ n = 1

Tactic:
constructor

Result:
case mp
n : ℕ
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1

case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactors = ∅

Proof state:
case mp
n : ℕ
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1

Tactic:
contrapose!

Result:
case mp
n : ℕ
⊢ n ≠ 0 ∧ n ≠ 1 → n.primeFactors ≠ ∅

Proof state:
case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactors = ∅

Tactic:
rintro (rfl | rfl) <;> simp

Result:
no goals

Proof state:
case mp.intro.intro
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
p : ℕ
hp : Prime p
hpn : p ∣ n
⊢ n.primeFactors ≠ ∅

Tactic:
exact Nonempty.ne_empty <| ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩

Result:
no goals

Proof state:
case mp
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
⊢ n.primeFactors ≠ ∅

Tactic:
obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2

Result:
case mp.intro.intro
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
p : ℕ
hp : Prime p
hpn : p ∣ n
⊢ n.primeFactors ≠ ∅

Proof state:
case mp
n : ℕ
⊢ n ≠ 0 ∧ n ≠ 1 → n.primeFactors ≠ ∅

Tactic:
rintro hn

Result:
case mp
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
⊢ n.primeFactors ≠ ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem ofNat'_val_eq_self [NeZero n] (x : Fin n) : (Fin.ofNat' n x) = x

Proof state:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑x < n

Tactic:
exact x.2

Result:
no goals

Proof state:
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ Fin.ofNat' n ↑x = x

Tactic:
ext

Result:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑(Fin.ofNat' n ↑x) = ↑x

Proof state:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑(Fin.ofNat' n ↑x) = ↑x

Tactic:
rw [val_ofNat', Nat.mod_eq_of_lt]

Result:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑x < n
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem coeff_mul_degree_add_degree (p q : R[X]) :
    coeff (p * q) (natDegree p + natDegree q) = leadingCoeff p * leadingCoeff q :=
  calc
    coeff (p * q) (natDegree p + natDegree q) =
        ∑ x ∈ antidiagonal (natDegree p + natDegree q), coeff p x.1 * coeff q x.2 :=
      coeff_mul _ _ _
    _ = coeff p (natDegree p) * coeff q (natDegree q)

Proof state:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
j : ℕ
h₁ : (p.natDegree, j).2 = q.natDegree
h₂ : (p.natDegree, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, j).1 * q.coeff (p.natDegree, j).2 = 0

Tactic:
dsimp at h₁

Result:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
j : ℕ
h₁ : j = q.natDegree
h₂ : (p.natDegree, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, j).1 * q.coeff (p.natDegree, j).2 = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∑ x ∈ antidiagonal (p.natDegree + q.natDegree), p.coeff x.1 * q.coeff x.2 = p.coeff p.natDegree * q.coeff q.natDegree

Tactic:
refine Finset.sum_eq_single (natDegree p, natDegree q) ?_ ?_

Result:
case refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ b ∈ antidiagonal (p.natDegree + q.natDegree), b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0

case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree) →
    p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_degree_lt
    (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),
  zero_mul]

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ b ∈ antidiagonal (p.natDegree + q.natDegree), b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0

Tactic:
rintro ⟨i, j⟩ h₁ h₂

Result:
case refine_1.mk
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ antidiagonal (p.natDegree + q.natDegree)
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
-- Mathlib/Logic/Function/Basic.lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
⊢ f x = g y ↔ f = g

Tactic:
refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z

case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y

Proof state:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z

Tactic:
rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h

Result:
no goals

Proof state:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y

Tactic:
rw [h, Subsingleton.elim x y]

Result:
no goals