harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_congr' {f : Filter β} {p q : β → Prop} {u : β → α}
    (h : ∀ᶠ x in f, u x ≠ ⊥ → (p x ↔ q x)) : blimsup u f p = blimsup u f q

Proof state:
case e_a.h.inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
rw [hb hu]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}

Tactic:
congr with a

Result:
case e_a.h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}

Proof state:
case e_a.h.inl
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
simp [hu]

Result:
no goals

Proof state:
case e_a.h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
rcases eq_or_ne (u b) ⊥ with hu | hu

Result:
case e_a.h.inl
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

case e_a.h.inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ blimsup u f p = blimsup u f q

Tactic:
simp only [blimsup_eq]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}

Proof state:
case e_a.h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}

Tactic:
refine eventually_congr (h.mono fun b hb => ?_)

Result:
case e_a.h
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem IsTopologicalRing.of_norm {R 𝕜 : Type*} [NonUnitalNonAssocRing R] [LinearOrderedField 𝕜]
    [TopologicalSpace R] [IsTopologicalAddGroup R] (norm : R → 𝕜)
    (norm_nonneg : ∀ x, 0 ≤ norm x) (norm_mul_le : ∀ x y, norm (x * y) ≤ norm x * norm y)
    (nhds_basis : (𝓝 (0 : R)).HasBasis ((0 : 𝕜) < ·) (fun ε ↦ { x | norm x < ε })) :
    IsTopologicalRing R

Proof state:
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x✝¹ : R × R
x y : R
x✝ : (x, y) ∈ {x | norm x < 1} ×ˢ {x | norm x < ε}
hx : x ∈ {x | norm x < 1}
hy : y ∈ {x | norm x < ε}
⊢ uncurry (fun x1 x2 => x1 * x2) (x, y) ∈ {x | norm x < ε}

Tactic:
calc norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
_ < ε := (mul_le_of_le_one_left (norm_nonneg _) hx.le).trans_lt hy

Result:
no goals

Proof state:
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ ia, 0 < ia ∧ ∀ x ∈ {x | norm x < ia}, f x ∈ {x | norm x < ε}

Tactic:
rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩

Result:
case intro.intro
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
⊢ ∃ ia, 0 < ia ∧ ∀ x ∈ {x | norm x < ia}, f x ∈ {x | norm x < ε}
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem nonempty (μ : ProbabilityMeasure Ω) : Nonempty Ω

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ Nonempty Ω

Tactic:
by_contra maybe_empty

Result:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
⊢ False

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
⊢ False

Tactic:
have zero : (μ : Measure Ω) univ = 0 := by
  rw [univ_eq_empty_iff.mpr (not_nonempty_iff.mp maybe_empty), measure_empty]

Result:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : ↑μ univ = 0
⊢ False

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : ↑μ univ = 0
⊢ False

Tactic:
rw [measure_univ] at zero

Result:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : 1 = 0
⊢ False

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : 1 = 0
⊢ False

Tactic:
exact zero_ne_one zero.symm

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
⊢ ↑μ univ = 0

Tactic:
rw [univ_eq_empty_iff.mpr (not_nonempty_iff.mp maybe_empty), measure_empty]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem one_mem_div_iff : (1 : α) ∈ s / t ↔ ¬Disjoint s t

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t

Tactic:
simp [not_disjoint_iff_nonempty_inter, mem_div, div_eq_one, Set.Nonempty]

Result:
no goals
-- Mathlib/MeasureTheory/Group/LIntegral.lean
theorem lintegral_mul_right_eq_self [IsMulRightInvariant μ] (f : G → ℝ≥0∞) (g : G) :
    (∫⁻ x, f (x * g) ∂μ) = ∫⁻ x, f x ∂μ

Proof state:
case h.e'_3
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g)) μ

Tactic:
simp [map_mul_right_eq_self μ g]

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
convert (lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm using 1

Result:
case h.e'_3
G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g)) μ
-- Mathlib/Data/Finset/Insert.lean
theorem Nonempty.cons_induction {α : Type*} {p : ∀ s : Finset α, s.Nonempty → Prop}
    (singleton : ∀ a, p {a} (singleton_nonempty _))
    (cons : ∀ a s (h : a ∉ s) (hs), p s hs → p (Finset.cons a s h) (cons_nonempty h))
    {s : Finset α} (hs : s.Nonempty) : p s hs

Proof state:
case cons
α : Type u_3
p : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), p {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), p t hs
hs : (Finset.cons a t ha).Nonempty
⊢ p (Finset.cons a t ha) hs

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Result:
case cons.inl
α : Type u_3
p : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), p {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : ∅.Nonempty), p ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ p (Finset.cons a ∅ ha) hs

case cons.inr
α : Type u_3
p : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), p {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), p t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ p (Finset.cons a t ha) hs

Proof state:
case cons.inl
α : Type u_3
p : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), p {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : ∅.Nonempty), p ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ p (Finset.cons a ∅ ha) hs

Tactic:
exact singleton a

Result:
no goals

Proof state:
case cons.inr
α : Type u_3
p : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), p {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), p t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ p (Finset.cons a t ha) hs

Tactic:
exact cons a t ha ht (h ht)

Result:
no goals

Proof state:
case empty
α : Type u_3
p : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), p {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯
hs : ∅.Nonempty
⊢ p ∅ hs

Tactic:
exact (not_nonempty_empty hs).elim

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma IsEllSequence.smul (h : IsEllSequence W) (x : R) : IsEllSequence (x • W) :=
  fun m n r => by
    linear_combination (norm := (simp only [Pi.smul_apply, smul_eq_mul]; ring1)) x ^ 4 * h m n r

Proof state:
case a.a
R : Type u
inst✝ : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
⊢ (x • W) (m + n) * (x • W) (m - n) * (x • W) r ^ 2 +
        x ^ 4 * (W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2) -
      ((x • W) (m + r) * (x • W) (m - r) * (x • W) n ^ 2 - (x • W) (n + r) * (x • W) (n - r) * (x • W) m ^ 2 +
        x ^ 4 * (W (m + n) * W (m - n) * W r ^ 2)) =
    0

Tactic:
simp only [Pi.smul_apply, smul_eq_mul]

Result:
case a.a
R : Type u
inst✝ : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
⊢ x * W (m + n) * (x * W (m - n)) * (x * W r) ^ 2 +
        x ^ 4 * (W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2) -
      (x * W (m + r) * (x * W (m - r)) * (x * W n) ^ 2 - x * W (n + r) * (x * W (n - r)) * (x * W m) ^ 2 +
        x ^ 4 * (W (m + n) * W (m - n) * W r ^ 2)) =
    0

Proof state:
case a.a
R : Type u
inst✝ : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
⊢ x * W (m + n) * (x * W (m - n)) * (x * W r) ^ 2 +
        x ^ 4 * (W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2) -
      (x * W (m + r) * (x * W (m - r)) * (x * W n) ^ 2 - x * W (n + r) * (x * W (n - r)) * (x * W m) ^ 2 +
        x ^ 4 * (W (m + n) * W (m - n) * W r ^ 2)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
⊢ (x • W) (m + n) * (x • W) (m - n) * (x • W) r ^ 2 =
    (x • W) (m + r) * (x • W) (m - r) * (x • W) n ^ 2 - (x • W) (n + r) * (x • W) (n - r) * (x • W) m ^ 2

Tactic:
linear_combination (norm := (simp only [Pi.smul_apply, smul_eq_mul]; ring1)) x ^ 4 * h m n r

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Module.lean
/-- `M[1/f] = 0` if and only if `D(f) ∩ Supp M = 0`. -/
lemma LocalizedModule.subsingleton_iff_disjoint {f : R} :
    Subsingleton (LocalizedModule (.powers f) M) ↔
      Disjoint ↑(PrimeSpectrum.basicOpen f) (Module.support R M)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Subsingleton (LocalizedModule (Submonoid.powers f) M) ↔ Disjoint (↑(PrimeSpectrum.basicOpen f)) (Module.support R M)

Tactic:
rw [subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
  disjoint_compl_left_iff, Set.le_iff_subset]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) : n.factorization.prod (· ^ ·) = n

Proof state:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun x1 x2 => x1 ^ x2) = n

Tactic:
rw [factorization_eq_primeFactorsList_multiset n]

Result:
n : ℕ
hn : n ≠ 0
⊢ ((Multiset.toFinsupp ↑n.primeFactorsList).prod fun x1 x2 => x1 ^ x2) = n

Proof state:
n : ℕ
hn : n ≠ 0
⊢ n.primeFactorsList.prod = n

Tactic:
exact prod_primeFactorsList hn

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
⊢ ((Multiset.toFinsupp ↑n.primeFactorsList).prod fun x1 x2 => x1 ^ x2) = n

Tactic:
simp only [← prod_toMultiset, factorization, Multiset.prod_coe, Multiset.toFinsupp_toMultiset]

Result:
n : ℕ
hn : n ≠ 0
⊢ n.primeFactorsList.prod = n
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem dNext_nat (C D : ChainComplex V ℕ) (i : ℕ) (f : ∀ i j, C.X i ⟶ D.X j) :
    dNext i f = C.d i (i - 1) ≫ f (i - 1) i

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ C.d i ((ComplexShape.down ℕ).next i) ≫ f ((ComplexShape.down ℕ).next i) i = C.d i (i - 1) ≫ f (i - 1) i

Tactic:
cases i

Result:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ C.d 0 ((ComplexShape.down ℕ).next 0) ≫ f ((ComplexShape.down ℕ).next 0) 0 = C.d 0 (0 - 1) ≫ f (0 - 1) 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ C.d (n✝ + 1) ((ComplexShape.down ℕ).next (n✝ + 1)) ≫ f ((ComplexShape.down ℕ).next (n✝ + 1)) (n✝ + 1) =
    C.d (n✝ + 1) (n✝ + 1 - 1) ≫ f (n✝ + 1 - 1) (n✝ + 1)

Proof state:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ C.d 0 ((ComplexShape.down ℕ).next 0) ≫ f ((ComplexShape.down ℕ).next 0) 0 = C.d 0 (0 - 1) ≫ f (0 - 1) 0

Tactic:
simp only [shape, ChainComplex.next_nat_zero, ComplexShape.down_Rel, Nat.one_ne_zero,
  not_false_iff, zero_comp, reduceCtorEq]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ (dNext i) f = C.d i (i - 1) ≫ f (i - 1) i

Tactic:
dsimp [dNext]

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ C.d i ((ComplexShape.down ℕ).next i) ≫ f ((ComplexShape.down ℕ).next i) i = C.d i (i - 1) ≫ f (i - 1) i

Proof state:
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ C.d (n✝ + 1) ((ComplexShape.down ℕ).next (n✝ + 1)) ≫ f ((ComplexShape.down ℕ).next (n✝ + 1)) (n✝ + 1) =
    C.d (n✝ + 1) (n✝ + 1 - 1) ≫ f (n✝ + 1 - 1) (n✝ + 1)

Tactic:
congr <;> simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_univ_of_surjective {ι : Type*} {f : ι → β} (H : Surjective f) : f '' univ = univ :=
  eq_univ_of_forall <| by simpa [image]

Proof state:
β : Type u_2
ι : Type u_5
f : ι → β
H : Surjective f
⊢ ∀ (x : β), x ∈ f '' univ

Tactic:
simpa [image]

Result:
no goals
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem map_wittStructureInt (Φ : MvPolynomial idx ℤ) (n : ℕ) :
    map (Int.castRingHom ℚ) (wittStructureInt p Φ n) =
      wittStructureRat p (map (Int.castRingHom ℚ) Φ) n

Proof state:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ (fun x => ↑x)
      (coeff c
            ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
          ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n

Tactic:
simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ←
  map_bind₁, ← RingHom.map_sub, coeff_map]

Result:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑((Int.castRingHom ℚ)
            (coeff c
              ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
                ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) /
          ↑p ^ n).num =
    (Int.castRingHom ℚ)
        (coeff c
          ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
            ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) /
      ↑p ^ n
-- Mathlib/Data/Multiset/Filter.lean
theorem count_filter {p} [DecidablePred p] {a} {s : Multiset α} :
    count a (filter p s) = if p a then count a s else 0

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
exact count_filter_of_neg h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ count a (filter p s) = if p a then count a s else 0

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

Tactic:
exact count_filter_of_pos h

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma monic_esymm {i : ℕ} (him : i ≤ m) : Monic toLex (esymm (Fin m) R i)

Proof state:
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
i : ℕ
him : i ≤ m
⊢ Monic (⇑toLex) (esymm (Fin m) R i)

Tactic:
cases i with
| zero =>
  rw [esymm_zero]
  exact monic_one toLex.injective
| succ i =>
  nontriviality R
  exact (supDegree_monic_esymm him).2

Result:
no goals

Proof state:
case zero
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
him : 0 ≤ m
⊢ Monic (⇑toLex) 1

Tactic:
exact monic_one toLex.injective

Result:
no goals

Proof state:
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
i : ℕ
him : i + 1 ≤ m
a✝ : Nontrivial R
⊢ Monic (⇑toLex) (esymm (Fin m) R (i + 1))

Tactic:
exact (supDegree_monic_esymm him).2

Result:
no goals

Proof state:
case zero
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
him : 0 ≤ m
⊢ Monic (⇑toLex) (esymm (Fin m) R 0)

Tactic:
rw [esymm_zero]

Result:
case zero
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
him : 0 ≤ m
⊢ Monic (⇑toLex) 1

Proof state:
case succ
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
i : ℕ
him : i + 1 ≤ m
⊢ Monic (⇑toLex) (esymm (Fin m) R (i + 1))

Tactic:
nontriviality R

Result:
R : Type u_3
m : ℕ
inst✝ : CommSemiring R
i : ℕ
him : i + 1 ≤ m
a✝ : Nontrivial R
⊢ Monic (⇑toLex) (esymm (Fin m) R (i + 1))
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_linearCombination_right (f : ι →₀ R) (i : ι) :
    b.toDual (b i) (Finsupp.linearCombination R b f) = f i

Proof state:
case neg
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∉ f.support
⊢ 0 = f i

Tactic:
rw [Finsupp.not_mem_support_iff.mp h]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (b.toDual (b i)) ((Finsupp.linearCombination R ⇑b) f) = f i

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum, _root_.map_sum]

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (b.toDual (b i)) (f x • b x) = f i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (b.toDual (b i)) (f x • b x) = f i

Tactic:
simp_rw [LinearMap.map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq]

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then f i else 0) = f i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then f i else 0) = f i

Tactic:
split_ifs with h

Result:
case pos
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ f i = f i

case neg
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∉ f.support
⊢ 0 = f i

Proof state:
case pos
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ f i = f i

Tactic:
rfl

Result:
no goals