harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netEntropyEntourage_le_coverEntropyEntourage (T : X → X) (F : Set X) {U : Set (X × X)}
    (U_symm : SymmetricRel U) :
    netEntropyEntourage T F U ≤ coverEntropyEntourage T F U

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
⊢ ↑(netMaxcard T F U n) ≤ ↑(coverMincard T F U n)

Tactic:
exact ENat.toENNReal_le.2 (netMaxcard_le_coverMincard T F U_symm n)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
⊢ netEntropyEntourage T F U ≤ coverEntropyEntourage T F U

Tactic:
refine (limsup_le_limsup) (Eventually.of_forall fun n ↦ ?_)

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
⊢ (fun n => (↑(netMaxcard T F U n)).log / ↑n) n ≤ (fun n => (↑(coverMincard T F U n)).log / ↑n) n

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
⊢ (fun n => (↑(netMaxcard T F U n)).log / ↑n) n ≤ (fun n => (↑(coverMincard T F U n)).log / ↑n) n

Tactic:
apply div_le_div_right_of_nonneg (Nat.cast_nonneg' n) (log_monotone _)

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
⊢ ↑(netMaxcard T F U n) ≤ ↑(coverMincard T F U n)
-- Mathlib/Data/Complex/Exponential.lean
theorem norm_exp_sub_one_le {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖exp x - 1‖ ≤ 2 * ‖x‖ :=
  calc
    ‖exp x - 1‖ = ‖exp x - ∑ m ∈ range 1, x ^ m / m.factorial‖

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 1 * (↑(Nat.succ 1) * (↑(Nat.factorial 1) * ↑1)⁻¹) = 2 * ‖x‖

Tactic:
simp [two_mul, mul_two, mul_add, mul_comm, add_mul, Nat.factorial]

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1‖ = ‖cexp x - ∑ m ∈ range 1, x ^ m / ↑m.factorial‖

Tactic:
simp [sum_range_succ]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Icc_succ_pred_eq_Ioo (a b : α) : Icc (succ a) (pred b) = Ioo a b :=
  coe_injective <| by simpa using Set.Icc_succ_pred_eq_Ioo _ _

Proof state:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : LocallyFiniteOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
⊢ ↑(Icc (succ a) (pred b)) = ↑(Ioo a b)

Tactic:
simpa using Set.Icc_succ_pred_eq_Ioo _ _

Result:
no goals
-- Mathlib/Algebra/Order/Nonneg/Field.lean
@[simp] lemma mk_nnqsmul (q : ℚ≥0) (a : α) (ha : 0 ≤ a) :
    (⟨q • a, by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha⟩ : {x : α // 0 ≤ x}) =
      q • a := rfl

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
rw [NNRat.smul_def]

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a

Tactic:
exact mul_nonneg q.cast_nonneg ha

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_iff_eq_mul : a / b = c ↔ a = c * b

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / b = c ↔ a = c * b

Tactic:
rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_prod : Module.rank R (M × M') =
    Cardinal.lift.{v'} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M')

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Free R M'
⊢ Module.rank R (M × M') = lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M')

Tactic:
simpa [rank_eq_card_chooseBasisIndex R M, rank_eq_card_chooseBasisIndex R M', lift_umax]
  using ((chooseBasis R M).prod (chooseBasis R M')).mk_eq_rank.symm

Result:
no goals
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem card_fixingSubgroup_eq_finrank [DecidablePred (· ∈ IntermediateField.fixingSubgroup K)]
    [FiniteDimensional F E] [IsGalois F E] :
    Fintype.card (IntermediateField.fixingSubgroup K) = finrank K E

Proof state:
F : Type u_1
inst✝⁵ : Field F
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : IntermediateField F E
inst✝² : DecidablePred fun x => x ∈ K.fixingSubgroup
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
⊢ Fintype.card ↥K.fixingSubgroup = finrank (↥K) E

Tactic:
conv_rhs => rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem inv_mul (t : TransvectionStruct n R) : t.inv.toMatrix * t.toMatrix = 1

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
⊢ t.inv.toMatrix * t.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩

Result:
case mk
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ { i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix = 1

Proof state:
case mk
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
i✝ j✝ : n
t_hij : i✝ ≠ j✝
c✝ : R
⊢ { i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix = 1

Tactic:
simp [toMatrix, transvection_mul_transvection_same, t_hij]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem Functor.map_isPullback [PreservesLimit (cospan h i) F] (s : IsPullback f g h i) :
    IsPullback (F.map f) (F.map g) (F.map h) (F.map i)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)

Tactic:
refine
  IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)
      (isLimitOfPreserves F s.isLimit))

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅ ⋯.cone.pt

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    Iso.hom ?refine_1 ≫ ⋯.cone.π.app WalkingCospan.left

case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    Iso.hom ?refine_1 ≫ ⋯.cone.π.app WalkingCospan.right

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅ ⋯.cone.pt

Tactic:
rfl

Result:
no goals

Proof state:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.right

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    (Iso.refl ((Cones.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt).hom ≫
      ⋯.cone.π.app WalkingCospan.left

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma Equation.map {x y : R} (h : W'.Equation x y) : (W'.map f).toAffine.Equation (f x) (f y)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y : R
h : W'.Equation x y
⊢ (WeierstrassCurve.map W' f).toAffine.Equation (f x) (f y)

Tactic:
rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_iInf_rng {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} :
    Continuous[t₁, iInf t₂] f ↔ ∀ i, Continuous[t₁, t₂ i] f

Proof state:
α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ : ι → TopologicalSpace β
⊢ Continuous f ↔ ∀ (i : ι), Continuous f

Tactic:
simp only [continuous_iff_coinduced_le, le_iInf_iff]

Result:
no goals
-- Mathlib/Data/Matrix/Invertible.lean
@[simp] lemma isUnit_transpose : IsUnit Aᵀ ↔ IsUnit A

Proof state:
n : Type u_2
α : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring α
A : Matrix n n α
⊢ IsUnit Aᵀ ↔ IsUnit A

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
  (transposeInvertibleEquivInvertible A).nonempty_congr]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_inter_mulSupport_eq' (f : α → M) (s t : Set α)
    (h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t) : ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
apply finprod_mem_inter_mulSupport_eq

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
⊢ s ∩ mulSupport f = t ∩ mulSupport f

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
⊢ s ∩ mulSupport f = t ∩ mulSupport f

Tactic:
ext x

Result:
case h.h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f

Proof state:
case h.h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f

Tactic:
exact and_congr_left (h x)

Result:
no goals
-- Mathlib/RingTheory/KrullDimension/Basic.lean
/-- Alternative constructor for `Ring.KrullDimLE 1`, convenient for domains. -/
lemma Ring.KrullDimLE.mk₁' (H : ∀ I : Ideal R, I ≠ ⊥ → I.IsPrime → I.IsMaximal) :
    Ring.KrullDimLE 1 R

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 0 R

Tactic:
exact .mk₀ fun I hI ↦ H I (fun e ↦ hR (e ▸ hI)) hI

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ⊥.IsPrime
⊢ KrullDimLE 1 R

Tactic:
rwa [Ring.krullDimLE_one_iff_of_isPrime_bot]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
by_cases hR : (⊥ : Ideal R).IsPrime

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ⊥.IsPrime
⊢ KrullDimLE 1 R

case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 1 R

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 1 R

Tactic:
suffices Ring.KrullDimLE 0 R from inferInstance

Result:
case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 0 R
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem set_smul_sphere_zero {s : Set 𝕜} (hs : 0 ∉ s) (r : ℝ) :
    s • sphere (0 : E) r = (‖·‖) ⁻¹' ((‖·‖ * r) '' s) :=
  calc
    s • sphere (0 : E) r = ⋃ c ∈ s, c • sphere (0 : E) r := iUnion_smul_left_image.symm
    _ = ⋃ c ∈ s, sphere (0 : E) (‖c‖ * r) := iUnion₂_congr fun c hc ↦ by
      rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero]
    _ = (‖·‖) ⁻¹' ((‖·‖ * r) '' s)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
x✝ : E
⊢ x✝ ∈ ⋃ c ∈ s, sphere 0 (‖c‖ * r) ↔ x✝ ∈ (fun x => ‖x‖) ⁻¹' ((fun x => ‖x‖ * r) '' s)

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
⊢ c • sphere 0 r = sphere 0 (‖c‖ * r)

Tactic:
rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
⊢ ⋃ c ∈ s, sphere 0 (‖c‖ * r) = (fun x => ‖x‖) ⁻¹' ((fun x => ‖x‖ * r) '' s)

Tactic:
ext

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
x✝ : E
⊢ x✝ ∈ ⋃ c ∈ s, sphere 0 (‖c‖ * r) ↔ x✝ ∈ (fun x => ‖x‖) ⁻¹' ((fun x => ‖x‖ * r) '' s)
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem isNoetherian_coeIdeal [IsNoetherianRing R₁] (I : Ideal R₁) :
    IsNoetherian R₁ (I : FractionalIdeal R₁⁰ K)

Proof state:
case intro
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I J : Ideal R₁
hJ : ↑J ≤ ↑I
⊢ (↑↑J).FG

Tactic:
exact (IsNoetherian.noetherian J).map _

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ IsNoetherian R₁ ↥↑↑I

Tactic:
rw [isNoetherian_iff]

Result:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ ∀ J ≤ ↑I, (↑J).FG

Proof state:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
J : FractionalIdeal R₁⁰ K
hJ : J ≤ ↑I
⊢ (↑J).FG

Tactic:
obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp (le_trans hJ coeIdeal_le_one)

Result:
case intro
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I J : Ideal R₁
hJ : ↑J ≤ ↑I
⊢ (↑↑J).FG

Proof state:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
⊢ ∀ J ≤ ↑I, (↑J).FG

Tactic:
intro J hJ

Result:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsNoetherianRing R₁
I : Ideal R₁
J : FractionalIdeal R₁⁰ K
hJ : J ≤ ↑I
⊢ (↑J).FG
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_modify (h : m.1.WF) {k k' : α} {f : β → β} :
    (Const.modify m k f).getKey? k' =
      if k == k' then
        if m.contains k then some k else none
      else
        m.getKey? k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : β → β
⊢ (modify m k f).getKey? k' = if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'

Tactic:
simp_to_model [Const.modify] using List.Const.getKey?_modifyKey

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Sheaf/Limits.lean
lemma isSheaf_of_isLimit (hc : IsLimit c) (hF : ∀ j, Presheaf.IsSheaf J (F.obj j).presheaf) :
    Presheaf.IsSheaf J (c.pt.presheaf)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Cᵒᵖ ⥤ RingCat
F : D ⥤ PresheafOfModules R
inst✝¹ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
inst✝ : HasLimitsOfShape D AddCommGrp
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
⊢ Presheaf.IsSheaf J c.pt.presheaf

Tactic:
let G : D ⥤ Sheaf J AddCommGrp.{v} :=
  { obj := fun j => ⟨(F.obj j).presheaf, hF j⟩
    map := fun φ => ⟨(PresheafOfModules.toPresheaf R).map (F.map φ)⟩ }

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Cᵒᵖ ⥤ RingCat
F : D ⥤ PresheafOfModules R
inst✝¹ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
inst✝ : HasLimitsOfShape D AddCommGrp
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
G : D ⥤ Sheaf J AddCommGrp :=
  { obj := fun j => { val := (F.obj j).presheaf, cond := ⋯ },
    map := fun {X Y} φ => { val := (toPresheaf R).map (F.map φ) }, map_id := ⋯, map_comp := ⋯ }
⊢ Presheaf.IsSheaf J c.pt.presheaf

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
R : Cᵒᵖ ⥤ RingCat
F : D ⥤ PresheafOfModules R
inst✝¹ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
inst✝ : HasLimitsOfShape D AddCommGrp
hc : IsLimit c
hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf
G : D ⥤ Sheaf J AddCommGrp :=
  { obj := fun j => { val := (F.obj j).presheaf, cond := ⋯ },
    map := fun {X Y} φ => { val := (toPresheaf R).map (F.map φ) }, map_id := ⋯, map_comp := ⋯ }
⊢ Presheaf.IsSheaf J c.pt.presheaf

Tactic:
exact Sheaf.isSheaf_of_isLimit G _ (isLimitOfPreserves (toPresheaf R) hc)

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem StrictMono.pow_const (hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → StrictMono (f · ^ n)
  | 0, hn => (hn rfl).elim
  | 1, _ => by simpa
  | Nat.succ <| Nat.succ n, _ => by
    simpa only [pow_succ] using (hf.pow_const n.succ_ne_zero).mul' hf

Proof state:
β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
f : β → M
hf : StrictMono f
x✝ : 1 ≠ 0
⊢ StrictMono fun x => f x ^ 1

Tactic:
simpa

Result:
no goals

Proof state:
β : Type u_1
M : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Preorder M
inst✝² : Preorder β
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
f : β → M
hf : StrictMono f
n : ℕ
x✝ : n.succ.succ ≠ 0
⊢ StrictMono fun x => f x ^ n.succ.succ

Tactic:
simpa only [pow_succ] using (hf.pow_const n.succ_ne_zero).mul' hf

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem subtype_val {p : α → Prop} [DecidablePred p] {hp : PrimrecPred p} :
    haveI := Primcodable.subtype hp
    Primrec (@Subtype.val α p)

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
⊢ Primrec Subtype.val

Tactic:
letI := Primcodable.subtype hp

Result:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ Primrec Subtype.val

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ Primrec Subtype.val

Tactic:
refine (@Primcodable.prim (Subtype p)).of_eq fun n => ?_

Result:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode (decode n) = encode (Option.map Subtype.val (decode n))

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode (decode n) = encode (Option.map Subtype.val (decode n))

Tactic:
rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩) <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_pi_add (θ : Angle) : ((π : Angle) + θ).sign = -θ.sign

Proof state:
θ : Angle
⊢ (↑π + θ).sign = -θ.sign

Tactic:
rw [add_comm, sign_add_pi]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Groebner.lean
theorem degree_sub_LTerm_le (f : MvPolynomial σ R) :
    m.degree (m.subLTerm f) ≼[m] m.degree f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree ((monomial (m.degree f)) (m.leadingCoeff f))) ≤ m.toSyn (m.degree f)

Tactic:
apply degree_monomial_le

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (m.subLTerm f)) ≤ m.toSyn (m.degree f)

Tactic:
apply le_trans degree_sub_le

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree ((monomial (m.degree f)) (m.leadingCoeff f))) ≤ m.toSyn (m.degree f)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree ((monomial (m.degree f)) (m.leadingCoeff f))) ≤ m.toSyn (m.degree f)

Tactic:
simp only [sup_le_iff, le_refl, true_and]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree ((monomial (m.degree f)) (m.leadingCoeff f))) ≤ m.toSyn (m.degree f)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).1.size = if m.contains k then m.1.size else m.1.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).val.size = if m.contains k = true then m.val.size else m.val.size + 1

Tactic:
simp_to_model [insert] using List.length_insertEntry

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem cancel_left {g : β →*o γ} {f₁ f₂ : α →*o β} (hg : Function.Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.eventually_iff (hl : l.HasBasis p s) {q : α → Prop} :
    (∀ᶠ x in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x⦄, x ∈ s i → q x

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ᶠ (x : α) in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x

Tactic:
simpa using hl.mem_iff

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem AddContent.extend_eq_top (hC : IsSetSemiring C) (m : AddContent C) (hs : s ∉ C) :
    m.extend hC s = ∞

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
hs : s ∉ C
⊢ (AddContent.extend hC m) s = ⊤

Tactic:
rwa [m.extend_eq_extend, extend_eq_top]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_eq_nat_iff_finset {n : ℕ} :
    #α = n ↔ ∃ t : Finset α, (t : Set α) = univ ∧ t.card = n

Proof state:
α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
rw [← mk_univ, mk_set_eq_nat_iff_finset]

Result:
no goals