harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem lift_index_right {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v2 : ℕ) :
    padicNorm p (f (stationaryPoint hf)) =
    padicNorm p (f (max v1 (max v2 (stationaryPoint hf))))

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (v1 ⊔ (v2 ⊔ stationaryPoint hf)))

Tactic:
apply stationaryPoint_spec hf

Result:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ v1 ⊔ (v2 ⊔ stationaryPoint hf)

case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Proof state:
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ v2 ⊔ stationaryPoint hf ≤ v1 ⊔ (v2 ⊔ stationaryPoint hf)

Tactic:
apply le_max_right

Result:
no goals

Proof state:
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝

Tactic:
apply le_max_right v2

Result:
no goals

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ v1 ⊔ (v2 ⊔ stationaryPoint hf)

Tactic:
apply le_trans

Result:
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝

case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ ?a.b✝ ≤ v1 ⊔ (v2 ⊔ stationaryPoint hf)

case a.b
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ ℕ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n = 0 then none else some a

Proof state:
α : Type u_1
a : α
n : Nat
⊢ (replicate n a).getLast? = if n = 0 then none else some a

Tactic:
simp only [← head?_reverse, reverse_replicate, head?_replicate]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_image2 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
    ⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
δ : Type u_9
f : β → γ → δ
s : Set β
t : Set γ
g : δ → α
⊢ ⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)

Tactic:
rw [← image_prod, iSup_image, biSup_prod]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem root_left_of_root_gcd [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k}
    (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : f.eval₂ ϕ α = 0

Proof state:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
⊢ eval₂ ϕ α f = 0

Tactic:
obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_left f g

Result:
case intro
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α f = 0

Proof state:
case intro
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α f = 0

Tactic:
rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem equivPair_head_smul_equivPair_tail {i : ι} (w : Word M) :
    of (equivPair i w).head • (equivPair i w).tail = w

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ of ((equivPair i) w).head • ((equivPair i) w).tail = w

Tactic:
rw [← rcons_eq_smul, ← equivPair_symm, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l)

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, t ++ l = replicate (n - l.length) a ++ l

Tactic:
exact Exists.intro (replicate (n - length l) a) rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ l <:+ leftpad n a l

Tactic:
simp only [IsSuffix, leftpad]

Result:
α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, t ++ l = replicate (n - l.length) a ++ l
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
lemma finsuppScalarRight_apply_tmul (m : M) (p : ι →₀ R) :
    finsuppScalarRight R M ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (n • m)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
⊢ (finsuppScalarRight R M ι) (m ⊗ₜ[R] p) = p.sum fun i n => Finsupp.single i (n • m)

Tactic:
ext i

Result:
case h
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ ((finsuppScalarRight R M ι) (m ⊗ₜ[R] p)) i = (p.sum fun i n => Finsupp.single i (n • m)) i

Proof state:
case h
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ ((finsuppScalarRight R M ι) (m ⊗ₜ[R] p)) i = (p.sum fun i n => Finsupp.single i (n • m)) i

Tactic:
rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
  Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne) (by simp), Finsupp.single_eq_same]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ p i = 0 → (Finsupp.single i (0 • m)) i = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem covBy_iff : x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹) ⋖ (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹).1 ⋖ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 ∨
      (fst✝¹, snd✝¹).2 ⋖ (fst✝, snd✝).2 ∧ (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1

Tactic:
exact mk_covBy_mk_iff

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⋖ y ↔ (fst✝, snd✝).1 ⋖ y.1 ∧ (fst✝, snd✝).2 = y.2 ∨ (fst✝, snd✝).2 ⋖ y.2 ∧ (fst✝, snd✝).1 = y.1

Tactic:
cases y

Result:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹) ⋖ (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹).1 ⋖ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 ∨
      (fst✝¹, snd✝¹).2 ⋖ (fst✝, snd✝).2 ∧ (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1

Tactic:
cases x

Result:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⋖ y ↔ (fst✝, snd✝).1 ⋖ y.1 ∧ (fst✝, snd✝).2 = y.2 ∨ (fst✝, snd✝).2 ⋖ y.2 ∧ (fst✝, snd✝).1 = y.1
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
lemma LFunctionTrivChar₁_apply_one_ne_zero : LFunctionTrivChar₁ n 1 ≠ 0

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹) ≠ 0

Tactic:
refine Finset.prod_ne_zero_iff.mpr fun p hp ↦ ?_

Result:
n : ℕ
inst✝ : NeZero n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - (↑p)⁻¹ ≠ 0

Proof state:
n : ℕ
inst✝ : NeZero n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - (↑p)⁻¹ ≠ 0

Tactic:
simpa [sub_ne_zero] using (Nat.prime_of_mem_primeFactors hp).ne_one

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ LFunctionTrivChar₁ n 1 ≠ 0

Tactic:
simp only [Function.update_self]

Result:
n : ℕ
inst✝ : NeZero n
⊢ ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹) ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter_of_beq [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF)
    (he : k == k') : k' ∈ m.alter k f ↔ (f (m.get? k)).isSome

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
he : (k == k') = true
⊢ k' ∈ m.alter k f ↔ (f (m.get? k)).isSome = true

Tactic:
rw [mem_alter h, if_pos he]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_pred_lt_pow {x w : Nat} (h₁ : 1 < x) (h₂ : 0 < w) :
    x ^ (w - 1) < x ^ w :=
  Nat.pow_lt_pow_of_lt h₁ (by omega)

Proof state:
x w : Nat
h₁ : 1 < x
h₂ : 0 < w
⊢ w - 1 < w

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
@[simp]
lemma Dual.apply_one_mul_eq (f : Dual R R) (r : R) :
    f 1 * r = f r

Proof state:
R : Type u
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ f 1 * r = f r

Tactic:
conv_rhs => rw [← mul_one r, ← smul_eq_mul]

Result:
R : Type u
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ f 1 * r = f (r • 1)

Proof state:
R : Type u
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ f 1 * r = f (r • 1)

Tactic:
rw [map_smul, smul_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_ne_empty_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Array α}
    (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ #[] ↔ xs ≠ #[]

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
⊢ pmap f xs H ≠ #[] ↔ xs ≠ #[]

Tactic:
cases xs

Result:
case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ pmap f { toList := toList✝ } H ≠ #[] ↔ { toList := toList✝ } ≠ #[]

Proof state:
case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ pmap f { toList := toList✝ } H ≠ #[] ↔ { toList := toList✝ } ≠ #[]

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem fromBlocks_eq_of_invertible₁₁ (A : Matrix m m α) (B : Matrix m n α) (C : Matrix l m α)
    (D : Matrix l n α) [Invertible A] :
    fromBlocks A B C D =
      fromBlocks 1 0 (C * ⅟ A) 1 * fromBlocks A 0 0 (D - C * ⅟ A * B) *
        fromBlocks 1 (⅟ A * B) 0 1

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix l m α
D : Matrix l n α
inst✝ : Invertible A
⊢ fromBlocks A B C D = fromBlocks 1 0 (C * ⅟A) 1 * fromBlocks A 0 0 (D - C * ⅟A * B) * fromBlocks 1 (⅟A * B) 0 1

Tactic:
simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add,
  Matrix.one_mul, Matrix.mul_one, invOf_mul_self, Matrix.mul_invOf_cancel_left,
  Matrix.invOf_mul_cancel_right, Matrix.mul_assoc, add_sub_cancel]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean
theorem ContMDiffWithinAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M}
    (hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x)
    (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x) :
    ContMDiffWithinAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s x :=
  ContDiffWithinAt.comp_contMDiffWithinAt (t := univ)
    (g := fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2)
    (by apply ContDiff.contDiffAt; exact contDiff_fst.clm_apply contDiff_snd) (hg.prod_mk_space hf)
    (by simp_rw [preimage_univ, subset_univ])

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_8
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
⊢ ContDiffWithinAt 𝕜 n (fun x => x.1 x.2) univ (g x, f x)

Tactic:
apply ContDiff.contDiffAt

Result:
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_8
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
⊢ ContDiff 𝕜 n fun x => x.1 x.2

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_8
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
⊢ s ⊆ (fun x => (g x, f x)) ⁻¹' univ

Tactic:
simp_rw [preimage_univ, subset_univ]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_8
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_9
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x
hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x
⊢ ContDiff 𝕜 n fun x => x.1 x.2

Tactic:
exact contDiff_fst.clm_apply contDiff_snd

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_comp (f : F ⟶ G) (g : G ⟶ K) :
    ofHom (f ≫ g) = (ofHom f).comp (ofHom g) (zero_add 0)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
f : F ⟶ G
g : G ⟶ K
⊢ ofHom (f ≫ g) = (ofHom f).comp (ofHom g) ⋯

Tactic:
simp only [ofHom, HomologicalComplex.comp_f, ofHoms_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_le_integral_pos (hf : Integrable f μ) : 0 < μ {x | f x ≤ ∫ a, f a ∂μ}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ 0 < μ {x | f x ≤ ∫ (a : α), f a ∂μ}

Tactic:
simpa only [average_eq_integral] using
  measure_le_average_pos (IsProbabilityMeasure.ne_zero μ) hf

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem map_X : map f X = X

Proof state:
case h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
n✝ : ℕ
⊢ (coeff S n✝) ((map f) X) = (coeff S n✝) X

Tactic:
simp [coeff_X, apply_ite f]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
⊢ (map f) X = X

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
n✝ : ℕ
⊢ (coeff S n✝) ((map f) X) = (coeff S n✝) X
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_neg_eq_smul (A : Matrix n n R) :
    det (-A) = (-1 : Units ℤ) ^ Fintype.card n • det A

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
⊢ (-A).det = (-1) ^ Fintype.card n • A.det

Tactic:
rw [← det_smul_of_tower, Units.neg_smul, one_smul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_inter_edgeSet_right_eq :
    G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s

Tactic:
ext <;> simp +contextual [imp_false]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem filterMap_mono (h : s ⊆ t) :
    filterMap f s f_inj ⊆ filterMap f t f_inj

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
h : s ⊆ t
⊢ filterMap f s f_inj ⊆ filterMap f t f_inj

Tactic:
rw [← val_le_iff] at h ⊢

Result:
α : Type u_1
β : Type u_2
f : α → Option β
s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
h : s.val ≤ t.val
⊢ (filterMap f s f_inj).val ≤ (filterMap f t f_inj).val

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
h : s.val ≤ t.val
⊢ (filterMap f s f_inj).val ≤ (filterMap f t f_inj).val

Tactic:
exact Multiset.filterMap_le_filterMap f h

Result:
no goals
-- Mathlib/Order/Filter/Extr.lean
theorem IsMinFilter.sub (hf : IsMinFilter f l a) (hg : IsMaxFilter g l a) :
    IsMinFilter (fun x => f x - g x) l a

Proof state:
α : Type u
β : Type v
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter (fun x => f x - g x) l a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem periodic_with_period_zero [AddZeroClass α] (f : α → β) : Periodic f 0 := fun x => by
  rw [add_zero]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass α
f : α → β
x : α
⊢ f (x + 0) = f x

Tactic:
rw [add_zero]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem norm_mk_zero (S : AddSubgroup M) : ‖(0 : M ⧸ S)‖ = 0

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
⊢ ‖0‖ = 0

Tactic:
erw [quotient_norm_eq_zero_iff]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
⊢ 0 ∈ closure ↑S

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
⊢ 0 ∈ closure ↑S

Tactic:
exact subset_closure S.zero_mem

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem div_self_mul_self (a : G₀) : a / a * a = a

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / a * a = a

Tactic:
rw [div_eq_mul_inv, mul_inv_mul_cancel a]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_else_decide_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
    (@ite _ p h q (decide p)) = (decide p && q)

Proof state:
p : Prop
h w : Decidable p
q : Bool
⊢ (if p then q else decide p) = (decide p && q)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_apply_of_not_predicate {f : R → R} (a : A) (ha : ¬ p a) :
    cfcₙ f a = 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
ha : ¬p a
⊢ cfcₙ f a = 0

Tactic:
rw [cfcₙ_def, dif_neg (not_and_of_not_left _ ha)]

Result:
no goals
-- Mathlib/Data/List/TakeWhile.lean
theorem takeWhile_idem : takeWhile p (takeWhile p l) = takeWhile p l

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p (takeWhile p l) = takeWhile p l

Tactic:
simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem mem_dlookup {a} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : Sigma.mk a b ∈ l) :
    b ∈ dlookup a l

Proof state:
case intro
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
b' : β ⟨a, b⟩.fst
h' : dlookup ⟨a, b⟩.fst l = some b'
⊢ b ∈ dlookup a l

Tactic:
cases nd.eq_of_mk_mem h (of_mem_dlookup h')

Result:
case intro.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
h' : dlookup ⟨a, b⟩.fst l = some b
⊢ b ∈ dlookup a l

Proof state:
case intro.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
h' : dlookup ⟨a, b⟩.fst l = some b
⊢ b ∈ dlookup a l

Tactic:
exact h'

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ b ∈ dlookup a l

Tactic:
obtain ⟨b', h'⟩ := Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h))

Result:
case intro
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
b' : β ⟨a, b⟩.fst
h' : dlookup ⟨a, b⟩.fst l = some b'
⊢ b ∈ dlookup a l
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_zero : HasFiniteIntegral (fun _ : α => (0 : β)) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
⊢ HasFiniteIntegral (fun x => 0) μ

Tactic:
simp [hasFiniteIntegral_iff_enorm]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_comm : f ×ˢ g = map (fun p : β × α => (p.2, p.1)) (g ×ˢ f)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ Prod.swap <$> (g ×ˢ f) = map (fun p => (p.2, p.1)) (g ×ˢ f)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = map (fun p => (p.2, p.1)) (g ×ˢ f)

Tactic:
rw [prod_comm', ← map_swap_eq_comap_swap]

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ Prod.swap <$> (g ×ˢ f) = map (fun p => (p.2, p.1)) (g ×ˢ f)
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem degree_interpolate_erase_lt (hvs : Set.InjOn v s) (hi : i ∈ s) :
    (interpolate (s.erase i) v r).degree < ↑(#s - 1)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#s - 1)

Tactic:
rw [← Finset.card_erase_of_mem hi]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#(s.erase i))

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ((interpolate (s.erase i) v) r).degree < ↑(#(s.erase i))

Tactic:
exact degree_interpolate_lt _ (Set.InjOn.mono (coe_subset.mpr (erase_subset _ _)) hvs)

Result:
no goals
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem isCountablyGenerated_seq [Countable ι'] (x : ι' → Set α) :
    IsCountablyGenerated (⨅ i, 𝓟 (x i))

Proof state:
α : Type u_1
ι' : Sort u_5
inst✝ : Countable ι'
x : ι' → Set α
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated

Tactic:
use range x, countable_range x

Result:
case right
α : Type u_1
ι' : Sort u_5
inst✝ : Countable ι'
x : ι' → Set α
⊢ ⨅ i, 𝓟 (x i) = generate (range x)

Proof state:
case right
α : Type u_1
ι' : Sort u_5
inst✝ : Countable ι'
x : ι' → Set α
⊢ ⨅ i, 𝓟 (x i) = generate (range x)

Tactic:
rw [generate_eq_biInf, iInf_range]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_eq_mkRat {num den} (den_nz) : normalize num den den_nz = mkRat num den

Proof state:
num : Int
den : Nat
den_nz : den ≠ 0
⊢ normalize num den den_nz = mkRat num den

Tactic:
simp [mkRat, den_nz]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_two_pi : cos (2 * π) = 1

Proof state:
⊢ cos (2 * ↑π) = 1

Tactic:
simp [two_mul, cos_add]

Result:
no goals