harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
lemma exact_iff_of_hasForget [S.HasHomology] :
    S.Exact ↔ ∀ (x₂ : (forget₂ C Ab).obj S.X₂) (_ : ((forget₂ C Ab).map S.g) x₂ = 0),
      ∃ (x₁ : (forget₂ C Ab).obj S.X₁), ((forget₂ C Ab).map S.f) x₁ = x₂

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (∀ (x₂ : ↑(S.map (forget₂ C Ab)).X₂),
      (ConcreteCategory.hom (S.map (forget₂ C Ab)).g) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom (S.map (forget₂ C Ab)).f) x₁ = x₂) ↔
    ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)),
      (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x₁ = x₂

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.Exact ↔
    ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)),
      (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x₁ = x₂

Tactic:
rw [S.exact_iff_exact_map_forget₂, ab_exact_iff]

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (∀ (x₂ : ↑(S.map (forget₂ C Ab)).X₂),
      (ConcreteCategory.hom (S.map (forget₂ C Ab)).g) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom (S.map (forget₂ C Ab)).f) x₁ = x₂) ↔
    ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)),
      (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x₁ = x₂
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem inner_eq_neg_mul_norm_iff_angle_eq_pi {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ⟪x, y⟫ = -(‖x‖ * ‖y‖) ↔ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = -(‖x‖ * ‖y‖)
⊢ angle x y = π

Tactic:
have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = -(‖x‖ * ‖y‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ inner x y = -(‖x‖ * ‖y‖) ↔ angle x y = π

Tactic:
refine ⟨fun h => ?_, inner_eq_neg_mul_norm_of_angle_eq_pi⟩

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = -(‖x‖ * ‖y‖)
⊢ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : inner x y = -(‖x‖ * ‖y‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
⊢ angle x y = π

Tactic:
rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]

Result:
no goals
-- Mathlib/Data/Vector/Snoc.lean
theorem replicate_succ_to_snoc (val : α) :
    replicate (n+1) val = (replicate n val).snoc val

Proof state:
α : Type u_1
n : ℕ
val : α
⊢ replicate (n + 1) val = (replicate n val).snoc val

Tactic:
induction n with
| zero => rfl
| succ n ih =>
  rw [replicate_succ]
  conv => rhs; rw [replicate_succ]
  rw [snoc_cons, ih]

Result:
no goals

Proof state:
case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (val ::ᵥ replicate n val).snoc val

Tactic:
rw [snoc_cons, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
n : ℕ
val : α
⊢ replicate (0 + 1) val = (replicate 0 val).snoc val

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (replicate (n + 1) val).snoc val

Tactic:
conv => rhs; rw [replicate_succ]

Result:
case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (val ::ᵥ replicate n val).snoc val

Proof state:
case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ replicate (n + 1 + 1) val = (replicate (n + 1) val).snoc val

Tactic:
rw [replicate_succ]

Result:
case succ
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = (replicate n val).snoc val
⊢ val ::ᵥ replicate (n + 1) val = (replicate (n + 1) val).snoc val
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[reassoc]
lemma stalkMap_congr_point {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) (x x' : X) (hxx' : x = x') :
    f.stalkMap x ≫ X.presheaf.stalkSpecializes (specializes_of_eq hxx'.symm) =
      Y.presheaf.stalkSpecializes (specializes_of_eq <| hxx' ▸ rfl) ≫ f.stalkMap x'

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x

Tactic:
simp

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'

Tactic:
subst hxx'

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x
-- Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
theorem span_minpoly_eq_annihilator {M} [AddCommGroup M] [Module 𝕜 M] (f : Module.End 𝕜 M) :
    Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f)

Proof state:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
⊢ Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f)

Tactic:
rw [← annIdealGenerator_eq_minpoly, span_singleton_annIdealGenerator]

Result:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
⊢ annIdeal 𝕜 f = Module.annihilator 𝕜[X] (Module.AEval' f)

Proof state:
case h
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ (∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ ∀ (m : Module.AEval' f), x✝ • m = 0

Tactic:
rfl

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ x✝ ∈ annIdeal 𝕜 f ↔ x✝ ∈ Module.annihilator 𝕜[X] (Module.AEval' f)

Tactic:
rw [mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff, Module.mem_annihilator]

Result:
case h
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ (∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ ∀ (m : Module.AEval' f), x✝ • m = 0

Proof state:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
⊢ annIdeal 𝕜 f = Module.annihilator 𝕜[X] (Module.AEval' f)

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ x✝ ∈ annIdeal 𝕜 f ↔ x✝ ∈ Module.annihilator 𝕜[X] (Module.AEval' f)
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma Nontrivial.pow (hs : s.Nontrivial) : ∀ {n}, n ≠ 0 → (s ^ n).Nontrivial
  | 1, _ => by simpa
  | n + 2, _ => by simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nontrivial
x✝ : 1 ≠ 0
⊢ (s ^ 1).Nontrivial

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem exists_ne_of_one_lt_encard (h : 1 < s.encard) (a : α) : ∃ b ∈ s, b ≠ a

Proof state:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_contra! h'

Result:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
⊢ b = b'

Tactic:
rw [h' b hb, h' b' hb']

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
⊢ False

Tactic:
obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h

Result:
case intro.intro.intro.intro
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
⊢ False

Tactic:
apply hne

Result:
case intro.intro.intro.intro
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
⊢ b = b'
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem mk_one' (p : K[X]) :
    RatFunc.mk p 1 = ofFractionRing (algebraMap _ _ p)

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p }

Tactic:
rw [← IsLocalization.mk'_one (M := K[X]⁰) (FractionRing K[X]) p, ← mk_coe_def, Submonoid.coe_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
  getLsbD (BitVec.ofNat n x) i = (i < n && x.testBit i)

Proof state:
n x i : Nat
⊢ (BitVec.ofNat n x).getLsbD i = (decide (i < n) && x.testBit i)

Tactic:
simp [getLsbD, BitVec.ofNat, Fin.val_ofNat']

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem ker_eq_range_of_comp_eq_id {M P} [AddCommGroup M] [Module R M]
    [AddCommGroup P] [Module R P] {f : M →ₗ[R] P} {g : P →ₗ[R] M} (h : f ∘ₗ g = .id) :
    ker f = range (LinearMap.id - g ∘ₗ f) :=
  le_antisymm (fun x hx ↦ ⟨x, show x - g (f x) = x by rw [hx, map_zero, sub_zero]⟩) <|
    range_le_ker_iff.mpr <| by rw [comp_sub, comp_id, ← comp_assoc, h, id_comp, sub_self]

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_11
P : Type u_12
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
x : M
hx : x ∈ ker f
⊢ x - g (f x) = x

Tactic:
rw [hx, map_zero, sub_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_11
P : Type u_12
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f ∘ₗ (id - g ∘ₗ f) = 0

Tactic:
rw [comp_sub, comp_id, ← comp_assoc, h, id_comp, sub_self]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem singleton_sub_eq (a : A) (r : R) : {r} - σ a = σ (↑ₐ r - a)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ {r} - σ a = σ (↑ₐ r - a)

Tactic:
rw [sub_eq_add_neg, neg_eq, singleton_add_eq, sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^i * a ||| b

Proof state:
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
j_lt : j < i
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)

Tactic:
simp [Nat.not_le_of_lt, j_lt]

Result:
no goals

Proof state:
case pred
i b : Nat
b_lt : b < 2 ^ i
a : Nat
⊢ ∀ (i_1 : Nat), (2 ^ i * a + b).testBit i_1 = (2 ^ i * a ||| b).testBit i_1

Tactic:
intro j

Result:
case pred
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
⊢ (2 ^ i * a + b).testBit j = (2 ^ i * a ||| b).testBit j

Proof state:
i b : Nat
b_lt : b < 2 ^ i
a : Nat
⊢ 2 ^ i * a + b = 2 ^ i * a ||| b

Tactic:
apply eq_of_testBit_eq

Result:
case pred
i b : Nat
b_lt : b < 2 ^ i
a : Nat
⊢ ∀ (i_1 : Nat), (2 ^ i * a + b).testBit i_1 = (2 ^ i * a ||| b).testBit i_1

Proof state:
case pred
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
⊢ (2 ^ i * a + b).testBit j = (2 ^ i * a ||| b).testBit j

Tactic:
simp only [testBit_mul_pow_two_add _ b_lt,
      testBit_or, testBit_mul_pow_two]

Result:
case pred
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)

Proof state:
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
j_lt : ¬j < i
i_le : i ≤ j
b_lt_j : b < 2 ^ j
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)

Tactic:
simp [i_le, j_lt, testBit_lt_two_pow, b_lt_j]

Result:
no goals

Proof state:
case pred
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)

Tactic:
if j_lt : j < i then
  simp [Nat.not_le_of_lt, j_lt]
else
  have i_le : i ≤ j := Nat.le_of_not_lt j_lt
  have b_lt_j :=
          calc b < 2 ^ i := b_lt
               _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_le
  simp [i_le, j_lt, testBit_lt_two_pow, b_lt_j]

Result:
no goals

Proof state:
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
j_lt : ¬j < i
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)

Tactic:
have i_le : i ≤ j := Nat.le_of_not_lt j_lt

Result:
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
j_lt : ¬j < i
i_le : i ≤ j
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)

Proof state:
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
j_lt : ¬j < i
i_le : i ≤ j
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)

Tactic:
have b_lt_j :=
        calc b < 2 ^ i := b_lt
             _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_le

Result:
i b : Nat
b_lt : b < 2 ^ i
a j : Nat
j_lt : ¬j < i
i_le : i ≤ j
b_lt_j : b < 2 ^ j
⊢ (if j < i then b.testBit j else a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i) || b.testBit j)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.of_denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (cancel m₁ m₂)) : denote_le ctx (m₁, m₂)

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁.cancel m₂)
⊢ denote_le ctx (m₁, m₂)

Tactic:
have := Poly.of_denote_le_cancelAux (h := h)

Result:
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁.cancel m₂)
this : denote_le ctx ([].reverse ++ m₁, [].reverse ++ m₂)
⊢ denote_le ctx (m₁, m₂)

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁.cancel m₂)
this : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (m₁, m₂)

Tactic:
assumption

Result:
no goals

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁.cancel m₂)
this : denote_le ctx ([].reverse ++ m₁, [].reverse ++ m₂)
⊢ denote_le ctx (m₁, m₂)

Tactic:
simp at this

Result:
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁.cancel m₂)
this : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (m₁, m₂)
-- Mathlib/MeasureTheory/Integral/ExpDecay.lean
theorem exp_neg_integrableOn_Ioi (a : ℝ) {b : ℝ} (h : 0 < b) :
    IntegrableOn (fun x : ℝ => exp (-b * x)) (Ioi a)

Proof state:
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (fun x => rexp (-b * x)) (Ioi a) volume

Tactic:
refine integrableOn_Ioi_deriv_of_nonneg' (fun x _ => ?_) (fun x _ => (exp_pos _).le) this

Result:
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
x✝ : x ∈ Ici a
⊢ HasDerivAt (fun x => -rexp (-b * x) / b) (rexp (-b * x)) x

Proof state:
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => rexp (-b * x)) atTop (𝓝 0)

Tactic:
exact tendsto_exp_atBot.comp (tendsto_id.const_mul_atTop_of_neg (neg_neg_iff_pos.2 h))

Result:
no goals

Proof state:
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => -rexp (-b * x) / b) atTop (𝓝 (-0 / b))

Tactic:
refine Tendsto.div_const (Tendsto.neg ?_) _

Result:
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => rexp (-b * x)) atTop (𝓝 0)

Proof state:
a b : ℝ
h : 0 < b
⊢ IntegrableOn (fun x => rexp (-b * x)) (Ioi a) volume

Tactic:
have : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b)) := by
  refine Tendsto.div_const (Tendsto.neg ?_) _
  exact tendsto_exp_atBot.comp (tendsto_id.const_mul_atTop_of_neg (neg_neg_iff_pos.2 h))

Result:
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (fun x => rexp (-b * x)) (Ioi a) volume

Proof state:
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
x✝ : x ∈ Ici a
⊢ HasDerivAt (fun x => -rexp (-b * x) / b) (rexp (-b * x)) x

Tactic:
simpa [h.ne'] using ((hasDerivAt_id x).const_mul b).neg.exp.neg.div_const b

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem eventually_fintsupport_subset :
    ∀ᶠ y in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy : {i | y ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))}
z : ι
hz : z ∈ ρ.fintsupport y
⊢ z ∈ ρ.fintsupport x₀

Tactic:
rw [PartitionOfUnity.mem_fintsupport_iff] at *

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy : {i | y ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))}
z : ι
hz : y ∈ tsupport ⇑(ρ z)
⊢ x₀ ∈ tsupport ⇑(ρ z)

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ (x : X),
    {i | x ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))} → ρ.fintsupport x ⊆ ρ.fintsupport x₀

Tactic:
intro y hy z hz

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy : {i | y ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))}
z : ι
hz : z ∈ ρ.fintsupport y
⊢ z ∈ ρ.fintsupport x₀

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy : {i | y ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))}
z : ι
hz : y ∈ tsupport ⇑(ρ z)
⊢ x₀ ∈ tsupport ⇑(ρ z)

Tactic:
exact hy hz

Result:
no goals

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ᶠ (y : X) in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀

Tactic:
apply (ρ.locallyFinite.closure.eventually_subset (fun _ ↦ isClosed_closure) x₀).mono

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ (x : X),
    {i | x ∈ closure (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure (support ⇑(ρ i))} → ρ.fintsupport x ⊆ ρ.fintsupport x₀
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableWithinAt_neg_iff :
    DifferentiableWithinAt 𝕜 (fun y => -f y) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 (fun y => -f y) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
simpa only [neg_neg] using h.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem mem_attachWith (l : Array α) {q : α → Prop} (H) (x : {x // q x}) :
    x ∈ l.attachWith q H ↔ x.1 ∈ l

Proof state:
case mk
α : Type u_1
q : α → Prop
x : { x // q x }
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → q x
⊢ x ∈ { toList := toList✝ }.attachWith q H ↔ x.val ∈ { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array α
q : α → Prop
H : ∀ (x : α), x ∈ l → q x
x : { x // q x }
⊢ x ∈ l.attachWith q H ↔ x.val ∈ l

Tactic:
cases l

Result:
case mk
α : Type u_1
q : α → Prop
x : { x // q x }
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → q x
⊢ x ∈ { toList := toList✝ }.attachWith q H ↔ x.val ∈ { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂) :
    l₂.lookup k = none → l₁.lookup k = none

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
l₁ l₂ : List (α × β)
h : l₁ <+ l₂
⊢ findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₂ = none →
    findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₁ = none

Tactic:
exact h.findSome?_eq_none

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
l₁ l₂ : List (α × β)
h : l₁ <+ l₂
⊢ lookup k l₂ = none → lookup k l₁ = none

Tactic:
simp only [lookup_eq_findSome?]

Result:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
l₁ l₂ : List (α × β)
h : l₁ <+ l₂
⊢ findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₂ = none →
    findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₁ = none
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_intCast {n : ℤ} : derivative (n : R[X]) = 0

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative (C ↑n) = 0

Tactic:
exact derivative_C

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative ↑n = 0

Tactic:
rw [← C_eq_intCast n]

Result:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative (C ↑n) = 0
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_append {b : ℕ} {l1 l2 : List ℕ} :
    ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

Proof state:
b : ℕ
l1 l2 : List ℕ
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

Tactic:
induction' l1 with hd tl IH

Result:
case nil
b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ [].length * ofDigits b l2

case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ (hd :: tl).length * ofDigits b l2

Proof state:
case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ (hd :: tl).length * ofDigits b l2

Tactic:
rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']

Result:
case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2

Proof state:
case nil
b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ [].length * ofDigits b l2

Tactic:
simp [ofDigits]

Result:
no goals

Proof state:
case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem decide_eq_true {p : Prop} {_ : Decidable p} : p = True → decide p = true

Proof state:
p : Prop
x✝ : Decidable p
⊢ p = True → decide p = true

Tactic:
simp

Result:
no goals