harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_eq_det_embeddingsMatrixReindex_pow_two
    [Algebra.IsSeparable K L] (e : ι ≃ (L →ₐ[K] E)) :
    algebraMap K E (discr K b) = (embeddingsMatrixReindex K E b e).det ^ 2

Proof state:
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
inst✝ : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ (algebraMap K E) (discr K b) = (embeddingsMatrixReindex K E b e).det ^ 2

Tactic:
rw [discr_def, RingHom.map_det, RingHom.mapMatrix_apply,
  traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul, det_transpose, pow_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_width_append (x : BitVec 0) (y : BitVec v) : x ++ y = y.cast (by omega)

Proof state:
case pred
v : Nat
x : BitVec 0
y : BitVec v
i✝ : Nat
a✝ : i✝ < 0 + v
⊢ (x ++ y).getLsbD i✝ = (BitVec.cast ⋯ y).getLsbD i✝

Tactic:
rw [getLsbD_append]

Result:
case pred
v : Nat
x : BitVec 0
y : BitVec v
i✝ : Nat
a✝ : i✝ < 0 + v
⊢ (if i✝ < v then y.getLsbD i✝ else x.getLsbD (i✝ - v)) = (BitVec.cast ⋯ y).getLsbD i✝

Proof state:
case pred
v : Nat
x : BitVec 0
y : BitVec v
i✝ : Nat
a✝ : i✝ < 0 + v
⊢ (if i✝ < v then y.getLsbD i✝ else x.getLsbD (i✝ - v)) = (BitVec.cast ⋯ y).getLsbD i✝

Tactic:
simpa using lt_of_getLsbD

Result:
no goals

Proof state:
v : Nat
x : BitVec 0
y : BitVec v
⊢ v = 0 + v

Tactic:
omega

Result:
no goals

Proof state:
v : Nat
x : BitVec 0
y : BitVec v
⊢ x ++ y = BitVec.cast ⋯ y

Tactic:
ext

Result:
case pred
v : Nat
x : BitVec 0
y : BitVec v
i✝ : Nat
a✝ : i✝ < 0 + v
⊢ (x ++ y).getLsbD i✝ = (BitVec.cast ⋯ y).getLsbD i✝
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_image (hf : Isometry f) (hd : 0 ≤ d ∨ Surjective f) (s : Set X) :
    μH[d] (f '' s) = μH[d] s

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ 0 ≤ d → Monotone fun r => r ^ d

Tactic:
exact ENNReal.monotone_rpow_of_nonneg

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ ((OuterMeasure.comap f) (OuterMeasure.mkMetric fun r => r ^ d)) s = (OuterMeasure.mkMetric fun r => r ^ d) s

Tactic:
rw [OuterMeasure.isometry_comap_mkMetric _ hf (hd.imp_left _)]

Result:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ 0 ≤ d → Monotone fun r => r ^ d

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ μH[d] (f '' s) = μH[d] s

Tactic:
simp only [hausdorffMeasure, ← OuterMeasure.coe_mkMetric, ← OuterMeasure.comap_apply]

Result:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ ((OuterMeasure.comap f) (OuterMeasure.mkMetric fun r => r ^ d)) s = (OuterMeasure.mkMetric fun r => r ^ d) s
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_symm (θ : Real.Angle) : (o.rotation θ).symm = o.rotation (-θ)

Proof state:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x✝ : V
⊢ (o.rotation θ).symm x✝ = (o.rotation (-θ)) x✝

Tactic:
simp [o.rotation_apply, o.rotation_symm_apply, sub_eq_add_neg]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ (o.rotation θ).symm = o.rotation (-θ)

Tactic:
ext

Result:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x✝ : V
⊢ (o.rotation θ).symm x✝ = (o.rotation (-θ)) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_one {l : List α} : l.take 1 = l.head?.toList

Proof state:
α : Type u_1
l : List α
⊢ take 1 l = l.head?.toList

Tactic:
induction l <;> simp

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean
theorem IsGδ.setOf_liouville : IsGδ { x | Liouville x }

Proof state:
⊢ IsGδ (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})

Tactic:
refine .iInter fun n => IsOpen.isGδ ?_

Result:
n : ℕ
⊢ IsOpen (⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})

Proof state:
n : ℕ
⊢ IsOpen (⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})

Tactic:
refine isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => ?_

Result:
n : ℕ
a b : ℤ
_hb : 1 < b
⊢ IsOpen (ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})

Proof state:
n : ℕ
a b : ℤ
_hb : 1 < b
⊢ IsOpen (ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})

Tactic:
exact isOpen_ball.inter isClosed_singleton.isOpen_compl

Result:
no goals

Proof state:
⊢ IsGδ {x | Liouville x}

Tactic:
rw [setOf_liouville_eq_iInter_iUnion]

Result:
⊢ IsGδ (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
-- Mathlib/Topology/Instances/Real/Defs.lean
theorem Real.uniformContinuous_neg : UniformContinuous (@Neg.neg ℝ _) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨_, ε0, fun _ _ h => by simpa only [abs_sub_comm, Real.dist_eq, neg_sub_neg] using h⟩

Proof state:
ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℝ
h : dist x✝¹ x✝ < ε
⊢ dist (-x✝¹) (-x✝) < ε

Tactic:
simpa only [abs_sub_comm, Real.dist_eq, neg_sub_neg] using h

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem goldConj_mul_gold : ψ * φ = -1

Proof state:
⊢ φ * ψ = -1

Tactic:
exact gold_mul_goldConj

Result:
no goals

Proof state:
⊢ ψ * φ = -1

Tactic:
rw [mul_comm]

Result:
⊢ φ * ψ = -1
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
/-- subsumed by `IdealSheafData.map_ideal` below. -/
private lemma map_ideal_basicOpen_of_eq
    {U V : X.affineOpens} (f : Γ(X, U)) (hV : V = X.affineBasicOpen f) :
    (I.ideal U).map (X.presheaf.map
        (homOfLE (X := X.Opens) (hV.trans_le (X.affineBasicOpen_le f))).op).hom =
      I.ideal V

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen f)

Tactic:
exact I.map_ideal_basicOpen _ _

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hV : V = X.affineBasicOpen f
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal V

Tactic:
subst hV

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen f)
-- Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
lemma opShiftFunctorEquivalence_zero_unitIso_hom_app (X : Cᵒᵖ) :
    (opShiftFunctorEquivalence C 0).unitIso.hom.app X =
      ((shiftFunctorZero C ℤ).hom.app X.unop).op ≫
      (((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop⟦(0 : ℤ)⟧').op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (opShiftFunctorEquivalence C 0).unitIso.hom.app X =
    ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.hom.app X).unop =
    (((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫
        ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op).unop

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.hom.app X).unop =
    (((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫
        ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op).unop

Tactic:
dsimp [opShiftFunctorEquivalence]

Result:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop ≫ (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop ≫ (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)

Tactic:
rw [shiftFunctorZero_op_inv_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
  shiftFunctorCompIsoId_zero_zero_hom_app, assoc]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast]
lemma cast_inv_of_ne_zero (hq : (q.num : α) ≠ 0) : (q⁻¹ : ℚ≥0) = (q⁻¹ : α)

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
hq : ↑q.num ≠ 0
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_eq_pow_single [DecidableEq M] (a : M) (h : ∀ a', a' ≠ a → a' ∈ l → a' = 1) :
    l.prod = a ^ l.count a :=
  _root_.trans (by rw [map_id]) (prod_map_eq_pow_single a id h)

Proof state:
M : Type u_4
inst✝¹ : Monoid M
l : List M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
⊢ l.prod = (map id l).prod

Tactic:
rw [map_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem denote_input_vec (s : RefVecEntry α len) {input : β s.aig len} {hcast} :
    ⟦(f s.aig input).aig, (s.vec.get idx hidx).cast hcast, assign⟧
      =
    ⟦s.aig, s.vec.get idx hidx, assign⟧ :=  by
  rw [denote_mem_prefix]
  rfl

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
idx : Nat
hidx : idx < len
s : RefVecEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦assign, { aig := s.aig, ref := { gate := ((s.vec.get idx hidx).cast hcast).gate, hgate := ?m.5317 } }⟧ =
    ⟦assign, { aig := s.aig, ref := s.vec.get idx hidx }⟧

α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
idx : Nat
hidx : idx < len
s : RefVecEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ((s.vec.get idx hidx).cast hcast).gate < s.aig.decls.size

Tactic:
rfl

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
idx : Nat
hidx : idx < len
s : RefVecEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦assign, { aig := (f s.aig input).aig, ref := (s.vec.get idx hidx).cast hcast }⟧ =
    ⟦assign, { aig := s.aig, ref := s.vec.get idx hidx }⟧

Tactic:
rw [denote_mem_prefix]

Result:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
idx : Nat
hidx : idx < len
s : RefVecEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ⟦assign, { aig := s.aig, ref := { gate := ((s.vec.get idx hidx).cast hcast).gate, hgate := ?m.5317 } }⟧ =
    ⟦assign, { aig := s.aig, ref := s.vec.get idx hidx }⟧

α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
idx : Nat
hidx : idx < len
s : RefVecEntry α len
input : β s.aig len
hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size
⊢ ((s.vec.get idx hidx).cast hcast).gate < s.aig.decls.size
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Tendsto.div {f : Filter α} {ma : α → ℝ≥0∞} {mb : α → ℝ≥0∞} {a b : ℝ≥0∞}
    (hma : Tendsto ma f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ 0) (hmb : Tendsto mb f (𝓝 b))
    (hb : b ≠ ∞ ∨ a ≠ ∞) : Tendsto (fun a => ma a / mb a) f (𝓝 (a / b))

Proof state:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ⊤ ∨ a ≠ ⊤
⊢ Tendsto (fun a => ma a / mb a) f (𝓝 (a / b))

Tactic:
apply Tendsto.mul hma _ (ENNReal.tendsto_inv_iff.2 hmb) _ <;> simp [ha, hb]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem frequently_prod_and {p : α → Prop} {q : β → Prop} :
    (∃ᶠ x in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ a in f, p a) ∧ ∃ᶠ b in g, q b

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b

Tactic:
simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_of_eventually_ge {u v : ℕ → ℝ≥0∞} {c : ℝ≥0∞} (hc : c ≠ 0)
    (h : ∀ᶠ n in atTop, c * u n ≤ v n) :
    expGrowthSup u ≤ expGrowthSup v

Proof state:
case inl
u v : ℕ → ℝ≥0∞
hc : ⊤ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ⊤ * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun x => ⊤) + expGrowthSup u

Tactic:
exact expGrowthInf_top ▸ le_add_of_nonneg_left le_top

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun x => c) + expGrowthSup u

Tactic:
rcases eq_top_or_lt_top c with rfl | c_top

Result:
case inl
u v : ℕ → ℝ≥0∞
hc : ⊤ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ⊤ * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun x => ⊤) + expGrowthSup u

case inr
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
c_top : c < ⊤
⊢ expGrowthSup u ≤ (expGrowthInf fun x => c) + expGrowthSup u

Proof state:
case inr
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
c_top : c < ⊤
⊢ expGrowthSup u ≤ (expGrowthInf fun x => c) + expGrowthSup u

Tactic:
rw [expGrowthInf_const hc c_top.ne, zero_add]

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
⊢ expGrowthSup u ≤ expGrowthSup v

Tactic:
apply (expGrowthSup_eventually_monotone h).trans' (le_expGrowthSup_mul'.trans' _)

Result:
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
⊢ expGrowthSup u ≤ (expGrowthInf fun x => c) + expGrowthSup u
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (h1) (assign1) :
    ⟦aig, ⟨start, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
⊢ ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true →
    State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true

Tactic:
have := go_sat aig start h1 assign1 (.empty aig)

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
this : State.Sat (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val
⊢ ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true →
    State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
this : CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf = true
⊢ ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true →
    State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true

Tactic:
simp [this]

Result:
no goals

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
this : State.Sat (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val
⊢ ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true →
    State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true

Tactic:
simp only [State.Sat, CNF.sat_def] at this

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
this : CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf = true
⊢ ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true →
    State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true
-- Mathlib/Topology/Basic.lean
theorem nhds_basis_closeds (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∉ s ∧ IsClosed s) compl :=
  ⟨fun t => (nhds_basis_opens x).mem_iff.trans <|
    compl_surjective.exists.trans <| by simp only [isOpen_compl_iff, mem_compl_iff]⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
t : Set X
⊢ (∃ x_1, (x ∈ x_1ᶜ ∧ IsOpen x_1ᶜ) ∧ x_1ᶜ ⊆ t) ↔ ∃ i, (x ∉ i ∧ IsClosed i) ∧ iᶜ ⊆ t

Tactic:
simp only [isOpen_compl_iff, mem_compl_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem modByMonic_zero (p : R[X]) : p %ₘ 0 = p :=
  letI := Classical.decEq R
  if h : Monic (0 : R[X]) then by
    haveI := monic_zero_iff_subsingleton.mp h
    simp [eq_iff_true_of_subsingleton]
  else by unfold modByMonic divModByMonicAux; rw [dif_neg h]

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this✝ : DecidableEq R := Classical.decEq R
h : Monic 0
this : Subsingleton R
⊢ p %ₘ 0 = p

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p %ₘ 0 = p

Tactic:
unfold modByMonic divModByMonicAux

Result:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          let_fun _wf := ⋯;
          let dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0);
          let_fun _wf := ⋯;
          let dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p

Tactic:
rw [dif_neg h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p %ₘ 0 = p

Tactic:
haveI := monic_zero_iff_subsingleton.mp h

Result:
R : Type u
inst✝ : Ring R
p : R[X]
this✝ : DecidableEq R := Classical.decEq R
h : Monic 0
this : Subsingleton R
⊢ p %ₘ 0 = p
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma eq_zero_of_absolutelyContinuous_of_mutuallySingular {μ ν : Measure α}
    (h_ac : μ ≪ ν) (h_ms : μ ⟂ₘ ν) :
    μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ = 0

Tactic:
rw [← Measure.MutuallySingular.self_iff]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ ⟂ₘ μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ ⟂ₘ μ

Tactic:
exact h_ms.mono_ac Measure.AbsolutelyContinuous.rfl h_ac

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem forall_subset_range_iff {f : α → β} {p : Set β → Prop} :
    (∀ s, s ⊆ range f → p s) ↔ ∀ s, p (f '' s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ s ⊆ range f, p s) ↔ ∀ a ∈ 𝒫 range f, p a

Tactic:
simp only [mem_powerset_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ s ⊆ range f, p s) ↔ ∀ (s : Set α), p (f '' s)

Tactic:
rw [← forall_mem_range, range_image]

Result:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ s ⊆ range f, p s) ↔ ∀ a ∈ 𝒫 range f, p a
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem compLp_zero (hg : LipschitzWith c g) (g0 : g 0 = 0) : hg.compLp g0 (0 : Lp E p μ) = 0

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ g ∘ ↑↑0 =ᶠ[ae μ] 0

Tactic:
filter_upwards [Lp.coeFn_zero E p μ] with _ ha

Result:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
a✝ : α
ha : ↑↑0 a✝ = 0 a✝
⊢ (g ∘ ↑↑0) a✝ = 0 a✝

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ hg.compLp g0 0 = 0

Tactic:
rw [Lp.eq_zero_iff_ae_eq_zero]

Result:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ ↑↑(hg.compLp g0 0) =ᶠ[ae μ] 0

Proof state:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
a✝ : α
ha : ↑↑0 a✝ = 0 a✝
⊢ (g ∘ ↑↑0) a✝ = 0 a✝

Tactic:
simp only [ha, g0, Function.comp_apply, Pi.zero_apply]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ ↑↑(hg.compLp g0 0) =ᶠ[ae μ] 0

Tactic:
apply (coeFn_compLp _ _ _).trans

Result:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
⊢ g ∘ ↑↑0 =ᶠ[ae μ] 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_eq_some_getD [LawfulBEq α] {a : α} {fallback : β a} :
    a ∈ m → m.get? a = some (m.getD a fallback)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
a : α
fallback : β a
⊢ a ∈ m → m.get? a = some (m.getD a fallback)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
@[simp] lemma edgeDisjointTriangles_bot : (⊥ : SimpleGraph α).EdgeDisjointTriangles

Proof state:
α : Type u_1
⊢ ⊥.EdgeDisjointTriangles

Tactic:
simp [EdgeDisjointTriangles]

Result:
no goals