harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem prod_cyclotomic_eq_X_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type*) [CommRing R] :
    ∏ i ∈ Nat.divisors n, cyclotomic i R = X ^ n - 1

Proof state:
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1

Tactic:
have integer : ∏ i ∈ Nat.divisors n, cyclotomic i ℤ = X ^ n - 1 := by
  apply map_injective (Int.castRingHom ℂ) Int.cast_injective
  simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X,
    Polynomial.map_one, Polynomial.map_sub]
  exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')

Result:
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
integer : ∏ i ∈ n.divisors, cyclotomic i ℤ = X ^ n - 1
⊢ ∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1

Proof state:
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i ℤ = X ^ n - 1

Tactic:
apply map_injective (Int.castRingHom ℂ) Int.cast_injective

Result:
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ map (Int.castRingHom ℂ) (∏ i ∈ n.divisors, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (X ^ n - 1)

Proof state:
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ x ∈ n.divisors, cyclotomic' x ℂ = X ^ n - 1

Tactic:
exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')

Result:
no goals

Proof state:
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ map (Int.castRingHom ℂ) (∏ i ∈ n.divisors, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (X ^ n - 1)

Tactic:
simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X,
  Polynomial.map_one, Polynomial.map_sub]

Result:
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ x ∈ n.divisors, cyclotomic' x ℂ = X ^ n - 1

Proof state:
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
integer : ∏ i ∈ n.divisors, cyclotomic i ℤ = X ^ n - 1
⊢ ∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1

Tactic:
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one,
  Polynomial.map_pow, Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) integer

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedSup_of_isAntichain (hs : IsAntichain (· ≤ ·) (s : Set α)) (ha : a ∈ s) :
    truncatedSup s a = a

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedSup a ≤ a

Tactic:
simp_rw [truncatedSup_of_mem (subset_lowerClosure ha), sup'_le_iff, mem_filter]

Result:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ ∀ (b : α), b ∈ s ∧ a ≤ b → id b ≤ a

Proof state:
case intro
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ id b ≤ a

Tactic:
exact (hs.eq ha hb hab).ge

Result:
no goals

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ ∀ (b : α), b ∈ s ∧ a ≤ b → id b ≤ a

Tactic:
rintro b ⟨hb, hab⟩

Result:
case intro
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ id b ≤ a

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedSup a = a

Tactic:
refine le_antisymm ?_ le_truncatedSup

Result:
α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedSup a ≤ a
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_coeff {i : ℕ} :
    (integralNormalization p).coeff i =
      if p.degree = i then 1 else coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
this : p.coeff i = 0 → p.degree ≠ ↑i
⊢ p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
simp +contextual [sum_def, integralNormalization, coeff_monomial, this,
  mem_support_iff]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
have : p.coeff i = 0 → p.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
this : p.coeff i = 0 → p.degree ≠ ↑i
⊢ p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
-- Mathlib/FieldTheory/Differential/Basic.lean
@[simp]
lemma logDeriv_pow (n : ℕ) (a : R) : logDeriv (a ^ n) = n * logDeriv a

Proof state:
case succ.inl
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
n : ℕ
h2 : logDeriv (0 ^ n) = ↑n * logDeriv 0
⊢ logDeriv (0 ^ (n + 1)) = ↑(n + 1) * logDeriv 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = ↑n * logDeriv a
⊢ logDeriv (a ^ (n + 1)) = ↑(n + 1) * logDeriv a

Tactic:
obtain rfl | hb := eq_or_ne a 0

Result:
case succ.inl
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
n : ℕ
h2 : logDeriv (0 ^ n) = ↑n * logDeriv 0
⊢ logDeriv (0 ^ (n + 1)) = ↑(n + 1) * logDeriv 0

case succ.inr
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = ↑n * logDeriv a
hb : a ≠ 0
⊢ logDeriv (a ^ (n + 1)) = ↑(n + 1) * logDeriv a

Proof state:
case zero
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
⊢ logDeriv (a ^ 0) = ↑0 * logDeriv a

Tactic:
simp

Result:
no goals

Proof state:
case succ.inr
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
n : ℕ
h2 : logDeriv (a ^ n) = ↑n * logDeriv a
hb : a ≠ 0
⊢ logDeriv (a ^ (n + 1)) = ↑(n + 1) * logDeriv a

Tactic:
rw [Nat.cast_add, Nat.cast_one, add_mul, one_mul, ← h2, pow_succ, logDeriv_mul] <;>
simp [hb]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digit_sum_le (p n : ℕ) : List.sum (digits p n) ≤ n

Proof state:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Result:
no goals

Proof state:
case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ (digits 0 (n + 1)).sum ≤ n + 1

Tactic:
rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]

Result:
no goals

Proof state:
p n : ℕ
⊢ (p.digits n).sum ≤ n

Tactic:
induction' n with n

Result:
case zero
p : ℕ
⊢ (p.digits 0).sum ≤ 0

case succ
p n : ℕ
a✝ : (p.digits n).sum ≤ n
⊢ (p.digits (n + 1)).sum ≤ n + 1

Proof state:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
rw [← ofDigits_one <| digits p.succ n.succ]

Result:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))

Proof state:
case succ
p n : ℕ
a✝ : (p.digits n).sum ≤ n
⊢ (p.digits (n + 1)).sum ≤ n + 1

Tactic:
induction' p with p

Result:
case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ (digits 0 (n + 1)).sum ≤ n + 1

case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1

Proof state:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1

Tactic:
nth_rw 2 [← ofDigits_digits p.succ (n + 1)]

Result:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))

Proof state:
case zero
p : ℕ
⊢ (p.digits 0).sum ≤ 0

Tactic:
exact digits_zero _ ▸ Nat.le_refl (List.sum [])

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_setOf_Odd : schnirelmannDensity (setOf Odd) = 2⁻¹

Proof state:
⊢ schnirelmannDensity (setOf Odd) = 2⁻¹

Tactic:
have h : setOf Odd = {n | n % 2 = 1} := Set.ext fun _ => Nat.odd_iff

Result:
h : setOf Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity (setOf Odd) = 2⁻¹

Proof state:
h : setOf Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity {n | n % 2 = 1} = 2⁻¹

Tactic:
rw [schnirelmannDensity_setOf_mod_eq_one (by norm_num1), Nat.cast_two]

Result:
no goals

Proof state:
h : setOf Odd = {n | n % 2 = 1}
⊢ 2 ≠ 1

Tactic:
norm_num1

Result:
no goals

Proof state:
h : setOf Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity (setOf Odd) = 2⁻¹

Tactic:
simp only [h]

Result:
h : setOf Odd = {n | n % 2 = 1}
⊢ schnirelmannDensity {n | n % 2 = 1} = 2⁻¹
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_eq_mul_of_mem {s : Finset α} {f : α → β} (a b : α) (ha : a ∈ s) (hb : b ∈ s)
    (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : ∏ x ∈ s, f x = f a * f b

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
⊢ f c = 1

Tactic:
apply h₀ c hc

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a b : α
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq α
s' : Finset α := {a, b}
hu : s' ⊆ s
c : α
hc : c ∈ s
hcs : c ∉ s'
⊢ c ≠ a ∧ c ≠ b
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_induction (p : α → Prop) (s : Multiset α) (p_mul : ∀ a b, p a → p b → p (a * b))
    (p_one : p 1) (p_s : ∀ a ∈ s, p a) : p s.prod

Proof state:
α : Type u_3
inst✝ : CommMonoid α
p : α → Prop
s : Multiset α
p_mul : ∀ (a b : α), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ a ∈ s, p a
⊢ p s.prod

Tactic:
rw [prod_eq_foldr]

Result:
α : Type u_3
inst✝ : CommMonoid α
p : α → Prop
s : Multiset α
p_mul : ∀ (a b : α), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ a ∈ s, p a
⊢ p (foldr (fun x1 x2 => x1 * x2) 1 s)
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem pos_of_mem_rowLens (μ : YoungDiagram) (x : ℕ) (hx : x ∈ μ.rowLens) : 0 < x

Proof state:
μ : YoungDiagram
x : ℕ
hx : x ∈ μ.rowLens
⊢ 0 < x

Tactic:
rw [rowLens, List.mem_map] at hx

Result:
μ : YoungDiagram
x : ℕ
hx : ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x
⊢ 0 < x

Proof state:
case intro.intro
μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (μ.colLen 0)
⊢ 0 < μ.rowLen i

Tactic:
rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi

Result:
no goals

Proof state:
μ : YoungDiagram
x : ℕ
hx : ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x
⊢ 0 < x

Tactic:
obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx

Result:
case intro.intro
μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (μ.colLen 0)
⊢ 0 < μ.rowLen i
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem fun_eq_repr {x ζ : (𝓞 K)ˣ} {f : Fin (rank K) → ℤ} (hζ : ζ ∈ torsion K)
    (h : x = ζ * ∏ i, (fundSystem K i) ^ (f i)) :
    f = (basisModTorsion K).repr (Additive.ofMul ↑x)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
⊢ f = sorry

Tactic:
suffices Additive.ofMul ↑x = ∑ i, (f i) • (basisModTorsion K i) by
  rw [← (basisModTorsion K).repr_sum_self f, ← this]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
⊢ Additive.ofMul x = ∑ i : Fin (rank K), f i • sorry

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
⊢ Additive.ofMul x = ∑ i : Fin (rank K), f i • Additive.ofMul (fundSystem K i)

Tactic:
rw [h, QuotientGroup.mk_mul, (QuotientGroup.eq_one_iff _).mpr hζ, one_mul,
  QuotientGroup.mk_prod, ofMul_prod]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
⊢ Additive.ofMul (ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i) =
    ∑ i : Fin (rank K), f i • Additive.ofMul (fundSystem K i)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
⊢ ∑ i : Fin (rank K), f i • Additive.ofMul (fundSystem K i) = ∑ i : Fin (rank K), f i • sorry

Tactic:
simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
⊢ ∑ x : Fin (rank K), f x • Additive.ofMul (sorry K x) = ∑ i : Fin (rank K), f i • sorry

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
⊢ Additive.ofMul x = ∑ i : Fin (rank K), f i • sorry

Tactic:
calc
  Additive.ofMul ↑x
  _ = ∑ i, (f i) • Additive.ofMul ↑(fundSystem K i) := by
        rw [h, QuotientGroup.mk_mul, (QuotientGroup.eq_one_iff _).mpr hζ, one_mul,
          QuotientGroup.mk_prod, ofMul_prod]; rfl
  _ = ∑ i, (f i) • (basisModTorsion K i) := by
        simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem convs_eq_convs' [LinearOrderedField K] {c : ContFract K} :
    (↑c : GenContFract K).convs = (↑c : GenContFract K).convs'

Proof state:
case a.s_pos
K : Type u_1
inst✝ : LinearOrderedField K
c : ContFract K
n : ℕ
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
intro gp m _ s_nth_eq

Result:
case a.s_pos
K : Type u_1
inst✝ : LinearOrderedField K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
s_nth_eq : (↑↑c).s.get? m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b

Proof state:
case a
K : Type u_1
inst✝ : LinearOrderedField K
c : ContFract K
n : ℕ
⊢ (↑↑c).convs.get n = Stream'.get (↑↑c).convs' n

Tactic:
apply convs_eq_convs'

Result:
case a.s_pos
K : Type u_1
inst✝ : LinearOrderedField K
c : ContFract K
n : ℕ
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
c : ContFract K
⊢ (↑↑c).convs = (↑↑c).convs'

Tactic:
ext n

Result:
case a
K : Type u_1
inst✝ : LinearOrderedField K
c : ContFract K
n : ℕ
⊢ (↑↑c).convs.get n = Stream'.get (↑↑c).convs' n

Proof state:
case a.s_pos
K : Type u_1
inst✝ : LinearOrderedField K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
s_nth_eq : (↑↑c).s.get? m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b

Tactic:
exact ⟨zero_lt_one.trans_le ((c : SimpContFract K).property m gp.a
  (partNum_eq_s_a s_nth_eq)).symm.le, c.property m gp.b <| partDen_eq_s_b s_nth_eq⟩

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
protected lemma map_smul [AddCommMonoid U] [Module R U] (f : U →ₗ[R] V) {r : R}
    {x : HahnSeries Γ U} : (r • x).map f = r • ((x.map f) : HahnSeries Γ V)

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : HahnSeries Γ U
x✝ : Γ
⊢ ((r • x).map f).coeff x✝ = (r • x.map f).coeff x✝

Tactic:
simp

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : HahnSeries Γ U
⊢ (r • x).map f = r • x.map f

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : HahnSeries Γ U
x✝ : Γ
⊢ ((r • x).map f).coeff x✝ = (r • x.map f).coeff x✝
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem MonoidHomClass.isometry_iff_norm [MonoidHomClass 𝓕 E F] (f : 𝓕) :
    Isometry f ↔ ∀ x, ‖f x‖ = ‖x‖

Proof state:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
simp only [isometry_iff_dist_eq, dist_eq_norm_div, ← map_div]

Result:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ (∀ (x y : E), ‖f (x / y)‖ = ‖x / y‖) ↔ ∀ (x : E), ‖f x‖ = ‖x‖

Proof state:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
⊢ (∀ (x y : E), ‖f (x / y)‖ = ‖x / y‖) ↔ ∀ (x : E), ‖f x‖ = ‖x‖

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

Result:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∀ (x y : E), ‖f (x / y)‖ = ‖x / y‖
x : E
⊢ ‖f x‖ = ‖x‖

Proof state:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∀ (x y : E), ‖f (x / y)‖ = ‖x / y‖
x : E
⊢ ‖f x‖ = ‖x‖

Tactic:
simpa using h x 1

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.dep_of_ssubset (hI : M.IsBasis I X) (hIY : I ⊂ Y) (hYX : Y ⊆ X) : M.Dep Y

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
⊢ M.Dep Y

Tactic:
have : X ⊆ M.E := hI.subset_ground

Result:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ M.Dep Y

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ ¬M.Indep Y

Tactic:
exact fun hY ↦ hIY.ne (hI.eq_of_subset_indep hY hIY.subset hYX)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ M.Dep Y

Tactic:
rw [← not_indep_iff]

Result:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊂ Y
hYX : Y ⊆ X
this : X ⊆ M.E
⊢ ¬M.Indep Y
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integral_comp_inv_smul_of_nonneg (f : E → F) {R : ℝ} (hR : 0 ≤ R) :
    ∫ x, f (R⁻¹ • x) ∂μ = R ^ finrank ℝ E • ∫ x, f x ∂μ

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ finrank ℝ E • ∫ (x : E), f x ∂μ

Tactic:
rw [integral_comp_inv_smul μ f R, abs_of_nonneg (pow_nonneg hR _)]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem linearIndependent_le_span {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M)
    [Fintype w] (s : span R w = ⊤) : #ι ≤ Fintype.card w

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ range v ≤ ↑(span R w)

Tactic:
rw [s]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ range v ≤ ↑⊤

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
apply linearIndependent_le_span' v i w

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ range v ≤ ↑(span R w)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ range v ≤ ↑⊤

Tactic:
exact le_top

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_inter_Iic (a b c : α) : Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Proof state:
α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]

Result:
no goals
-- Mathlib/Data/Int/Basic.lean
lemma strongRec_of_ge :
    ∀ hn : m ≤ n, m.strongRec lt ge n = ge n hn fun k _ ↦ m.strongRec lt ge k

Proof state:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
hn : m ≤ n
⊢ Int.strongRec lt ge n = ge n hn fun k x => Int.strongRec lt ge k

Tactic:
rw [Int.strongRec, dif_neg (Int.not_lt.mpr hn)]

Result:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
hn : m ≤ n
⊢ ge n ⋯
      (n.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k x => ih k ⋯)
        fun n_1 x hn l x => hn l ⋯) =
    ge n hn fun k x => Int.strongRec lt ge k

Proof state:
case e_a
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
hn : m ≤ n
⊢ (n.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k x => ih k ⋯)
      fun n_1 x hn l x => hn l ⋯) =
    fun k x => Int.strongRec lt ge k

Tactic:
revert ih

Result:
case e_a
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
⊢ (∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1) →
    (n.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k x => ih k ⋯)
        fun n_1 x hn l x => hn l ⋯) =
      fun k x => Int.strongRec lt ge k