harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ZMod/Basic.lean
theorem ringHom_map_cast [Ring R] (f : R →+* ZMod n) (k : ZMod n) : f (cast k) = k

Proof state:
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f ↑k.val = k

Tactic:
rw [map_natCast, natCast_zmod_val]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod 0
k : ZMod 0
⊢ f k.cast = k

Tactic:
dsimp [ZMod, ZMod.cast] at f k ⊢

Result:
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ℤ
k : ℤ
⊢ f ↑k = k

Proof state:
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k

Tactic:
dsimp [ZMod.cast]

Result:
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f ↑k.val = k

Proof state:
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ℤ
k : ℤ
⊢ f ↑k = k

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod n
k : ZMod n
⊢ f k.cast = k

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod 0
k : ZMod 0
⊢ f k.cast = k

case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_isSome_getValue? {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
    containsKey a l = (getValue? a l).isSome

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
⊢ containsKey a l = (getValue? a l).isSome

Tactic:
simp [containsKey_eq_isSome_getEntry?, getValue?_eq_getEntry?]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_union' (hst : Disjoint s t) (hs : (s ∩ mulSupport f).Finite)
    (ht : (t ∩ mulSupport f).Finite) : ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
  mul_one]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem foldr_max_of_ne_nil (h : l ≠ []) : ↑(l.foldr max ⊥) = l.maximum

Proof state:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ ↑hd ⊔ ↑(foldr max ⊥ tl) = ↑hd ⊔ tl.maximum

Tactic:
simp [IH h]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : [] ≠ []
⊢ ↑(foldr max ⊥ []) = [].maximum

Tactic:
contradiction

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = (hd :: tl).maximum

Tactic:
rw [maximum_cons, foldr, WithBot.coe_max]

Result:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ ↑hd ⊔ ↑(foldr max ⊥ tl) = ↑hd ⊔ tl.maximum

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : l ≠ []
⊢ ↑(foldr max ⊥ l) = l.maximum

Tactic:
induction' l with hd tl IH

Result:
case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : [] ≠ []
⊢ ↑(foldr max ⊥ []) = [].maximum

case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = (hd :: tl).maximum

Proof state:
case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h : hd :: tl ≠ []
⊢ ↑hd ⊔ ↑(foldr max ⊥ tl) = ↑hd ⊔ tl.maximum

Tactic:
by_cases h : tl = []

Result:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : tl = []
⊢ ↑hd ⊔ ↑(foldr max ⊥ tl) = ↑hd ⊔ tl.maximum

case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ ↑hd ⊔ ↑(foldr max ⊥ tl) = ↑hd ⊔ tl.maximum

Proof state:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : tl = []
⊢ ↑hd ⊔ ↑(foldr max ⊥ tl) = ↑hd ⊔ tl.maximum

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem MeasurableSet.tProd (l : List δ) {s : ∀ i, Set (π i)} (hs : ∀ i, MeasurableSet (s i)) :
    MeasurableSet (Set.tprod l s)

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
l : List δ
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod l s)

Tactic:
induction' l with i l ih

Result:
case nil
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod [] s)

case cons
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)

Proof state:
case nil
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod [] s)

Tactic:
exact MeasurableSet.univ

Result:
no goals

Proof state:
case cons
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
s : (i : δ) → Set (π i)
hs : ∀ (i : δ), MeasurableSet (s i)
i : δ
l : List δ
ih : MeasurableSet (Set.tprod l s)
⊢ MeasurableSet (Set.tprod (i :: l) s)

Tactic:
exact (hs i).prod ih

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem coeff_hsum_mul {β : Type*} (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) (g : Γ) :
    (mul s t).hsum.coeff g = ∑ gh ∈ addAntidiagonal s.isPWO_iUnion_support
      t.isPWO_iUnion_support g, (s.hsum.coeff gh.1) * (t.hsum.coeff gh.2)

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
β : Type u_7
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.smul t).hsum.coeff g = ∑ x ∈ addAntidiagonal ⋯ ⋯ g, s.hsum.coeff x.1 • t.hsum.coeff x.2

Tactic:
exact coeff_smul s t g

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
β : Type u_7
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.mul t).hsum.coeff g = ∑ gh ∈ addAntidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 * t.hsum.coeff gh.2

Tactic:
simp_rw [← smul_eq_mul, mul_eq_smul]

Result:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
β : Type u_7
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.smul t).hsum.coeff g = ∑ x ∈ addAntidiagonal ⋯ ⋯ g, s.hsum.coeff x.1 • t.hsum.coeff x.2
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
/-- Alternative formulation of `covariant_sequence_exact₂` -/
lemma covariant_sequence_exact₂' (n : ℕ) :
    (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X (add_zero n)))
      (AddCommGrp.ofHom ((mk₀ S.g).postcomp X (add_zero n))) (by
        ext x
        dsimp
        simp only [comp_assoc_of_third_deg_zero, mk₀_comp_mk₀, ShortComplex.zero, mk₀_zero,
          comp_zero])).Exact

Proof state:
case comm₁₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).g)
⊢ (ConcreteCategory.hom
          (ShortComplex.mk
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂)
              ⋯).f).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).f)

case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).f)
    ⇑(ConcreteCategory.hom
        (ShortComplex.mk
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
            (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂) ⋯).g)
⊢ (ConcreteCategory.hom
          (ShortComplex.mk
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₁)
              (((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n).map hS.singleTriangle.mor₂)
              ⋯).g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (ConcreteCategory.hom
        (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).g)

Tactic:
all_goals ext x; apply hom_comp_singleFunctor_map_shift (C := C)

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepFun_iff_measure_inter_preimage_eq_mul {ι : Type*} {β : ι → Type*}
    (m : ∀ x, MeasurableSpace (β x)) (f : ∀ i, Ω → β i) :
    iIndepFun m f κ μ ↔
      ∀ (S : Finset ι) {sets : ∀ i : ι, Set (β i)} (_H : ∀ i, i ∈ S → MeasurableSet[m i] (sets i)),
        ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, (f i) ⁻¹' (sets i)) = ∏ i ∈ S, κ a ((f i) ⁻¹' (sets i))

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
⊢ ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i

Tactic:
intro i hi_mem

Result:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x => {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i => if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
⊢ setsΩ i = f i ⁻¹' setsβ i
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_succ_eval (n p : ℕ) : (bernoulli p.succ).eval (n : ℚ) =
    _root_.bernoulli p.succ + (p + 1 : ℚ) * ∑ k ∈ range n, (k : ℚ) ^ p

Proof state:
case h
n p : ℕ
⊢ eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ = (↑p + 1) * ∑ k ∈ range n, ↑k ^ p

Tactic:
rw [sum_range_pow_eq_bernoulli_sub]

Result:
no goals

Proof state:
n p : ℕ
⊢ eval (↑n) (bernoulli p.succ) = _root_.bernoulli p.succ + (↑p + 1) * ∑ k ∈ range n, ↑k ^ p

Tactic:
apply eq_add_of_sub_eq'

Result:
case h
n p : ℕ
⊢ eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ = (↑p + 1) * ∑ k ∈ range n, ↑k ^ p
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
/-- A limit (over a general filter) of a.e.-measurable `ℝ≥0∞` valued functions is
a.e.-measurable. -/
lemma aemeasurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞}
    {μ : Measure α} (u : Filter ι) [NeBot u] [IsCountablyGenerated u]
    (hf : ∀ i, AEMeasurable (f i) μ) (hlim : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))) :
    AEMeasurable g μ

Proof state:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x
⊢ AEMeasurable g μ

Tactic:
set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some

Result:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x
aeSeqLim : α → ℝ≥0∞ := fun x => if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ AEMeasurable g μ
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 :=
  Polynomial.ext fun m => by
    rw [coeff_trunc, coeff_one, Polynomial.coeff_one]
    split_ifs with h _ h'
    · rfl
    · rfl
    · subst h'; simp at h
    · rfl

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
h : ¬0 < n + 1
⊢ 0 = 1

Tactic:
simp at h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ (if m < n + 1 then if m = 0 then 1 else 0 else 0) = if m = 0 then 1 else 0

Tactic:
split_ifs with h _ h'

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : m < n + 1
_ : m = 0
⊢ 1 = 1

case neg
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : m < n + 1
_ : ¬m = 0
⊢ 0 = 0

case pos
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : ¬m < n + 1
h' : m = 0
⊢ 0 = 1

case neg
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : ¬m < n + 1
h' : ¬m = 0
⊢ 0 = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : m < n + 1
_ : m = 0
⊢ 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : ¬m < n + 1
h' : m = 0
⊢ 0 = 1

Tactic:
subst h'

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
h : ¬0 < n + 1
⊢ 0 = 1

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : m < n + 1
_ : ¬m = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ (trunc (n + 1) 1).coeff m = Polynomial.coeff 1 m

Tactic:
rw [coeff_trunc, coeff_one, Polynomial.coeff_one]

Result:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ (if m < n + 1 then if m = 0 then 1 else 0 else 0) = if m = 0 then 1 else 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n m : ℕ
h : ¬m < n + 1
h' : ¬m = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalize_normalized_factor {a : α} :
    ∀ x : α, x ∈ normalizedFactors a → normalize x = x

Proof state:
case neg.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
y : α
left✝ : y ∈ Classical.choose ⋯
hx : normalize y ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)
⊢ normalize (normalize y) = normalize y

Tactic:
apply normalize_idem

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map (⇑normalize) (if h : a = 0 then 0 else Classical.choose ⋯), normalize x = x

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ ∀ x ∈ Multiset.map (fun x => normalize x) 0, normalize x = x

case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯), normalize x = x

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ ∀ x ∈ Multiset.map (fun x => normalize x) 0, normalize x = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ normalizedFactors a, normalize x = x

Tactic:
rw [normalizedFactors, factors]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map (⇑normalize) (if h : a = 0 then 0 else Classical.choose ⋯), normalize x = x

Proof state:
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯), normalize x = x

Tactic:
intro x hx

Result:
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)
⊢ normalize x = x

Proof state:
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
x : α
hx : x ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)
⊢ normalize x = x

Tactic:
obtain ⟨y, _, rfl⟩ := Multiset.mem_map.1 hx

Result:
case neg.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
y : α
left✝ : y ∈ Classical.choose ⋯
hx : normalize y ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)
⊢ normalize (normalize y) = normalize y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat m n = -[k+1]

Proof state:
m n k : Nat
h : n - m = k.succ
⊢ subNatNat m n = -[k+1]

Tactic:
rw [subNatNat, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem det_pos [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : 0 < det M

Proof state:
case h0
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
i : n
a✝ : i ∈ Finset.univ
⊢ 0 < ↑(⋯.eigenvalues i)

Tactic:
simpa using hM.eigenvalues_pos i

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ 0 < M.det

Tactic:
rw [hM.isHermitian.det_eq_prod_eigenvalues]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ 0 < ∏ i : n, ↑(⋯.eigenvalues i)

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ 0 < ∏ i : n, ↑(⋯.eigenvalues i)

Tactic:
apply Finset.prod_pos

Result:
case h0
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ ∀ i ∈ Finset.univ, 0 < ↑(⋯.eigenvalues i)

Proof state:
case h0
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ ∀ i ∈ Finset.univ, 0 < ↑(⋯.eigenvalues i)

Tactic:
intro i _

Result:
case h0
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
i : n
a✝ : i ∈ Finset.univ
⊢ 0 < ↑(⋯.eigenvalues i)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_add_right' (a b : α) : toIocDiv hp (a + p) b = toIocDiv hp a b - 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (a + p) b = toIocDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIocDiv_add_zsmul' hp a b 1

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval_assoc {τ} (f : σ → MvPolynomial τ R) (g : τ → R) (p : MvPolynomial σ R) :
    eval (eval g ∘ f) p = eval g (eval₂ C f p)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval (⇑(eval g) ∘ f)) p = eval₂ ((eval g).comp C) (⇑(eval g) ∘ f) p

Tactic:
unfold eval

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval₂Hom (RingHom.id R) (⇑(eval₂Hom (RingHom.id R) g) ∘ f)) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (⇑(eval₂Hom (RingHom.id R) g) ∘ f) p

Proof state:
case e_f.a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
a : R
⊢ (RingHom.id R) a = ((eval₂Hom (RingHom.id R) g).comp C) a

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval (⇑(eval g) ∘ f)) p = (eval g) (eval₂ C f p)

Tactic:
rw [eval₂_comp_left (eval g)]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval (⇑(eval g) ∘ f)) p = eval₂ ((eval g).comp C) (⇑(eval g) ∘ f) p

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval₂Hom (RingHom.id R) (⇑(eval₂Hom (RingHom.id R) g) ∘ f)) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (⇑(eval₂Hom (RingHom.id R) g) ∘ f) p

Tactic:
simp only [coe_eval₂Hom]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ eval₂ (RingHom.id R) (eval₂ (RingHom.id R) g ∘ f) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (eval₂ (RingHom.id R) g ∘ f) p

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ eval₂ (RingHom.id R) (eval₂ (RingHom.id R) g ∘ f) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (eval₂ (RingHom.id R) g ∘ f) p

Tactic:
congr with a

Result:
case e_f.a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
a : R
⊢ (RingHom.id R) a = ((eval₂Hom (RingHom.id R) g).comp C) a
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3

Proof state:
case mk
toBitVec✝ : BitVec 16
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3

Tactic:
simp_arith [UInt16.toNat, BitVec.toNat]

Result:
no goals

Proof state:
a : UInt16
⊢ sizeOf a = a.toNat + 3

Tactic:
cases a

Result:
case mk
toBitVec✝ : BitVec 16
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3