harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem null_iff_toMeasure_null (ν : FiniteMeasure Ω) (s : Set Ω) :
    ν s = 0 ↔ (ν : Measure Ω) s = 0 :=
  ⟨fun h ↦ by rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero],
   fun h ↦ congrArg ENNReal.toNNReal h⟩

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : FiniteMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑ν s = 0

Tactic:
rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_compContinuousMultilinearMap_le (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖g.compContinuousMultilinearMap f‖ ≤ ‖g‖ * ‖f‖ :=
  ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun m ↦
    calc
      ‖g (f m)‖ ≤ ‖g‖ * (‖f‖ * ∏ i, ‖m i‖) := g.le_opNorm_of_le <| f.le_opNorm _
      _ = _ := (mul_assoc _ _ _).symm

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : G →L[𝕜] G'
f : ContinuousMultilinearMap 𝕜 E G
⊢ 0 ≤ ‖g‖ * ‖f‖

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_le_iff {f : MvPolynomial σ R} {d : σ →₀ ℕ} :
    m.degree f ≼[m] d ↔ ∀ c ∈ f.support, c ≼[m] d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn (m.degree f) ≤ m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c ≤ m.toSyn d

Tactic:
unfold degree

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn)) ≤ m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c ≤ m.toSyn d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn)) ≤ m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c ≤ m.toSyn d

Tactic:
simp only [AddEquiv.apply_symm_apply, Finset.sup_le_iff, mem_support_iff, ne_eq]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
lemma Real.summable_one_div_int_add_rpow (a : ℝ) (s : ℝ) :
    Summable (fun n : ℤ ↦ 1 / |n + a| ^ s) ↔ 1 < s

Proof state:
a s : ℝ
⊢ (Summable fun n => 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
  Int.cast_neg, neg_neg, Int.cast_natCast, summable_one_div_nat_add_rpow, and_self]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_right' (a b : α) : toIocMod hp (a + p) b = toIocMod hp a b + p

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

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

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem card_toMultiset (f : α →₀ ℕ) : Multiset.card (toMultiset f) = f.sum fun _ => id

Proof state:
α : Type u_1
f : α →₀ ℕ
⊢ (toMultiset f).card = f.sum fun x => id

Tactic:
simp [toMultiset_apply, map_finsupp_sum, Function.id_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem map_prod_right_eq_zip {l : Vector α n} (f : α → β) :
    (l.map fun x => (f x, x)) = (l.map f).zip l

Proof state:
case mk.e_w
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => x) { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β
⊢ map (fun x => (f x, x)) l = (map f l).zip l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => (f x, x)) { toArray := l, size_toArray := ⋯ } =
    (map f { toArray := l, size_toArray := ⋯ }).zip { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => (f x, x)) { toArray := l, size_toArray := ⋯ } =
    (map f { toArray := l, size_toArray := ⋯ }).zip { toArray := l, size_toArray := ⋯ }

Tactic:
rw [← zip_map']

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ (map f { toArray := l, size_toArray := ⋯ }).zip (map (fun x => x) { toArray := l, size_toArray := ⋯ }) =
    (map f { toArray := l, size_toArray := ⋯ }).zip { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ (map f { toArray := l, size_toArray := ⋯ }).zip (map (fun x => x) { toArray := l, size_toArray := ⋯ }) =
    (map f { toArray := l, size_toArray := ⋯ }).zip { toArray := l, size_toArray := ⋯ }

Tactic:
congr

Result:
case mk.e_w
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map (fun x => x) { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x

Proof state:
x y : Nat
⊢ x % y = ite (0 < y ∧ y ≤ x) ((x - y) % y) x

Tactic:
rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore]

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Basic.lean
theorem map_invOf {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [Monoid S]
    [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R)
    [Invertible r] [ifr : Invertible (f r)] :
    f (⅟ r) = ⅟ (f r) :=
  have h : ifr = Invertible.map f r := Subsingleton.elim _ _
  by subst h; rfl

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f ⅟r = ⅟(f r)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
ifr : Invertible (f r)
h : ifr = Invertible.map f r
⊢ f ⅟r = ⅟(f r)

Tactic:
subst h

Result:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f ⅟r = ⅟(f r)
-- Mathlib/Data/Stream/Init.lean
theorem append_stream_head_tail (s : Stream' α) : [head s] ++ₛ tail s = s

Proof state:
α : Type u
s : Stream' α
⊢ [s.head] ++ₛ s.tail = s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive ite_pos]
lemma one_lt_ite [LT α] (ha : 1 < a) (hb : 1 < b) : 1 < ite p a b

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 1 < a
hb : 1 < b
⊢ 1 < if p then a else b

Tactic:
split <;> assumption

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_le_add (n : ℕ) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n

Proof state:
n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt

Tactic:
exact le_of_lt_succ (lt_succ_sqrt n)

Result:
no goals

Proof state:
n : ℕ
⊢ n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

Tactic:
rw [← succ_mul]

Result:
n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt
-- Mathlib/Data/Int/ModEq.lean
theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]

Proof state:
n a b : ℤ
⊢ -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp only [modEq_iff_dvd, (by omega : -b - -a = -(b - a)), Int.dvd_neg]

Result:
no goals

Proof state:
n a b : ℤ
⊢ -b - -a = -(b - a)

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Group/Translate.lean
@[simp] lemma translate_zero (f : G → α) : τ 0 f = f

Proof state:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
⊢ τ 0 f = f

Tactic:
ext

Result:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
x✝ : G
⊢ τ 0 f x✝ = f x✝

Proof state:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
x✝ : G
⊢ τ 0 f x✝ = f x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_monomial_le (n : ℕ) (a : R) : degree (monomial n a) ≤ n :=
  letI := Classical.decEq R
  if h : a = 0 then by rw [h, (monomial n).map_zero, degree_zero]; exact bot_le
  else le_of_eq (degree_monomial n h)

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ((monomial n) a).degree ≤ ↑n

Tactic:
rw [h, (monomial n).map_zero, degree_zero]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ⊥ ≤ ↑n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ⊥ ≤ ↑n

Tactic:
exact bot_le

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
lemma realContinuousMapZeroOfNNReal_injective :
    Function.Injective (realContinuousMapZeroOfNNReal (X := X) (A := A))

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
⊢ φ = ψ

Tactic:
ext f

Result:
case h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
f : C(X, ℝ≥0)₀
⊢ φ f = ψ f

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
⊢ Function.Injective realContinuousMapZeroOfNNReal

Tactic:
intro φ ψ h

Result:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
⊢ φ = ψ

Proof state:
case h
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
f : C(X, ℝ≥0)₀
⊢ φ f = ψ f

Tactic:
simpa using congr($(h) ((ContinuousMapZero.mk ⟨toReal, continuous_coe⟩ rfl).comp f))

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem eval_sumIDeriv_of_pos
    [CommRing R] [Nontrivial R] [NoZeroDivisors R] (p : R[X]) {q : ℕ} (hq : 0 < q) :
    ∃ gp : R[X], gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : R) {p' : R[X]},
        p = ((X : R[X]) - C r) ^ (q - 1) * p' →
        eval r (sumIDeriv p) = (q - 1)! • p'.eval r + q ! • eval r gp

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
p : R[X]
q : ℕ
hq : 0 < q
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : R) {p' : R[X]},
        p = (X - C r) ^ (q - 1) * p' → eval r (sumIDeriv p) = (q - 1)! • eval r p' + q ! • eval r gp

Tactic:
simpa using aeval_sumIDeriv_of_pos R p hq Function.injective_id

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_self_homothety (p₁ p₂ : P) (c : 𝕜) :
    dist p₂ (homothety p₁ c p₂) = ‖1 - c‖ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist p₂ ((homothety p₁ c) p₂) = ‖1 - c‖ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_homothety_self]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem H1Map_id : H1Map (MonoidHom.id _) (𝟙 A) = 𝟙 _

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ 𝟙 (moduleCatMk (dZero A) (dOne A) ⋯).moduleCatLeftHomologyData.H = 𝟙 (H1 A)

Tactic:
rfl

Result:
no goals

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ H1Map (MonoidHom.id H) (𝟙 A) = 𝟙 (H1 A)

Tactic:
simp only [H1Map, shortComplexH1, mapShortComplexH1_id, leftHomologyMap'_id]

Result:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ 𝟙 (moduleCatMk (dZero A) (dOne A) ⋯).moduleCatLeftHomologyData.H = 𝟙 (H1 A)
-- Mathlib/Data/List/Basic.lean
theorem head_cons_tail (x : List α) (h : x ≠ []) : x.head h :: x.tail = x

Proof state:
α : Type u
x : List α
h : x ≠ []
⊢ x.head h :: x.tail = x

Tactic:
cases x <;> simp at h ⊢

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem mem_seq_iff {f : Filter (α → β)} {g : Filter α} {s : Set β} :
    s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, Set.seq u t ⊆ s

Proof state:
α : Type u_1
β : Type u_2
f : Filter (α → β)
g : Filter α
s : Set β
⊢ s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s

Tactic:
simp only [mem_seq_def, seq_subset, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_of_forall_one_lt_lt_mul (h : ∀ ε : α, 1 < ε → a < b * ε) : a ≤ b :=
  le_of_not_lt fun h₁ => lt_irrefl a (by simpa using h _ (lt_inv_mul_iff_lt.mpr h₁))

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b : α
h : ∀ (ε : α), 1 < ε → a < b * ε
h₁ : b < a
⊢ a < a

Tactic:
simpa using h _ (lt_inv_mul_iff_lt.mpr h₁)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_C_mul_X_add_C_of_IsUnit (b : R) (a : Rˣ) : (C (a : R) * X + C b).roots =
    {-(a⁻¹ * b)}

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C ↑a * X + C b).roots = {-(↑a⁻¹ * b)}

Tactic:
rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₂_eq_zero' (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂)
    (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ ≠ i₁₂) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
rw [totalAux.d₂_eq' K c₁₂ i₁ h i₁₂, K.toGradedObject.ιMapObjOrZero_eq_zero, comp_zero, smul_zero]

Result:
case h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂
⊢ c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂

Proof state:
case h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂
⊢ c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂

Tactic:
exact h'

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem eq_zero_of_mono_cokernel [Mono (cokernel.π f)] : f = 0 :=
  (cancel_mono (cokernel.π f)).1 (by simp)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : Mono (cokernel.π f)
⊢ f ≫ cokernel.π f = 0 ≫ cokernel.π f

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem injective (f : α → β) (hf : Injective f) : Injective (mapFun f : 𝕎 α → 𝕎 β)

Proof state:
case h
p✝ : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
a₁✝ a₂✝ : WittVector p✝ α
h : mapFun f a₁✝ = mapFun f a₂✝
p : ℕ
⊢ a₁✝.coeff p = a₂✝.coeff p

Tactic:
exact hf (congr_arg (fun x => coeff x p) h :)

Result:
no goals

Proof state:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
a₁✝ a₂✝ : 𝕎 α
h : mapFun f a₁✝ = mapFun f a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext p

Result:
case h
p✝ : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
a₁✝ a₂✝ : WittVector p✝ α
h : mapFun f a₁✝ = mapFun f a₂✝
p : ℕ
⊢ a₁✝.coeff p = a₂✝.coeff p

Proof state:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ Injective (mapFun f)

Tactic:
intros _ _ h

Result:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
a₁✝ a₂✝ : 𝕎 α
h : mapFun f a₁✝ = mapFun f a₂✝
⊢ a₁✝ = a₂✝
-- Mathlib/Probability/Martingale/Basic.lean
theorem smul_nonneg {f : ι → Ω → F} {c : ℝ} (hc : 0 ≤ c) (hf : Submartingale f ℱ μ) :
    Submartingale (c • f) ℱ μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (-(c • -f)) ℱ μ

Tactic:
exact Supermartingale.neg (hf.neg.smul_nonneg hc)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ - -c • f = -(c • -f)

Tactic:
ext (i x)

Result:
case h.h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
i : ι
x : Ω
⊢ (- -c • f) i x = (-(c • -f)) i x

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (c • f) ℱ μ

Tactic:
rw [← neg_neg c, (by ext (i x); simp : - -c • f = -(c • -f))]

Result:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
⊢ Submartingale (-(c • -f)) ℱ μ

Proof state:
case h.h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Submartingale f ℱ μ
i : ι
x : Ω
⊢ (- -c • f) i x = (-(c • -f)) i x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_replicate : eval assign (.replicate n expr) = BitVec.replicate n (expr.eval assign)

Proof state:
assign : Assignment
n a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (replicate n expr) = BitVec.replicate n (eval assign expr)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive (attr := simp, norm_cast)]
lemma coe_div_coe [SetLike S G] [DivisionMonoid G] [SubgroupClass S G] (H : S) :
    H / H = (H : Set G)

Proof state:
G : Type u_2
S : Type u_4
inst✝² : SetLike S G
inst✝¹ : DivisionMonoid G
inst✝ : SubgroupClass S G
H : S
⊢ ↑H / ↑H = ↑H

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem mkNotCached_le_size (aig : AIG α) (gate : Ref aig) :
    aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤
    ((aig.mkConstCached true).aig.mkGateCached
            { lhs := { ref := (aig.mkConstCached true).ref, inv := false },
              rhs := { ref := gate.cast ⋯, inv := true } }).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤ (aig.mkConstCached true).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size

Tactic:
simp only [mkNotCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤
    ((aig.mkConstCached true).aig.mkGateCached
            { lhs := { ref := (aig.mkConstCached true).ref, inv := false },
              rhs := { ref := gate.cast ⋯, inv := true } }).aig.decls.size

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤ (aig.mkConstCached true).aig.decls.size

Tactic:
apply mkConstCached_le_size

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem Disjoint.ndunion_eq {s t : Multiset α} (h : Disjoint s t) :
    s.ndunion t = s.dedup + t

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ ndunion (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) =
    dedup (Quot.mk (⇑(isSetoid α)) a✝) + Quot.mk (⇑(isSetoid α)) b✝

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.union_eq <| by simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ s.ndunion t = s.dedup + t

Tactic:
induction s, t using Quot.induction_on₂

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ ndunion (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) =
    dedup (Quot.mk (⇑(isSetoid α)) a✝) + Quot.mk (⇑(isSetoid α)) b✝
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_dual : ∀ t : Ordnode α, dual (dual t) = t
  | nil => rfl
  | node s l x r => by rw [dual, dual, dual_dual l, dual_dual r]

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node s l x r).dual.dual = node s l x r

Tactic:
rw [dual, dual, dual_dual l, dual_dual r]

Result:
no goals