harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_range_natCast_sub (n k : ℕ) :
    ∏ i ∈ range k, (n - i : α) = (∏ i ∈ range k, (n - i) : ℕ)

Proof state:
case inr
α : Type u_3
inst✝ : CommRing α
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
rw [← mem_range] at hnk

Result:
case inr
α : Type u_3
inst✝ : CommRing α
n k : ℕ
hnk : n ∈ range k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Proof state:
α : Type u_3
inst✝ : CommRing α
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
rcases le_or_lt k n with hkn | hnk

Result:
case inl
α : Type u_3
inst✝ : CommRing α
n k : ℕ
hkn : k ≤ n
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

case inr
α : Type u_3
inst✝ : CommRing α
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Proof state:
α : Type u_3
inst✝ : CommRing α
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ↑(∏ i ∈ range k, (n - i))

Tactic:
rw [prod_natCast]

Result:
α : Type u_3
inst✝ : CommRing α
n k : ℕ
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Proof state:
case inl
α : Type u_3
inst✝ : CommRing α
n k : ℕ
hkn : k ≤ n
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm

Result:
no goals

Proof state:
case inr
α : Type u_3
inst✝ : CommRing α
n k : ℕ
hnk : n ∈ range k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem nhds_eq_iInf_abs_sub (a : α) : 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| < r }

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a : α
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) =
    (⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}) ⊓ ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}

Tactic:
refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)

Result:
case refine_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) = ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}

case refine_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}

Proof state:
case refine_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.subLeft a) x > 0), 𝓟 {a_1 | a - a_1 < (Equiv.subLeft a) x} = ⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x)

Tactic:
simp [Ioi]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.subRight a) x > 0), 𝓟 {a_1 | -(Equiv.subRight a) x < a - a_1} = ⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x)

Tactic:
simp [Iio]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a : α
⊢ 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}

Tactic:
simp only [nhds_eq_order, abs_lt, setOf_and, ← inf_principal, iInf_inf_eq]

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a : α
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) =
    (⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}) ⊓ ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}

Proof state:
case refine_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) = ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | a - a_1 < x}

Tactic:
refine (Equiv.subLeft a).iInf_congr fun x => ?_

Result:
case refine_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.subLeft a) x > 0), 𝓟 {a_1 | a - a_1 < (Equiv.subLeft a) x} = ⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x)

Proof state:
case refine_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a : α
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = ⨅ x, ⨅ (_ : x > 0), 𝓟 {a_1 | -x < a - a_1}

Tactic:
refine (Equiv.subRight a).iInf_congr fun x => ?_

Result:
case refine_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.subRight a) x > 0), 𝓟 {a_1 | -(Equiv.subRight a) x < a - a_1} = ⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x)
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_subsieve_aux (P : Cᵒᵖ ⥤ Type w) {S : Sieve X} {R : Presieve X}
    (h : (S : Presieve X) ≤ R) (hS : IsSheafFor P (S : Presieve X))
    (trans : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (S.pullback f : Presieve Y)) :
    IsSheafFor P R

Proof state:
case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
⊢ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
intro x hx

Result:
case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_edist_self (f : WithLp p (α × β)) : edist f f = 0

Proof state:
case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp ⊤ (α × β)
⊢ edist f f = 0

Tactic:
simp [prod_edist_eq_sup]

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp 0 (α × β)
⊢ edist f f = 0

Tactic:
classical
simp

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
⊢ edist f f = 0

Tactic:
rcases p.trichotomy with (rfl | rfl | h)

Result:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp 0 (α × β)
⊢ edist f f = 0

case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp ⊤ (α × β)
⊢ edist f f = 0

case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f f = 0

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp 0 (α × β)
⊢ edist f f = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
simp [prod_edist_eq_add h, ENNReal.zero_rpow_of_pos h,
  ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigOWith.right_le_sub_of_lt_one {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) :
    IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x :=
  IsBigOWith.of_bound <|
    mem_of_superset h.bound fun x hx => by
      simp only [mem_setOf_eq] at hx ⊢
      rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]
      · exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _)
      · exact sub_pos.2 hc

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖

Tactic:
exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _)

Result:
no goals

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖

Tactic:
rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]

Result:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖

α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ 0 < 1 - c

Tactic:
exact sub_pos.2 hc

Result:
no goals

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : x ∈ {x | (fun x => ‖f₁ x‖ ≤ c * ‖f₂ x‖) x}
⊢ x ∈ {x | (fun x => ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖) x}

Tactic:
simp only [mem_setOf_eq] at hx ⊢

Result:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem IsSimpleModule.annihilator_isMaximal {R} [CommRing R] [Module R M]
    [simple : IsSimpleModule R M] : (Module.annihilator R M).IsMaximal

Proof state:
M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
⊢ (Module.annihilator R M).IsMaximal

Tactic:
have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple

Result:
M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
I : Ideal R
max : I.IsMaximal
e : M ≃ₗ[R] R ⧸ I
⊢ (Module.annihilator R M).IsMaximal

Proof state:
M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
I : Ideal R
max : I.IsMaximal
e : M ≃ₗ[R] R ⧸ I
⊢ (Module.annihilator R M).IsMaximal

Tactic:
rwa [e.annihilator_eq, I.annihilator_quotient]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k : α}
    (contains : containsKey k l = true) {h}:
    getKey k (insertListIfNewUnit l toInsert) h = getKey k l contains

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
contains : containsKey k l = true
h : containsKey k (insertListIfNewUnit l toInsert) = true
⊢ getKey k (insertListIfNewUnit l toInsert) h = getKey k l contains

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey, ← getKey?_eq_some_getKey,
  getKey?_insertListIfNewUnit_of_contains contains]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.

See `ENNReal.iInf_mul'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`. -/
lemma iInf_mul_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : (⨅ i, f i) * a = ⨅ i, f i * a :=
  iInf_mul' (by simp [ha]) (by simp [ha₀])

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = 0 → Nonempty ι

Tactic:
simp [ha₀]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem eq_pow_of_pow_eq_one {k : ℕ} [NeZero k] {ζ ξ : R} (h : IsPrimitiveRoot ζ k)
    (hξ : ξ ^ k = 1) :
    ∃ i < k, ζ ^ i = ξ

Proof state:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
lift ζ to Rˣ using h.isUnit <| NeZero.pos k

Result:
case intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ξ : R
hξ : ξ ^ k = 1
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ ∃ i < k, ↑ζ ^ i = ξ

Proof state:
case intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ξ : R
hξ : ξ ^ k = 1
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ ∃ i < k, ↑ζ ^ i = ξ

Tactic:
lift ξ to Rˣ using .of_pow_eq_one hξ <| NeZero.ne k

Result:
case intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i < k, ↑ζ ^ i = ↑ξ

Proof state:
case intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i < k, ↑ζ ^ i = ↑ξ

Tactic:
simp only [← Units.val_pow_eq_pow_val, ← Units.ext_iff]

Result:
case intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Proof state:
case intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
exact h.eq_pow_of_mem_rootsOfUnity <| (mem_rootsOfUnity' k ξ).mpr hξ

Result:
no goals

Proof state:
case intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
rw [coe_units_iff] at h

Result:
case intro.intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma strictAnti_sumCoeffsExp : StrictAnti (fun (p : ℝ) => ∑ i, a i * (b i) ^ p)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ StrictAnti fun p => ∑ i : α, a i * b i ^ p

Tactic:
rw [← Finset.sum_fn]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ StrictAnti (∑ c : α, fun p => a c * b c ^ p)

Proof state:
case terms
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : i ∈ univ
⊢ StrictAnti (HPow.hPow (b i))

Tactic:
exact Real.strictAnti_rpow_of_base_lt_one (R.b_pos i) (R.b_lt_one i)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ StrictAnti (∑ c : α, fun p => a c * b c ^ p)

Tactic:
refine Finset.sum_induction_nonempty _ _ (fun _ _ => StrictAnti.add) univ_nonempty ?terms

Result:
case terms
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ x ∈ univ, StrictAnti fun p => a x * b x ^ p

Proof state:
case terms
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ x ∈ univ, StrictAnti fun p => a x * b x ^ p

Tactic:
refine fun i _ => StrictAnti.const_mul ?_ (R.a_pos i)

Result:
case terms
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
x✝ : i ∈ univ
⊢ StrictAnti (HPow.hPow (b i))
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_X_add_C (a : R) : degree (X + C a) = 1

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : (C a).degree < X.degree
⊢ (X + C a).degree = 1

Tactic:
rw [degree_add_eq_left_of_degree_lt this, degree_X]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
⊢ (X + C a).degree = 1

Tactic:
have : degree (C a) < degree (X : R[X]) :=
  calc
    degree (C a) ≤ 0 := degree_C_le
    _ < 1 := WithBot.coe_lt_coe.mpr zero_lt_one
    _ = degree X := degree_X.symm

Result:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : (C a).degree < X.degree
⊢ (X + C a).degree = 1
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
theorem spineToSimplex_arrow (i : Fin n) (f : Path X n) :
    X.map (mkOfSucc i).op (spineToSimplex f) = f.arrow i

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ X.map (mkOfSucc i).op (spineToSimplex f) = f.arrow i

Tactic:
rw [← spine_arrow, spine_spineToSimplex]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
@[simp] lemma d_one (X : Dᵒᵖ) : d.d (X := X) 1 = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
d : M.Derivation φ
X : Dᵒᵖ
⊢ d.d 1 = 0

Tactic:
simpa using d.d_mul (X := X) 1 1

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_lt_of_lt_count {n k : ℕ} (h : k < count p n) : nth p k < n

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n

Tactic:
refine (count_monotone p).reflect_lt ?_

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ count p (nth p k) < count p n

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ count p (nth p k) < count p n

Tactic:
rwa [count_nth]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ ∀ (hf : (setOf p).Finite), k < #hf.toFinset

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ ∀ (hf : (setOf p).Finite), k < #hf.toFinset

Tactic:
exact fun hf => h.trans_le (count_le_card hf n)

Result:
no goals
-- Mathlib/Control/Traversable/Lemmas.lean
theorem traverse_map (f : β → F γ) (g : α → β) (x : t α) :
    traverse f (g <$> x) = traverse (f ∘ g) x

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f (traverse (pure ∘ g) x) = traverse (f ∘ g) x

Tactic:
refine (comp_traverse (G := Id) f (pure ∘ g) x).symm.trans ?_

Result:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x

Proof state:
case h.e_4.h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst✝¹

Tactic:
apply Comp.applicative_id_comp

Result:
no goals

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f (g <$> x) = traverse (f ∘ g) x

Tactic:
rw [@map_eq_traverse_id t _ _ _ _ g]

Result:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse f (traverse (pure ∘ g) x) = traverse (f ∘ g) x

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ traverse (Comp.mk ∘ map f ∘ pure ∘ g) x = traverse (f ∘ g) x

Tactic:
congr

Result:
case h.e_4.h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst✝¹
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem multiset_image_add_of_nonempty {F α β : Type*} [AddCommGroup α] [FunLike F α ℝ]
    [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean f)
    (g : β → α) {s : Multiset β} (hs : s ≠ 0) :
    ∃ b : β, (b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
hs : s ≠ 0
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Tactic:
obtain ⟨b, hbs, hbf⟩ := multiset_image_add hna g s

Result:
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
hs : s ≠ 0
b : β
hbs : s ≠ 0 → b ∈ s
hbf : f (Multiset.map g s).sum ≤ f (g b)
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Proof state:
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
hs : s ≠ 0
b : β
hbs : s ≠ 0 → b ∈ s
hbf : f (Multiset.map g s).sum ≤ f (g b)
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Tactic:
exact ⟨b, hbs hs, hbf⟩

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_X [DecidableEq σ] (i j : σ) [Nontrivial R] :
    degreeOf i (X j : MvPolynomial σ R) = if i = j then 1 else 0

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0

Tactic:
simp only [c, if_true, eq_self_iff_true, degreeOf_def, degrees_X, Multiset.count_singleton]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
⊢ degreeOf i (X j) = if i = j then 1 else 0

Tactic:
by_cases c : i = j

Result:
case pos
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0

case neg
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : ¬i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : ¬i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0

Tactic:
simp [c, if_false, degreeOf_def, degrees_X]

Result:
no goals
-- Mathlib/NumberTheory/ADEInequality.lean
theorem admissible_of_one_lt_sumInv_aux :
    ∀ {pqr : List ℕ+} (_ : pqr.Sorted (· ≤ ·)) (_ : pqr.length = 3) (_ : 1 < sumInv pqr),
      Admissible pqr
  | [p, q, r], hs, _, H => by
    obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r

Proof state:
p q r : ℕ+
hs : List.Sorted (fun x1 x2 => x1 ≤ x2) [p, q, r]
x✝ : [p, q, r].length = 3
H : 1 < sumInv ↑[p, q, r]
⊢ (p ≤ q ∧ p ≤ r) ∧ q ≤ r

Tactic:
simpa using hs

Result:
no goals

Proof state:
p q r : ℕ+
hs : List.Sorted (fun x1 x2 => x1 ≤ x2) [p, q, r]
x✝ : [p, q, r].length = 3
H : 1 < sumInv ↑[p, q, r]
⊢ Admissible ↑[p, q, r]

Tactic:
obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r := by simpa using hs

Result:
case intro.intro
p q r : ℕ+
hs : List.Sorted (fun x1 x2 => x1 ≤ x2) [p, q, r]
x✝ : [p, q, r].length = 3
H : 1 < sumInv ↑[p, q, r]
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible ↑[p, q, r]

Proof state:
case intro.intro
p q r : ℕ+
hs : List.Sorted (fun x1 x2 => x1 ≤ x2) [p, q, r]
x✝ : [p, q, r].length = 3
H : 1 < sumInv ↑[p, q, r]
hqr : q ≤ r
hpq : p ≤ q
⊢ Admissible ↑[p, q, r]

Tactic:
exact admissible_of_one_lt_sumInv_aux' hpq hqr H

Result:
no goals