harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aeval_algHom_apply {F : Type*} [FunLike F A B] [AlgHomClass F R A B]
    (f : F) (x : A) (p : R[X]) :
    aeval (f x) p = f (aeval x p)

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (a : R), (aeval (f x)) (C a) = f ((aeval x) (C a))

Tactic:
simp [AlgHomClass.commutes]

Result:
no goals

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    (aeval (f x)) (C a * X ^ n) = f ((aeval x) (C a * X ^ n)) →
      (aeval (f x)) (C a * X ^ (n + 1)) = f ((aeval x) (C a * X ^ (n + 1)))

Tactic:
simp [AlgHomClass.commutes]

Result:
no goals

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ (aeval (f x)) (p + q) = f ((aeval x) (p + q))

Tactic:
rw [map_add, hp, hq, ← map_add, ← map_add]

Result:
no goals

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ (aeval (f x)) p = f ((aeval x) p)

Tactic:
refine Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => ?_)
  (by simp [AlgHomClass.commutes])

Result:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ (aeval (f x)) (p + q) = f ((aeval x) (p + q))
-- Mathlib/LinearAlgebra/InvariantBasisNumber.lean
theorem card_le_of_injective [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α → R) →ₗ[R] β → R) (i : Injective f) : Fintype.card α ≤ Fintype.card β

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact
  le_of_fin_injective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
    (((LinearEquiv.symm Q).injective.comp i).comp (LinearEquiv.injective P))

Result:
no goals

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card α ≤ Fintype.card β

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ⇑f
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card α ≤ Fintype.card β
-- Mathlib/Analysis/Convex/Deriv.lean
theorem antitoneOn_deriv (hfc : ConcaveOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) :
    AntitoneOn (deriv f) S

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ AntitoneOn (deriv f) S

Tactic:
simpa only [Pi.neg_def, deriv.neg, neg_neg] using
  (hfc.neg.monotoneOn_deriv (fun x hx ↦ (hfd x hx).neg)).neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k fallback : α} :
    (m.erase k).getKeyD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k fallback : α
⊢ (m.erase k).getKeyD k fallback = fallback

Tactic:
simp_to_model [erase] using List.getKeyD_eraseKey_self

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
    (x.rotateLeft r)[i] =
      if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)]

Proof state:
w : Nat
x : BitVec w
r i : Nat
h : i < w
⊢ (x.rotateLeft r)[i] = if h' : i < r % w then x[w - r % w + i] else x[i - r % w]

Tactic:
simp [← BitVec.getLsbD_eq_getElem, h]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem exists_Polynomial_intValuation_lt (F : K⟦X⟧) (η : ℤₘ₀ˣ) :
    ∃ P : K[X], (PowerSeries.idealX K).intValuation (F - P) < η

Proof state:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ Valued.v ((ofPowerSeries ℤ K) (F - ↑(trunc (d + 1) F))) ≤ ↑(Multiplicative.ofAdd (-(↑d + 1)))

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr

Result:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
⊢ ∀ n < d + 1, (PowerSeries.coeff K n) (F - ↑(trunc (d + 1) F)) = 0

Proof state:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : 1 < η
⊢ (PowerSeries.idealX K).intValuation (F - ↑0) < ↑η

Tactic:
simpa using (intValuation_le_one (PowerSeries.idealX K) F).trans_lt h_neg

Result:
no goals

Proof state:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑η * ↑(Multiplicative.ofAdd (-1)) < ↑η * 1

Tactic:
gcongr

Result:
case h.a0
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ 0 < ↑η

case h.bc
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : ℤₘ₀ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑(trunc (d + 1) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ ↑(Multiplicative.ofAdd (-1)) < 1
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_mono (f : X ⟶ Y) [Mono f] : imageSubobject f = Subobject.mk f :=
  eq_of_comm (imageSubobjectIso f ≪≫ imageMonoIsoSource f ≪≫ (underlyingIso f).symm) (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageSubobjectIso f ≪≫ imageMonoIsoSource f ≪≫ (underlyingIso f).symm).hom ≫ (Subobject.mk f).arrow =
    (imageSubobject f).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem DenseRange.piMap {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (Y i)]
    {f : (i : ι) → (X i) → (Y i)} (hf : ∀ i, DenseRange (f i)):
    DenseRange (Pi.map f)

Proof state:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ DenseRange (Pi.map f)

Tactic:
rw [DenseRange, Set.range_piMap]

Result:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (univ.pi fun i => range (f i))

Proof state:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (univ.pi fun i => range (f i))

Tactic:
exact dense_pi Set.univ (fun i _ => hf i)

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem eventually_nhdsWithin {x : X} (p : Y → Prop) {s : Set X}
    (hx : x ∈ e.source) : (∀ᶠ y in 𝓝[e.symm ⁻¹' s] e x, p y) ↔ ∀ᶠ x in 𝓝[s] x, p (e x)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : Y) in map (↑e) (𝓝[s] x), p b

Tactic:
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p (↑e x)

Tactic:
refine Iff.trans ?_ eventually_map

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : Y) in map (↑e) (𝓝[s] x), p b
-- Mathlib/FieldTheory/Extension.lean
theorem lt_iff_le_carrier_ne : L₁ < L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier

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
L₁ L₂ : Lifts F E K
h : L₁ ≤ L₂
⊢ L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier

Tactic:
simp_rw [Ne, eq_iff_le_carrier_eq, h, true_and]

Result:
no goals

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
L₁ L₂ : Lifts F E K
⊢ L₁ < L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier

Tactic:
rw [lt_iff_le_and_ne, and_congr_right]

Result:
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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ → (L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier)

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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ → (L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier)

Tactic:
intro h

Result:
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
L₁ L₂ : Lifts F E K
h : L₁ ≤ L₂
⊢ L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq
    {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
    ((extChartAt I x).symm ⁻¹' s ∩ range I : Set E) =ᶠ[𝓝 (extChartAt I x x)]
      ((extChartAt I x).target ∩
        (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) : Set E)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x =
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] ↑(extChartAt I x) x

Tactic:
exact hc.nhdsWithin_extChartAt_symm_preimage_inter_range

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(extChartAt I x) x)]
    (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x =
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] ↑(extChartAt I x) x
-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem iso_of_restrict_iso {ℱ ℱ' : Sheaf K A} (α : ℱ ⟶ ℱ') (i : IsIso (whiskerLeft G.op α.val)) :
    IsIso α

Proof state:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_6, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ α.val = (sheafIso (asIso (whiskerLeft G.op α.val))).hom.val

Tactic:
apply (sheafHom_eq _ _).symm

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_6, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ IsIso α

Tactic:
convert (sheafIso (asIso (whiskerLeft G.op α.val))).isIso_hom using 1

Result:
case h.e'_5
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_6, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ α = (sheafIso (asIso (whiskerLeft G.op α.val))).hom

Proof state:
case h.e'_5
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_6, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ α = (sheafIso (asIso (whiskerLeft G.op α.val))).hom

Tactic:
ext1

Result:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_7, u_1} C
D : Type u_2
inst✝³ : Category.{u_5, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_6, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft G.op α.val)
⊢ α.val = (sheafIso (asIso (whiskerLeft G.op α.val))).hom.val
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma pairing_zero_iff :
    P.pairing i j = 0 ↔ P.pairing j i = 0

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : LinearOrderedCommRing S
inst✝⁸ : CommRing R
inst✝⁷ : Algebra S R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝¹ : FaithfulSMul S R
inst✝ : NoZeroDivisors R
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0

Tactic:
rw [← apply_root_root_zero_iff B, ← B.symm.eq, RingHom.id_apply, apply_root_root_zero_iff]

Result:
no goals
-- Mathlib/Data/ZMod/Factorial.lean
theorem cast_descFactorial {n p : ℕ} (h : n ≤ p) :
    (descFactorial (p - 1) n : ZMod p) = (-1) ^ n * n !

Proof state:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = ∏ a ∈ range n, -1 * ↑(a + 1)

Tactic:
refine prod_congr rfl ?_

Result:
n p : ℕ
h : n ≤ p
⊢ ∀ x ∈ range n, ↑(p - 1 - x) = -1 * ↑(x + 1)

Proof state:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ n * ∏ i ∈ range n, ↑(i + 1)

Tactic:
nth_rw 2 [← card_range n]

Result:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ #(range n) * ∏ i ∈ range n, ↑(i + 1)

Proof state:
n p : ℕ
h : n ≤ p
⊢ ↑(∏ i ∈ range n, (p - 1 - i)) = (-1) ^ n * ↑(∏ x ∈ range n, (x + 1))

Tactic:
simp only [cast_prod]

Result:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ n * ∏ i ∈ range n, ↑(i + 1)

Proof state:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ ↑(p - 1 - x) = -1 * ↑(x + 1)

Tactic:
rw [← tsub_add_eq_tsub_tsub_swap,
  Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
  CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
  mul_one, add_comm]

Result:
no goals

Proof state:
n p : ℕ
h : n ≤ p
⊢ ↑((p - 1).descFactorial n) = (-1) ^ n * ↑n !

Tactic:
rw [descFactorial_eq_prod_range, ← prod_range_add_one_eq_factorial]

Result:
n p : ℕ
h : n ≤ p
⊢ ↑(∏ i ∈ range n, (p - 1 - i)) = (-1) ^ n * ↑(∏ x ∈ range n, (x + 1))

Proof state:
n p : ℕ
h : n ≤ p
⊢ ∀ x ∈ range n, ↑(p - 1 - x) = -1 * ↑(x + 1)

Tactic:
intro x hx

Result:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ ↑(p - 1 - x) = -1 * ↑(x + 1)

Proof state:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = (-1) ^ #(range n) * ∏ i ∈ range n, ↑(i + 1)

Tactic:
rw [pow_card_mul_prod]

Result:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, ↑(p - 1 - i) = ∏ a ∈ range n, -1 * ↑(a + 1)
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem reverse_apply (x : CliffordAlgebra (0 : QuadraticForm R Unit)) :
    reverse (R := R) x = x

Proof state:
case add
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse (x₁ + x₂) = x₁ + x₂

Tactic:
rw [reverse.map_add, hx₁, hx₂]

Result:
no goals

Proof state:
case mul
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse (x₁ * x₂) = x₁ * x₂

Tactic:
rw [reverse.map_mul, mul_comm, hx₁, hx₂]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x : CliffordAlgebra 0
⊢ reverse x = x

Tactic:
induction x using CliffordAlgebra.induction with
| algebraMap r => exact reverse.commutes _
| ι x => rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]
| mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
| add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]

Result:
no goals

Proof state:
case ι
R : Type u_1
inst✝ : CommRing R
x : Unit
⊢ reverse ((ι 0) x) = (ι 0) x

Tactic:
rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]

Result:
no goals

Proof state:
case algebraMap
R : Type u_1
inst✝ : CommRing R
r : R
⊢ reverse ((algebraMap R (CliffordAlgebra 0)) r) = (algebraMap R (CliffordAlgebra 0)) r

Tactic:
exact reverse.commutes _

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Odd.const_smul [Monoid β] [AddGroup γ] [DistribMulAction β γ] (hg : g.Odd) (r : β) :
    (r • g).Odd

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hg : Function.Odd g
r : β
a : α
⊢ (r • g) (-a) = -(r • g) a

Tactic:
simp only [Pi.smul_apply, hg a, smul_neg]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hg : Function.Odd g
r : β
⊢ Function.Odd (r • g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hg : Function.Odd g
r : β
a : α
⊢ (r • g) (-a) = -(r • g) a
-- Mathlib/FieldTheory/Perfect.lean
theorem iterateFrobeniusEquiv_eq_pow : iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n :=
  DFunLike.ext' <| show _ = ⇑(RingAut.toPerm _ _) by
    rw [map_pow, Equiv.Perm.coe_pow]; exact (pow_iterate p n).symm

Proof state:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = (⇑((RingAut.toPerm R) (frobeniusEquiv R p)))^[n]

Tactic:
exact (pow_iterate p n).symm

Result:
no goals

Proof state:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = ⇑((RingAut.toPerm R) (frobeniusEquiv R p ^ n))

Tactic:
rw [map_pow, Equiv.Perm.coe_pow]

Result:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = (⇑((RingAut.toPerm R) (frobeniusEquiv R p)))^[n]
-- Mathlib/Probability/Distributions/Uniform.lean
theorem support_uniformOfFintype (α : Type*) [Fintype α] [Nonempty α] :
    (uniformOfFintype α).support = ⊤ :=
  Set.ext fun x => by simp [mem_support_iff]

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nonempty α
x : α
⊢ x ∈ (uniformOfFintype α).support ↔ x ∈ ⊤

Tactic:
simp [mem_support_iff]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
protected lemma one_ne_zero : (1 : ℤ) ≠ 0

Proof state:
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem?_zipIdx :
    ∀ (l : List α) n m, (zipIdx l n)[m]? = l[m]?.map fun a => (a, n + m)
  | [], _, _ => rfl
  | _ :: _, _, 0 => by simp
  | _ :: l, n, m + 1 => by
    simp only [zipIdx_cons, getElem?_cons_succ]
    exact (getElem?_zipIdx l (n + 1) m).trans <| by rw [Nat.add_right_comm]; rfl

Proof state:
α : Type u_1
head✝ : α
l : List α
n m : Nat
⊢ Option.map (fun a => (a, n + m + 1)) l[m]? = Option.map (fun a => (a, n + (m + 1))) l[m]?

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
head✝ : α
l : List α
n m : Nat
⊢ (l.zipIdx (n + 1))[m]? = Option.map (fun a => (a, n + (m + 1))) l[m]?

Tactic:
exact (getElem?_zipIdx l (n + 1) m).trans <| by rw [Nat.add_right_comm]; rfl

Result:
no goals

Proof state:
α : Type u_1
head✝ : α
l : List α
n m : Nat
⊢ Option.map (fun a => (a, n + 1 + m)) l[m]? = Option.map (fun a => (a, n + (m + 1))) l[m]?

Tactic:
rw [Nat.add_right_comm]

Result:
α : Type u_1
head✝ : α
l : List α
n m : Nat
⊢ Option.map (fun a => (a, n + m + 1)) l[m]? = Option.map (fun a => (a, n + (m + 1))) l[m]?

Proof state:
α : Type u_1
head✝ : α
tail✝ : List α
x✝ : Nat
⊢ ((head✝ :: tail✝).zipIdx x✝)[0]? = Option.map (fun a => (a, x✝ + 0)) (head✝ :: tail✝)[0]?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
head✝ : α
l : List α
n m : Nat
⊢ ((head✝ :: l).zipIdx n)[m + 1]? = Option.map (fun a => (a, n + (m + 1))) (head✝ :: l)[m + 1]?

Tactic:
simp only [zipIdx_cons, getElem?_cons_succ]

Result:
α : Type u_1
head✝ : α
l : List α
n m : Nat
⊢ (l.zipIdx (n + 1))[m]? = Option.map (fun a => (a, n + (m + 1))) l[m]?
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_smul (r : R) (q : ℍ[R]) : normSq (r • q) = r ^ 2 * normSq q

Proof state:
R : Type u_3
inst✝ : CommRing R
r : R
q : ℍ[R]
⊢ normSq (r • q) = r ^ 2 * normSq q

Tactic:
simp only [normSq_def', smul_re, smul_imI, smul_imJ, smul_imK, mul_pow, mul_add, smul_eq_mul]

Result:
no goals