harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Identities.lean
theorem poly_binom_aux2 (f : R[X]) (x y : R) :
    f.eval (x + y) =
      f.sum fun e a => a * (x ^ e + e * x ^ (e - 1) * y + (polyBinomAux1 x y e a).val * y ^ 2)

Proof state:
case e_f.h.h
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
n : ℕ
z : R
⊢ (RingHom.id R) z * (x + y) ^ n = z * (x ^ n + ↑n * x ^ (n - 1) * y + ↑(Polynomial.polyBinomAux1 x y n z) * y ^ 2)

Tactic:
apply (polyBinomAux1 x y _ _).property

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) (x + y) f =
    f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)

Tactic:
rw [eval₂_eq_sum]

Result:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (f.sum fun e a => (RingHom.id R) a * (x + y) ^ e) =
    f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f = f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)

Tactic:
unfold eval

Result:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval₂ (RingHom.id R) (x + y) f =
    f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (f.sum fun e a => (RingHom.id R) a * (x + y) ^ e) =
    f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)

Tactic:
congr with (n z)

Result:
case e_f.h.h
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
n : ℕ
z : R
⊢ (RingHom.id R) z * (x + y) ^ n = z * (x ^ n + ↑n * x ^ (n - 1) * y + ↑(Polynomial.polyBinomAux1 x y n z) * y ^ 2)
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_expand (q : ℕ) [hF : ExpChar F q] {n : ℕ} :
    (expand F (q ^ n) f).natSepDegree = f.natSepDegree

Proof state:
case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
this : Fact (Nat.Prime q)
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
classical
simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand,
  Fintype.card_coe] using Fintype.card_eq.2
    ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
q : ℕ
hF : ExpChar F q
n : ℕ
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
obtain - | hprime := hF

Result:
case zero
F : Type u
inst✝¹ : Field F
f : F[X]
n : ℕ
inst✝ : CharZero F
⊢ ((expand F (1 ^ n)) f).natSepDegree = f.natSepDegree

case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Proof state:
case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
this : Fact (Nat.Prime q)
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand,
  Fintype.card_coe] using Fintype.card_eq.2
    ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩

Result:
no goals

Proof state:
case zero
F : Type u
inst✝¹ : Field F
f : F[X]
n : ℕ
inst✝ : CharZero F
⊢ ((expand F (1 ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
simp only [one_pow, expand_one]

Result:
no goals

Proof state:
case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
haveI := Fact.mk hprime

Result:
case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
this : Fact (Nat.Prime q)
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem compRight_id (B : BilinForm R M) : B.compRight LinearMap.id = B

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
⊢ B.compRight id = B

Tactic:
ext

Result:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.compRight id) x✝) y✝ = (B x✝) y✝

Proof state:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.compRight id) x✝) y✝ = (B x✝) y✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finAddFlip_apply_mk_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
    finAddFlip (⟨k, h₂⟩ : Fin (m + n)) = ⟨k - m, by omega⟩

Proof state:
case h.e'_2.h.e'_6.h.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(Fin.natAdd m ⟨k - m, ⋯⟩)

Tactic:
simp [Nat.add_sub_cancel' h₁]

Result:
no goals

Proof state:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ finAddFlip ⟨k, h₂⟩ = ⟨k - m, ⋯⟩

Tactic:
convert @finAddFlip_apply_natAdd n ⟨k - m, by omega⟩ m

Result:
case h.e'_2.h.e'_6.h.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(Fin.natAdd m ⟨k - m, ⋯⟩)

Proof state:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n + m

Tactic:
omega

Result:
no goals

Proof state:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem SupPrime.supIrred : SupPrime a → SupIrred a :=
  And.imp_right fun h b c ha => by simpa [← ha] using h ha.ge

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
h : ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
b c : α
ha : b ⊔ c = a
⊢ b = a ∨ c = a

Tactic:
simpa [← ha] using h ha.ge

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem IsLocalization.isMaximal_of_isMaximal_disjoint
    [IsJacobsonRing R] (I : Ideal R) (hI : I.IsMaximal)
    (hy : y ∉ I) : (I.map (algebraMap R S)).IsMaximal

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ I.IsMaximal ∧ y ∉ I

Tactic:
exact ⟨hI, hy⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ (Ideal.map (algebraMap R S) I).IsMaximal

Tactic:
rw [isMaximal_iff_isMaximal_disjoint S y,
  comap_map_of_isPrime_disjoint (powers y) S I (IsMaximal.isPrime hI)
    ((disjoint_powers_iff_not_mem y hI.isPrime.isRadical).2 hy)]

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
y : R
inst✝² : Algebra R S
inst✝¹ : Away y S
inst✝ : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ I.IsMaximal ∧ y ∉ I
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem ofReal_condCDF_ae_eq (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (r : ℚ) :
    (fun a ↦ ENNReal.ofReal (condCDF ρ a r)) =ᵐ[ρ.fst] preCDF ρ r

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
a : α
ha : ↑(condCDF ρ a) ↑r = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a ≠ ⊤

Tactic:
exact ((ha_le_one r).trans_lt ENNReal.one_lt_top).ne

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
a : α
ha : ↑(condCDF ρ a) ↑r = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ ENNReal.ofReal (↑(condCDF ρ a) ↑r) = preCDF ρ r a

Tactic:
rw [ha, ENNReal.ofReal_toReal]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
a : α
ha : ↑(condCDF ρ a) ↑r = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a ≠ ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a => ENNReal.ofReal (↑(condCDF ρ a) ↑r)) =ᶠ[ae ρ.fst] preCDF ρ r

Tactic:
filter_upwards [condCDF_ae_eq ρ r, preCDF_le_one ρ] with a ha ha_le_one

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
a : α
ha : ↑(condCDF ρ a) ↑r = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ ENNReal.ofReal (↑(condCDF ρ a) ↑r) = preCDF ρ r a
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_neg_iff : a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
⊢ a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
simp [division_def, mul_neg_iff]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infiniteNeg_add_not_infinitePos {x y : ℝ*} :
    InfiniteNeg x → ¬InfinitePos y → InfiniteNeg (x + y)

Proof state:
x y : ℝ*
⊢ x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]

Result:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos

Proof state:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos

Tactic:
exact infinitePos_add_not_infiniteNeg

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_le_one_iff : b * a⁻¹ ≤ 1 ↔ b ≤ a :=
  _root_.trans mul_inv_le_iff_le_mul <| by rw [one_mul]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ b ≤ 1 * a ↔ b ≤ a

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem Measurable.ennreal_tsum' {ι} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) :
    Measurable (∑' i, f i)

Proof state:
case h.e'_5.h
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
x : α
⊢ (∑' (i : ι), f i) x = ∑' (i : ι), f i x

Tactic:
exact tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (∑' (i : ι), f i)

Tactic:
convert Measurable.ennreal_tsum h with x

Result:
case h.e'_5.h
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
x : α
⊢ (∑' (i : ι), f i) x = ∑' (i : ι), f i x
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLinAlgEquiv_toMatrixAlgEquiv (f : M₁ →ₗ[R] M₁) :
    Matrix.toLinAlgEquiv v₁ (LinearMap.toMatrixAlgEquiv v₁ f) = f

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
⊢ (toLinAlgEquiv v₁) ((toMatrixAlgEquiv v₁) f) = f

Tactic:
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem natCast_coeff_zero {n : ℕ} {R : Type*} [Semiring R] : (n : R[X]).coeff 0 = n

Proof state:
n : ℕ
R : Type u_1
inst✝ : Semiring R
⊢ (↑n).coeff 0 = ↑n

Tactic:
simp only [coeff_natCast_ite, ite_true]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem subgraphOfAdj_symm {v w : V} (hvw : G.Adj v w) :
    G.subgraphOfAdj hvw.symm = G.subgraphOfAdj hvw

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw

Tactic:
ext <;> simp [or_comm, and_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJNe0Or1728_c₄ : (ofJNe0Or1728 j).c₄ = j * (j - 1728) ^ 3

Proof state:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ ((j - 1728) ^ 2 + 4 * 0) ^ 2 - 24 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) = j * (j - 1728) ^ 3

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ (ofJNe0Or1728 j).c₄ = j * (j - 1728) ^ 3

Tactic:
simp only [ofJNe0Or1728, c₄, b₂, b₄]

Result:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ ((j - 1728) ^ 2 + 4 * 0) ^ 2 - 24 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) = j * (j - 1728) ^ 3
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@[reassoc]
lemma r_f (s : S.Splitting) : s.r ≫ S.f = 𝟙 _ - S.g ≫ s.s

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ s.r ≫ S.f = 𝟙 S.X₂ - S.g ≫ s.s

Tactic:
rw [← s.id, add_sub_cancel_right]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem negAt_apply_abs_isReal (x : mixedSpace K) (w : {w // IsReal w}) :
    |(negAt s x).1 w| = |x.1 w|

Proof state:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
⊢ |((negAt s) x).1 w| = |x.1 w|

Tactic:
by_cases hw : w ∈ s <;> simp [hw]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
@[simp]
lemma comp_assoc [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W X Z]
    [HasSmallLocalizedHom.{w} W X T] [HasSmallLocalizedHom.{w} W Y Z]
    [HasSmallLocalizedHom.{w} W Y T] [HasSmallLocalizedHom.{w} W Z T]
    (α : SmallHom.{w} W X Y) (β : SmallHom.{w} W Y Z) (γ : SmallHom.{w} W Z T) :
    (α.comp β).comp γ = α.comp (β.comp γ)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z T : C
inst✝⁵ : HasSmallLocalizedHom W X Y
inst✝⁴ : HasSmallLocalizedHom W X Z
inst✝³ : HasSmallLocalizedHom W X T
inst✝² : HasSmallLocalizedHom W Y Z
inst✝¹ : HasSmallLocalizedHom W Y T
inst✝ : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ (α.comp β).comp γ = α.comp (β.comp γ)

Tactic:
apply (equiv W W.Q).injective

Result:
case a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z T : C
inst✝⁵ : HasSmallLocalizedHom W X Y
inst✝⁴ : HasSmallLocalizedHom W X Z
inst✝³ : HasSmallLocalizedHom W X T
inst✝² : HasSmallLocalizedHom W Y Z
inst✝¹ : HasSmallLocalizedHom W Y T
inst✝ : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ (equiv W W.Q) ((α.comp β).comp γ) = (equiv W W.Q) (α.comp (β.comp γ))

Proof state:
case a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z T : C
inst✝⁵ : HasSmallLocalizedHom W X Y
inst✝⁴ : HasSmallLocalizedHom W X Z
inst✝³ : HasSmallLocalizedHom W X T
inst✝² : HasSmallLocalizedHom W Y Z
inst✝¹ : HasSmallLocalizedHom W Y T
inst✝ : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ (equiv W W.Q) ((α.comp β).comp γ) = (equiv W W.Q) (α.comp (β.comp γ))

Tactic:
simp only [equiv_comp, assoc]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Basic.lean
theorem any_iff {t : RBNode α} : t.any p ↔ t.Any (p ·)

Proof state:
α : Type u_1
p : α → Bool
t : RBNode α
⊢ any p t = true ↔ Any (fun x => p x = true) t

Tactic:
induction t <;> simp [*, any, Any, or_assoc]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem powerlt_zero {a : Cardinal} : a ^< 0 = 0

Proof state:
a : Cardinal.{u_1}
⊢ a ^< 0 = 0

Tactic:
convert Cardinal.iSup_of_empty _

Result:
case convert_3
a : Cardinal.{u_1}
⊢ IsEmpty ↑(Iio 0)

Proof state:
case convert_3
a : Cardinal.{u_1}
⊢ IsEmpty ↑(Iio 0)

Tactic:
exact Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr (Cardinal.zero_le x).not_lt

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRight_id {f g : C}
    {η : f ⟶ g} {η₁ : f ⟶ g ⊗ 𝟙_ C} {η₂ : f ⊗ 𝟙_ C ⟶ g ⊗ 𝟙_ C}
    (e_η₁ : η ≫ (ρ_ _).inv = η₁) (e_η₂ : (ρ_ _).hom ≫ η₁ = η₂) :
    η ▷ 𝟙_ C = η₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
η₁ : f ⟶ g ⊗ 𝟙_ C
η₂ : f ⊗ 𝟙_ C ⟶ g ⊗ 𝟙_ C
e_η₁ : η ≫ (ρ_ g).inv = η₁
e_η₂ : (ρ_ f).hom ≫ η₁ = η₂
⊢ η ▷ 𝟙_ C = η₂

Tactic:
simp [e_η₁, e_η₂]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
/-- Expression for `hurwitzZeta a 1` as a limit. (Mathematically `hurwitzZeta a 1` is
undefined, but our construction assigns some value to it; this lemma is mostly of interest for
determining what that value is). -/
lemma tendsto_hurwitzZeta_sub_one_div_nhds_one (a : UnitAddCircle) :
    Tendsto (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) (𝓝 1) (𝓝 (hurwitzZeta a 1))

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) (𝓝 1)
    (𝓝 (hurwitzZetaEven a 1 + hurwitzZetaOdd a 1))

Tactic:
refine (tendsto_hurwitzZetaEven_sub_one_div_nhds_one a).add
  (differentiable_hurwitzZetaOdd a 1).continuousAt.tendsto

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZeta a 1))

Tactic:
simp only [hurwitzZeta, add_sub_right_comm]

Result:
a : UnitAddCircle
⊢ Tendsto (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) (𝓝 1)
    (𝓝 (hurwitzZetaEven a 1 + hurwitzZetaOdd a 1))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_eq_self {f : α → α} {n} {l : List α} (h : l.length ≤ n) :
    l.modify f n = l

Proof state:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
⊢ ∀ (i : Nat) (h₁ : i < (modify f n l).length) (h₂ : i < l.length), (modify f n l)[i] = l[i]

Tactic:
intro m h₁ h₂

Result:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < l.length
⊢ (modify f n l)[m] = l[m]

Proof state:
case hl
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
⊢ (modify f n l).length = l.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
⊢ modify f n l = l

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
⊢ (modify f n l).length = l.length

case h
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
⊢ ∀ (i : Nat) (h₁ : i < (modify f n l).length) (h₂ : i < l.length), (modify f n l)[i] = l[i]

Proof state:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < l.length
⊢ (modify f n l)[m] = l[m]

Tactic:
simp only [getElem_modify, ite_eq_right_iff]

Result:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < l.length
⊢ n = m → f l[m] = l[m]

Proof state:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
h : l.length ≤ n
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < l.length
⊢ n = m → f l[m] = l[m]

Tactic:
intro h

Result:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
h✝ : l.length ≤ n
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < l.length
h : n = m
⊢ f l[m] = l[m]

Proof state:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
h✝ : l.length ≤ n
m : Nat
h₁ : m < (modify f n l).length
h₂ : m < l.length
h : n = m
⊢ f l[m] = l[m]

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem exists_of_mem_mapIdx {b : β} {l : Array α}
    (h : b ∈ mapIdx f l) : ∃ (i : Nat) (h : i < l.size), f i l[i] = b

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
h : b ∈ l.mapFinIdx fun i a x => f i a
⊢ ∃ i h, f i l[i] = b

Tactic:
simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Tactic:
rw [mapIdx_eq_mapFinIdx] at h

Result:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : Array α
h : b ∈ l.mapFinIdx fun i a x => f i a
⊢ ∃ i h, f i l[i] = b
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccEquivLast_last : finSuccEquivLast (Fin.last n) = none

Proof state:
n : ℕ
⊢ finSuccEquivLast (Fin.last n) = none

Tactic:
simp [finSuccEquivLast]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_pow :
    (expand R (p ^ n) f).roots = p ^ n • f.roots.map (iterateFrobeniusEquiv R p n).symm

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ p ^ n * (filter (fun x => r ^ p ^ n = x) f.roots).card =
    p ^ n * (filter (fun a => r = (iterateFrobeniusEquiv R p n).symm a) f.roots).card

Tactic:
congr

Result:
case e_a.e_a.e_p
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ (fun x => r ^ p ^ n = x) = fun a => r = (iterateFrobeniusEquiv R p n).symm a

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ count r ((expand R (p ^ n)) f).roots = count r (p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots)

Tactic:
rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
  count_eq_card_filter_eq]

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ p ^ n * (filter (fun x => r ^ p ^ n = x) f.roots).card =
    p ^ n * (filter (fun a => r = (iterateFrobeniusEquiv R p n).symm a) f.roots).card

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ ((expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots

Tactic:
classical
refine ext' fun r ↦ ?_
rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
  count_eq_card_filter_eq]; congr; ext
exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ ((expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots

Tactic:
refine ext' fun r ↦ ?_

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ count r ((expand R (p ^ n)) f).roots = count r (p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots)

Proof state:
case e_a.e_a.e_p
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ (fun x => r ^ p ^ n = x) = fun a => r = (iterateFrobeniusEquiv R p n).symm a

Tactic:
ext

Result:
case e_a.e_a.e_p.h.a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r x✝ : R
⊢ r ^ p ^ n = x✝ ↔ r = (iterateFrobeniusEquiv R p n).symm x✝

Proof state:
case e_a.e_a.e_p.h.a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r x✝ : R
⊢ r ^ p ^ n = x✝ ↔ r = (iterateFrobeniusEquiv R p n).symm x✝

Tactic:
exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma δ_inl :
    δ (-1) 0 (inl φ) = Cochain.ofHom (φ ≫ inr φ)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ p + -1 = p - 1

Tactic:
omega

Result:
no goals

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ (δ (-1) 0 (inl φ)).v p p ⋯ = (Cochain.ofHom (φ ≫ inr φ)).v p p ⋯

Tactic:
simp [δ_v (-1) 0 (neg_add_cancel 1) (inl φ) p p (add_zero p) _ _ rfl rfl,
  inl_v_d φ p (p - 1) (p + 1) (by omega) (by omega)]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ p + 1 + -1 = p

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ δ (-1) 0 (inl φ) = Cochain.ofHom (φ ≫ inr φ)

Tactic:
ext p

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ (δ (-1) 0 (inl φ)).v p p ⋯ = (Cochain.ofHom (φ ≫ inr φ)).v p p ⋯