harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_eq (p : MvPolynomial σ R) :
    p.totalDegree = p.support.sup fun m => Multiset.card (toMultiset m)

Proof state:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (fun s => s.sum fun x e => e) = fun m => (toMultiset m).card

Tactic:
funext m

Result:
case e_f.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (m.sum fun x e => e) = (toMultiset m).card

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (p.support.sup fun s => s.sum fun x e => e) = p.support.sup fun m => (toMultiset m).card

Tactic:
congr

Result:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (fun s => s.sum fun x e => e) = fun m => (toMultiset m).card

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = p.support.sup fun m => (toMultiset m).card

Tactic:
rw [totalDegree]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (p.support.sup fun s => s.sum fun x e => e) = p.support.sup fun m => (toMultiset m).card

Proof state:
case e_f.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ (m.sum fun x e => e) = (toMultiset m).card

Tactic:
exact (Finsupp.card_toMultiset _).symm

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem relabel_all (g : α → β ⊕ (Fin n)) {k} (φ : L.BoundedFormula α (k + 1)) :
    φ.all.relabel g = (φ.relabel g).all

Proof state:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ relabel g φ.all = (relabel g φ).all

Tactic:
rw [relabel, mapTermRel, relabel]

Result:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ (castLE ⋯ (mapTermRel (fun x t => Term.relabel (relabelAux g x) t) (fun x => id) (fun x => castLE ⋯) φ)).all =
    (mapTermRel (fun x t => Term.relabel (relabelAux g x) t) (fun x => id) (fun x => castLE ⋯) φ).all

Proof state:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ (castLE ⋯ (mapTermRel (fun x t => Term.relabel (relabelAux g x) t) (fun x => id) (fun x => castLE ⋯) φ)).all =
    (mapTermRel (fun x t => Term.relabel (relabelAux g x) t) (fun x => id) (fun x => castLE ⋯) φ).all

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem constantCoeff_wittStructureInt_zero (Φ : MvPolynomial idx ℤ) :
    constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ

Tactic:
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ

Tactic:
apply inj

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ (Int.castRingHom ℚ) m = (Int.castRingHom ℚ) n → m = n

Tactic:
exact Int.cast_inj.mp

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ Function.Injective ⇑(Int.castRingHom ℚ)

Tactic:
intro m n

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ (Int.castRingHom ℚ) m = (Int.castRingHom ℚ) n → m = n

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)

Tactic:
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
  constantCoeff_map]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem adj_of_mem_incidenceSet (h : a ≠ b) (ha : e ∈ G.incidenceSet a)
    (hb : e ∈ G.incidenceSet b) : G.Adj a b

Proof state:
V : Type u
G : SimpleGraph V
a b : V
e : Sym2 V
h : a ≠ b
ha : e ∈ G.incidenceSet a
hb : e ∈ G.incidenceSet b
⊢ G.Adj a b

Tactic:
rwa [← mk'_mem_incidenceSet_left_iff, ←
  Set.mem_singleton_iff.1 <| G.incidenceSet_inter_incidenceSet_subset h ⟨ha, hb⟩]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem span_singleton_prime {p : α} (hp : p ≠ 0) : IsPrime (span ({p} : Set α)) ↔ Prime p

Proof state:
α : Type u
inst✝ : CommSemiring α
p : α
hp : p ≠ 0
⊢ (span {p}).IsPrime ↔ Prime p

Tactic:
simp [isPrime_iff, Prime, span_singleton_eq_top, hp, mem_span_singleton]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_lt_div_iff_of_pos_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    a / b < a / c ↔ c < b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a / b < a / c ↔ c < b

Tactic:
simp only [div_eq_mul_inv, mul_lt_mul_left ha, inv_lt_inv₀ hb hc]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem verschiebung_mul_frobenius (x y : 𝕎 R) :
    verschiebung (x * frobenius y) = verschiebung x * y

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ verschiebung (x * frobenius y) = verschiebung x * y

Tactic:
have : IsPoly₂ p fun {R} [Rcr : CommRing R] x y ↦ verschiebung (x * frobenius y) :=
  IsPoly.comp₂ (hg := verschiebung_isPoly)
    (hf := IsPoly₂.comp (hh := mulIsPoly₂) (hf := idIsPolyI' p) (hg := frobenius_isPoly p))

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)
⊢ verschiebung (x * frobenius y) = verschiebung x * y

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung x * y
⊢ verschiebung (x * frobenius y) = verschiebung x * y

Tactic:
ghost_calc x y

Result:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ∀ (n : ℕ), (ghostComponent n) (verschiebung (x * frobenius y)) = (ghostComponent n) (verschiebung x * y)

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)
⊢ verschiebung (x * frobenius y) = verschiebung x * y

Tactic:
have : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y :=
  IsPoly₂.comp (hh := mulIsPoly₂) (hf := verschiebung_isPoly) (hg := idIsPolyI' p)

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung x * y
⊢ verschiebung (x * frobenius y) = verschiebung x * y

Proof state:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ∀ (n : ℕ), (ghostComponent n) (verschiebung (x * frobenius y)) = (ghostComponent n) (verschiebung x * y)

Tactic:
rintro ⟨⟩ <;> ghost_simp [mul_assoc]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gamma_one_half : HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Proof state:
case refine_1
m : ℕ
⊢ ¬1 / 2 = -↑m

Tactic:
exact ((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

Result:
no goals

Proof state:
⊢ HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)

Tactic:
have := HasDerivAt.complex_of_real
  (differentiableAt_Gamma _ ?_) Real.hasDerivAt_Gamma_one_half Gamma_ofReal

Result:
case refine_2
this : HasDerivAt Gamma ↑(-√π * (γ + 2 * Real.log 2)) ↑(1 / 2)
⊢ HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)

case refine_1

⊢ ∀ (m : ℕ), ↑(1 / 2) ≠ -↑m

Proof state:
case refine_1
m : ℕ
⊢ ↑(1 / 2) ≠ -↑m

Tactic:
rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]

Result:
case refine_1
m : ℕ
⊢ ¬1 / 2 = -↑m

Proof state:
case refine_1

⊢ ∀ (m : ℕ), ↑(1 / 2) ≠ -↑m

Tactic:
intro m

Result:
case refine_1
m : ℕ
⊢ ↑(1 / 2) ≠ -↑m

Proof state:
case refine_2
this : HasDerivAt Gamma ↑(-√π * (γ + 2 * Real.log 2)) ↑(1 / 2)
⊢ HasDerivAt Gamma (-↑√π * (↑γ + 2 * log 2)) (1 / 2)

Tactic:
simpa only [neg_mul, one_div, ofReal_neg, ofReal_mul, ofReal_add, ofReal_ofNat, ofNat_log,
  ofReal_inv] using this

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_Iic_mul_deriv_eq_deriv_mul
    (hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x)
    (huv' : IntegrableOn (u * v') (Iic a)) (hu'v : IntegrableOn (u' * v) (Iic a))
    (h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')) (h_infty : Tendsto (u * v) atBot (𝓝 b')) :
    ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x

Proof state:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x

Tactic:
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]

Result:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (a : ℝ) in Iic a, u a * v' a + u' a * v a ∂volume = a' - b'

Proof state:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (u * v') (Iic a) volume
hu'v : IntegrableOn (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x

Tactic:
rw [Pi.mul_def] at huv' hu'v

Result:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x

Proof state:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Iic a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ ∫ (a : ℝ) in Iic a, u a * v' a + u' a * v a ∂volume = a' - b'

Tactic:
simpa only [add_comm] using integral_Iic_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_mapAccumr :
    mapAccumr f₁ (mapAccumr f₂ xs s₂).snd s₁
    = let m := (mapAccumr (fun x s =>
        let r₂ := f₂ x s.snd
        let r₁ := f₁ r₂.snd s.fst
        ((r₁.fst, r₂.fst), r₁.snd)
      ) xs (s₁, s₂))
      (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
⊢ mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ =
    let m :=
      mapAccumr
        (fun x s =>
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs using Vector.revInductionOn generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_add_coe_bot (a : ℝ) :
    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, ⊥)

Proof state:
a : ℝ
⊢ ContinuousAt (fun p => p.1 + p.2) (↑a, ⊥)

Tactic:
simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap]
  using Tendsto.comp (continuousAt_add_bot_coe a) (continuous_swap.tendsto ((a : EReal), ⊥))

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem top_apply' (s : Set α) : (⊤ : OuterMeasure α) s = ⨅ _ : s = ∅, 0 :=
  s.eq_empty_or_nonempty.elim (fun h => by simp [h]) fun h => by simp [h, h.ne_empty]

Proof state:
α : Type u_1
s : Set α
h : s.Nonempty
⊢ ⊤ s = ⨅ (_ : s = ∅), 0

Tactic:
simp [h, h.ne_empty]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s = ∅
⊢ ⊤ s = ⨅ (_ : s = ∅), 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem toInductiveLimit_isometry (I : ∀ n, Isometry (f n)) (n : ℕ) :
    Isometry (toInductiveLimit I n) :=
  Isometry.of_dist_eq fun x y => by
    change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y
    rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
      leRecOn_self]

Proof state:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y

Tactic:
rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
  leRecOn_self]

Result:
no goals

Proof state:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ dist (toInductiveLimit I n x) (toInductiveLimit I n y) = dist x y

Tactic:
change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y

Result:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y
-- Mathlib/Algebra/Category/Ring/Instances.lean
theorem isLocalHom_of_iso {R S : CommRingCat} (f : R ≅ S) : IsLocalHom f.hom.hom :=
  { map_nonunit := fun a ha => by
      convert f.inv.hom.isUnit_map ha
      simp }

Proof state:
case h.e'_3
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit ((CommRingCat.Hom.hom f.hom) a)
⊢ a = (CommRingCat.Hom.hom f.inv) ((CommRingCat.Hom.hom f.hom) a)

Tactic:
simp

Result:
no goals

Proof state:
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit ((CommRingCat.Hom.hom f.hom) a)
⊢ IsUnit a

Tactic:
convert f.inv.hom.isUnit_map ha

Result:
case h.e'_3
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit ((CommRingCat.Hom.hom f.hom) a)
⊢ a = (CommRingCat.Hom.hom f.inv) ((CommRingCat.Hom.hom f.hom) a)
-- Mathlib/NumberTheory/LSeries/Basic.lean
/-- If the `LSeries` of `f` is summable at `s`, then `f = O(n^(re s))`. -/
lemma LSeriesSummable.isBigO_rpow {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) :
    f =O[atTop] fun n ↦ (n : ℝ) ^ s.re

Proof state:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ f =O[atTop] fun n => ↑n ^ s.re

Tactic:
obtain ⟨C, hC⟩ := h.le_const_mul_rpow

Result:
case intro
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
⊢ f =O[atTop] fun n => ↑n ^ s.re

Proof state:
case intro
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
⊢ f =O[atTop] fun n => ↑n ^ s.re

Tactic:
refine Asymptotics.IsBigO.of_bound C <| eventually_atTop.mpr ⟨1, fun n hn ↦ ?_⟩

Result:
case intro
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
n : ℕ
hn : n ≥ 1
⊢ ‖f n‖ ≤ C * ‖↑n ^ s.re‖

Proof state:
case h.e'_4.h.e'_6
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
n : ℕ
hn : n ≥ 1
⊢ ‖↑n ^ s.re‖ = ↑n ^ s.re

Tactic:
rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg n.cast_nonneg, abs_of_nonneg n.cast_nonneg]

Result:
no goals

Proof state:
case intro
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
n : ℕ
hn : n ≥ 1
⊢ ‖f n‖ ≤ C * ‖↑n ^ s.re‖

Tactic:
convert hC n (Nat.pos_iff_ne_zero.mp hn) using 2

Result:
case h.e'_4.h.e'_6
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
n : ℕ
hn : n ≥ 1
⊢ ‖↑n ^ s.re‖ = ↑n ^ s.re
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem dist_fixedPoint_fixedPoint_of_dist_le' (g : α → α) {x y} (hx : IsFixedPt f x)
    (hy : IsFixedPt g y) {C} (hfg : ∀ z, dist (f z) (g z) ≤ C) : dist x y ≤ C / (1 - K) :=
  calc
    dist x y = dist y x := dist_comm x y
    _ ≤ dist y (f y) / (1 - K) := hf.dist_le_of_fixedPoint y hx
    _ = dist (f y) (g y) / (1 - K)

Proof state:
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
g : α → α
x y : α
hx : IsFixedPt f x
hy : IsFixedPt g y
C : ℝ
hfg : ∀ (z : α), dist (f z) (g z) ≤ C
⊢ dist y (f y) / (1 - ↑K) = dist (f y) (g y) / (1 - ↑K)

Tactic:
rw [hy.eq, dist_comm]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem Subsingleton.congr {s : Cycle α} (h : Subsingleton s) :
    ∀ ⦃x⦄ (_hx : x ∈ s) ⦃y⦄ (_hy : y ∈ s), x = y

Proof state:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y

Tactic:
simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff,
  length_eq_zero, length_eq_one, Nat.not_lt_zero, false_or] at h

Result:
case h
α : Type u_1
l : List α
h : l = [] ∨ ∃ a, l = [a]
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y

Proof state:
case h
α : Type u_1
l : List α
h : l = [] ∨ ∃ a, l = [a]
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y

Tactic:
rcases h with (rfl | ⟨z, rfl⟩) <;> simp

Result:
no goals

Proof state:
α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
induction' s using Quot.inductionOn with l

Result:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y
-- Mathlib/Computability/NFA.lean
theorem toNFA_correct (M : DFA α σ) : M.toNFA.accepts = M.accepts

Proof state:
case h.mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) → x ∈ M.accepts

Tactic:
rintro ⟨S, hS₁, hS₂⟩

Result:
case h.mp.intro.intro
α : Type u
σ : Type v
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ M.toNFA.accept
hS₂ : S ∈ {M.evalFrom M.start x}
⊢ x ∈ M.accepts

Proof state:
α : Type u
σ : Type v
M : DFA α σ
⊢ M.toNFA.accepts = M.accepts

Tactic:
ext x

Result:
case h
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.toNFA.accepts ↔ x ∈ M.accepts

Proof state:
case h
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.toNFA.accepts ↔ x ∈ M.accepts

Tactic:
rw [NFA.mem_accepts, toNFA_start, toNFA_evalFrom_match]

Result:
case h
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) ↔ x ∈ M.accepts

Proof state:
case h
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) ↔ x ∈ M.accepts

Tactic:
constructor

Result:
case h.mp
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) → x ∈ M.accepts

case h.mpr
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}

Proof state:
case h.mp.intro.intro
α : Type u
σ : Type v
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ M.toNFA.accept
hS₂ : S ∈ {M.evalFrom M.start x}
⊢ x ∈ M.accepts

Tactic:
rwa [Set.mem_singleton_iff.mp hS₂] at hS₁

Result:
no goals

Proof state:
case h.mpr
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}

Tactic:
exact fun h => ⟨M.eval x, h, rfl⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
lemma AffineSubspace.right_mem_of_wbtw {s : AffineSubspace R P} (hxyz : Wbtw R x y z) (hx : x ∈ s)
    (hy : y ∈ s) (hxy : x ≠ y) : z ∈ s

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : (lineMap x z) ε ∈ s
hxy : x ≠ (lineMap x z) ε
hε : ε ≠ 0
⊢ z ∈ s

Tactic:
simpa [hε] using lineMap_mem ε⁻¹ hx hy

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
s : AffineSubspace R P
hxyz : Wbtw R x y z
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ z ∈ s

Tactic:
obtain ⟨ε, -, rfl⟩ := hxyz

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : (lineMap x z) ε ∈ s
hxy : x ≠ (lineMap x z) ε
⊢ z ∈ s

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : (lineMap x z) ε ∈ s
hxy : x ≠ (lineMap x z) ε
⊢ ε ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
hy : (lineMap x z) 0 ∈ s
hxy : x ≠ (lineMap x z) 0
⊢ False

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : (lineMap x z) ε ∈ s
hxy : x ≠ (lineMap x z) ε
⊢ z ∈ s

Tactic:
have hε : ε ≠ 0 := by rintro rfl; simp at hxy

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : (lineMap x z) ε ∈ s
hxy : x ≠ (lineMap x z) ε
hε : ε ≠ 0
⊢ z ∈ s

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
hy : (lineMap x z) 0 ∈ s
hxy : x ≠ (lineMap x z) 0
⊢ False

Tactic:
simp at hxy

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem y_mul_pos {a b : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (hbx : 0 < b.x)
    (hby : 0 < b.y) : 0 < (a * b).y

Proof state:
d : ℤ
a b : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
hbx : 0 < b.x
hby : 0 < b.y
⊢ 0 < (a * b).y

Tactic:
simp only [y_mul]

Result:
d : ℤ
a b : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
hbx : 0 < b.x
hby : 0 < b.y
⊢ 0 < a.x * b.y + a.y * b.x

Proof state:
d : ℤ
a b : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
hbx : 0 < b.x
hby : 0 < b.y
⊢ 0 < a.x * b.y + a.y * b.x

Tactic:
positivity

Result:
no goals