harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftShift_add (a n' : ℤ) (hn' : n + a = n') :
    (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn').v p q hpq + (γ₂.leftShift a n' hn').v p q hpq

Tactic:
simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by omega), add_v, comp_add, smul_add]

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn').v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn').v p q hpq + (γ₂.leftShift a n' hn').v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
⊢ (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn').v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ p + a + n = q

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
@[to_additive]
protected lemma HasCompactMulSupport.inv' {α β : Type*} [TopologicalSpace α] [DivisionMonoid β]
    {f : α → β} (hf : HasCompactMulSupport f) :
    HasCompactMulSupport (f⁻¹)

Proof state:
α : Type u_9
β : Type u_10
inst✝¹ : TopologicalSpace α
inst✝ : DivisionMonoid β
f : α → β
hf : HasCompactMulSupport f
⊢ HasCompactMulSupport f⁻¹

Tactic:
simpa only [HasCompactMulSupport, mulTSupport, mulSupport_inv'] using hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
theorem blastDivSubtractShift_le_size (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
    aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size

Proof state:
case h.h.h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤
    (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
            { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv.blastShiftConcat)

Result:
case h.h.h.h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤ (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig.decls.size
-- Mathlib/Order/Birkhoff.lean
lemma exists_birkhoff_representation.{u} (α : Type u) [Finite α] [DistribLattice α] :
    ∃ (β : Type u) (_ : DecidableEq β) (_ : Fintype β) (f : LatticeHom α (Finset β)),
      Injective f

Proof state:
α : Type u
inst✝¹ : Finite α
inst✝ : DistribLattice α
⊢ ∃ β x x_1 f, Injective ⇑f

Tactic:
classical
cases nonempty_fintype α
exact ⟨{a : α // SupIrred a}, _, inferInstance, _, LatticeHom.birkhoffFinset_injective⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Finite α
inst✝ : DistribLattice α
⊢ ∃ β x x_1 f, Injective ⇑f

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u
inst✝¹ : Finite α
inst✝ : DistribLattice α
val✝ : Fintype α
⊢ ∃ β x x_1 f, Injective ⇑f

Proof state:
case intro
α : Type u
inst✝¹ : Finite α
inst✝ : DistribLattice α
val✝ : Fintype α
⊢ ∃ β x x_1 f, Injective ⇑f

Tactic:
exact ⟨{a : α // SupIrred a}, _, inferInstance, _, LatticeHom.birkhoffFinset_injective⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem deriv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : deriv f x = 0

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x = 0

Tactic:
unfold deriv

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ (fderiv 𝕜 f x) 1 = 0

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ 0 1 = 0

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ (fderiv 𝕜 f x) 1 = 0

Tactic:
rw [fderiv_zero_of_not_differentiableAt h]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ 0 1 = 0
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem nontrivial [IsDomain R] (h : degree f ≠ 0) : Nontrivial (AdjoinRoot f) :=
  Ideal.Quotient.nontrivial
    (by
      simp_rw [Ne, span_singleton_eq_top, Polynomial.isUnit_iff, not_exists, not_and]
      rintro x hx rfl
      exact h (degree_C hx.ne_zero))

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : f.degree ≠ 0
⊢ span {f} ≠ ⊤

Tactic:
simp_rw [Ne, span_singleton_eq_top, Polynomial.isUnit_iff, not_exists, not_and]

Result:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : f.degree ≠ 0
⊢ ∀ (x : R), IsUnit x → ¬C x = f

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : f.degree ≠ 0
⊢ ∀ (x : R), IsUnit x → ¬C x = f

Tactic:
rintro x hx rfl

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : IsUnit x
h : (C x).degree ≠ 0
⊢ False

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : IsUnit x
h : (C x).degree ≠ 0
⊢ False

Tactic:
exact h (degree_C hx.ne_zero)

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem disjoint_union_left (x y z : Finmap β) :
    Disjoint (x ∪ y) z ↔ Disjoint x z ∧ Disjoint y z

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ (x ∪ y).Disjoint z ↔ x.Disjoint z ∧ y.Disjoint z

Tactic:
simp [Disjoint, Finmap.mem_union, or_imp, forall_and]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
lemma eventually_isCompact_closedBall [WeaklyLocallyCompactSpace α] (x : α) :
    ∀ᶠ r in 𝓝 (0 : ℝ), IsCompact (closedBall x r)

Proof state:
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)

Tactic:
rcases exists_compact_mem_nhds x with ⟨s, s_compact, hs⟩

Result:
case intro.intro
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)

Tactic:
filter_upwards [eventually_closedBall_subset hs] with r hr

Result:
case h
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
r : ℝ
hr : closedBall x r ⊆ s
⊢ IsCompact (closedBall x r)

Proof state:
case h
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
r : ℝ
hr : closedBall x r ⊆ s
⊢ IsCompact (closedBall x r)

Tactic:
exact IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Raised.add_left (k) {n m} (H : Raised n m) : Raised (k + n) (k + m)

Proof state:
case inl
k m : ℕ
⊢ Raised (k + m) (k + m)

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
case inr
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))

Tactic:
exact Or.inr rfl

Result:
no goals

Proof state:
k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
rcases H with (rfl | rfl)

Result:
case inl
k m : ℕ
⊢ Raised (k + m) (k + m)

case inr
k n : ℕ
⊢ Raised (k + n) (k + (n + 1))
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem gen_eq_preimage_restrict {𝔖} (S : Set α) (V : Set (β × β)) :
    UniformOnFun.gen 𝔖 S V =
      Prod.map (S.restrict ∘ UniformFun.toFun) (S.restrict ∘ UniformFun.toFun) ⁻¹'
        UniformFun.gen S β V

Proof state:
case h
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    uv ∈ Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V

Tactic:
exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
⊢ UniformOnFun.gen 𝔖 S V =
    Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V

Tactic:
ext uv

Result:
case h
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    uv ∈ Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma pairwise_disjoint_supp_connectedComponent (G : SimpleGraph V) :
    Pairwise fun c c' : ConnectedComponent G ↦ Disjoint c.supp c'.supp

Proof state:
V : Type u
G : SimpleGraph V
⊢ Pairwise fun c c' => ∀ ⦃a : V⦄, a ∈ c.supp → a ∉ c'.supp

Tactic:
intro _ _ h a hsx hsy

Result:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : a ∈ i✝.supp
hsy : a ∈ j✝.supp
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : G.connectedComponentMk a = j✝
⊢ False

Tactic:
rw [hsx] at hsy

Result:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : i✝ = j✝
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : i✝ = j✝
⊢ False

Tactic:
exact h hsy

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : a ∈ i✝.supp
hsy : a ∈ j✝.supp
⊢ False

Tactic:
rw [ConnectedComponent.mem_supp_iff] at hsx hsy

Result:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : G.connectedComponentMk a = j✝
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
⊢ Pairwise fun c c' => Disjoint c.supp c'.supp

Tactic:
simp_rw [Set.disjoint_left]

Result:
V : Type u
G : SimpleGraph V
⊢ Pairwise fun c c' => ∀ ⦃a : V⦄, a ∈ c.supp → a ∉ c'.supp
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_mul_left {a : Int} (a0 : a ≠ 0) : (a * n) /. (a * d) = n /. d

Proof state:
n d a : Int
a0 : a ≠ 0
⊢ a * n /. (a * d) = n /. d

Tactic:
if d0 : d = 0 then simp [d0] else
simp [divInt_eq_iff (Int.mul_ne_zero a0 d0) d0, Int.mul_assoc, Int.mul_left_comm]

Result:
no goals

Proof state:
n d a : Int
a0 : a ≠ 0
d0 : ¬d = 0
⊢ a * n /. (a * d) = n /. d

Tactic:
simp [divInt_eq_iff (Int.mul_ne_zero a0 d0) d0, Int.mul_assoc, Int.mul_left_comm]

Result:
no goals

Proof state:
n d a : Int
a0 : a ≠ 0
d0 : d = 0
⊢ a * n /. (a * d) = n /. d

Tactic:
simp [d0]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem coeff_mul_X_sub_C {p : R[X]} {r : R} {a : ℕ} :
    coeff (p * (X - C r)) (a + 1) = coeff p a - coeff p (a + 1) * r

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
a : ℕ
⊢ (p * (X - C r)).coeff (a + 1) = p.coeff a - p.coeff (a + 1) * r

Tactic:
simp [mul_sub]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem spectralRadius_le_pow_nnnorm_pow_one_div (a : A) (n : ℕ) :
    spectralRadius 𝕜 a ≤ (‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / (n + 1) : ℝ) *
      (‖(1 : A)‖₊ : ℝ≥0∞) ^ (1 / (n + 1) : ℝ)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
⊢ ↑(‖k‖₊ ^ (n + 1)) ≤ ↑‖a ^ (n + 1)‖₊ * ↑‖1‖₊

Tactic:
simpa only [Real.toNNReal_mul (norm_nonneg _), norm_toNNReal, nnnorm_pow k (n + 1),
  ENNReal.coe_mul] using coe_mono (Real.toNNReal_mono (norm_le_norm_mul_of_mem pow_mem))

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
⊢ ↑‖k‖₊ ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))

Tactic:
have pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1)) := by
  simpa only [one_mul, Algebra.algebraMap_eq_smul_one, one_smul, aeval_monomial, one_mul,
    eval_monomial] using subset_polynomial_aeval a (@monomial 𝕜 _ (n + 1) (1 : 𝕜)) ⟨k, hk, rfl⟩

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
⊢ ↑‖k‖₊ ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
/-- `±α` are the only `K`-multiples of a root `α` that are also (non-zero) roots. -/
lemma eq_neg_or_eq_of_eq_smul (hβ : β.IsNonZero) (k : K) (h : (β : H → K) = k • α) :
    β = -α ∨ β = α

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : ⇑β = -1 • ⇑α
⊢ β = -α

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : ⇑β = -1 • ⇑α
x✝ : ↥H
⊢ β x✝ = (-α) x✝

Proof state:
case neg.inr.inr
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : ⇑β = 1 • ⇑α
⊢ β = -α ∨ β = α

Tactic:
exact .inr (by ext; rw [h, one_smul])

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
/-- If `x` is rational, it can be written as `a / b` with `a : ℤ` and `b : ℕ` satisfying `b > 0`. -/
private lemma not_irrational_exists_rep {x : ℝ} :
    ¬Irrational x → ∃ (a : ℤ) (b : ℕ), 0 < b ∧ x = a / b

Proof state:
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
exact_mod_cast (Rat.num_div_den _).symm

Result:
no goals

Proof state:
x : ℝ
⊢ ¬Irrational x → ∃ a b, 0 < b ∧ x = ↑a / ↑b

Tactic:
rw [Irrational, not_not, mem_range]

Result:
x : ℝ
⊢ (∃ y, ↑y = x) → ∃ a b, 0 < b ∧ x = ↑a / ↑b

Proof state:
x : ℝ
⊢ (∃ y, ↑y = x) → ∃ a b, 0 < b ∧ x = ↑a / ↑b

Tactic:
rintro ⟨q, rfl⟩

Result:
case intro
q : ℚ
⊢ ∃ a b, 0 < b ∧ ↑q = ↑a / ↑b

Proof state:
case intro
q : ℚ
⊢ ∃ a b, 0 < b ∧ ↑q = ↑a / ↑b

Tactic:
exact ⟨q.num, q.den, q.pos, by exact_mod_cast (Rat.num_div_den _).symm⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_sub_of_degree_eq (h : degree p = degree q)
    (hlc : leadingCoeff p ≠ leadingCoeff q) :
    leadingCoeff (p - q) = leadingCoeff p - leadingCoeff q

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Tactic:
replace h : degree p = degree (-q) := by rwa [q.degree_neg]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ p.degree = (-q).degree

Tactic:
rwa [q.degree_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Tactic:
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Tactic:
replace hlc : leadingCoeff p + leadingCoeff (-q) ≠ 0 := by
  rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0

Tactic:
rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem acc [RelHomClass F r s] (f : F) (a : α) : Acc s (f a) → Acc r a

Proof state:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a

Tactic:
subst h

Result:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b : β
a : α
H : ∀ (y : β), s y (f a) → Acc s y
IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a
⊢ Acc r a

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
⊢ Acc s (f a) → Acc r a

Tactic:
generalize h : f a = b

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r a

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r a

Tactic:
intro ac

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a

Proof state:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b : β
a : α
H : ∀ (y : β), s y (f a) → Acc s y
IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a
⊢ Acc r a

Tactic:
exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a

Tactic:
induction ac generalizing a with | intro _ H IH => ?_

Result:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
F : Type u_5
inst✝¹ : FunLike F α β
inst✝ : RelHomClass F r s
f : F
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a
-- Mathlib/Data/NNReal/Basic.lean
theorem iSup_mul_le {a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, g i * h ≤ a) : iSup g * h ≤ a

Proof state:
ι : Sort u_2
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ i, g i * h ≤ a

Tactic:
exact ciSup_le' H

Result:
no goals

Proof state:
ι : Sort u_2
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ iSup g * h ≤ a

Tactic:
rw [iSup_mul]

Result:
ι : Sort u_2
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ i, g i * h ≤ a
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem not_summable_of_ratio_norm_eventually_ge {α : Type*} [SeminormedAddCommGroup α] {f : ℕ → α}
    {r : ℝ} (hr : 1 < r) (hf : ∃ᶠ n in atTop, ‖f n‖ ≠ 0)
    (h : ∀ᶠ n in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖) : ¬Summable f

Proof state:
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∃ a, ∀ b ≥ a, r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f

Tactic:
rcases h with ⟨N₀, hN₀⟩

Result:
case intro
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable fun n => f (n + N)

Tactic:
refine mt Summable.tendsto_atTop_zero
  fun h' ↦ not_tendsto_atTop_of_tendsto_nhds (tendsto_norm_zero.comp h') ?_

Result:
case intro.intro.intro
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ Tendsto ((fun a => ‖a‖) ∘ fun n => f (n + N)) atTop atTop

Proof state:
case intro.intro.intro.convert_3
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ‖f (i + N)‖ ≤ ‖f (i + 1 + N)‖

Tactic:
convert hN₀ (i + N) (hNN₀.trans (N.le_add_left i)) using 3

Result:
case h.e'_4.h.e'_3.h.e'_1
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ i + 1 + N = i + N + 1

Proof state:
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
⊢ ¬Summable f

Tactic:
rw [eventually_atTop] at h

Result:
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∃ a, ∀ b ≥ a, r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f