harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_atTop_sumTransform_ge :
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ i, c * g n ≤ sumTransform (p a b) g (r i n) n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 > p a b + 1
⊢ ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) ≥
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1))

Tactic:
gcongr n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / ?_)

Result:
case h.h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 > p a b + 1
⊢ ↑(r i n) ^ (p a b + 1) ≤ (c₁ * ↑n) ^ (p a b + 1)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 > p a b + 1
⊢ 0 ≤ c₁

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/RingHom/Locally.lean
/-- In the definition of `Locally` we may replace `Localization.Away` with an arbitrary
algebra satisfying `IsLocalization.Away`. -/
lemma locally_iff_isLocalization (hP : RespectsIso P) (f : R →+* S) :
    Locally P f ↔ ∃ (s : Finset S) (_ : Ideal.span (s : Set S) = ⊤),
      ∀ t ∈ s, ∀ (Sₜ : Type u) [CommRing Sₜ] [Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)

Proof state:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
⊢ P ((algebraMap S Sₜ).comp f)

Tactic:
have : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t)) :=
  RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _) _).symm)

Result:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
this : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t))
⊢ P ((algebraMap S Sₜ).comp f)
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
theorem scaled_exp_map_periodic : Function.Periodic (fun x => Circle.exp (2 * π / T * x)) T

Proof state:
case inr
T : ℝ
hT : T ≠ 0
⊢ Periodic (fun x => Circle.exp (2 * π / T * x)) T

Tactic:
intro x

Result:
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ (fun x => Circle.exp (2 * π / T * x)) (x + T) = (fun x => Circle.exp (2 * π / T * x)) x

Proof state:
case inl
x : ℝ
⊢ (fun x => Circle.exp (2 * π / 0 * x)) (x + 0) = (fun x => Circle.exp (2 * π / 0 * x)) x

Tactic:
simp

Result:
no goals

Proof state:
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ (fun x => Circle.exp (2 * π / T * x)) (x + T) = (fun x => Circle.exp (2 * π / T * x)) x

Tactic:
simp_rw [mul_add]

Result:
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (2 * π / T * x + 2 * π / T * T) = Circle.exp (2 * π / T * x)

Proof state:
case inl

⊢ Periodic (fun x => Circle.exp (2 * π / 0 * x)) 0

Tactic:
intro x

Result:
case inl
x : ℝ
⊢ (fun x => Circle.exp (2 * π / 0 * x)) (x + 0) = (fun x => Circle.exp (2 * π / 0 * x)) x

Proof state:
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (2 * π / T * x + 2 * π / T * T) = Circle.exp (2 * π / T * x)

Tactic:
rw [div_mul_cancel₀ _ hT, Circle.periodic_exp]

Result:
no goals

Proof state:
T : ℝ
⊢ Periodic (fun x => Circle.exp (2 * π / T * x)) T

Tactic:
rcases eq_or_ne T 0 with (rfl | hT)

Result:
case inl

⊢ Periodic (fun x => Circle.exp (2 * π / 0 * x)) 0

case inr
T : ℝ
hT : T ≠ 0
⊢ Periodic (fun x => Circle.exp (2 * π / T * x)) T
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem toNNReal_eq_nnnorm_of_nonneg (hr : 0 ≤ r) : r.toNNReal = ‖r‖₊

Proof state:
r : ℝ
hr : 0 ≤ r
⊢ r.toNNReal = ‖r‖₊

Tactic:
rw [Real.toNNReal_of_nonneg hr]

Result:
r : ℝ
hr : 0 ≤ r
⊢ ⟨r, hr⟩ = ‖r‖₊

Proof state:
r : ℝ
hr : 0 ≤ r
⊢ ⟨r, hr⟩ = ‖r‖₊

Tactic:
ext

Result:
case a
r : ℝ
hr : 0 ≤ r
⊢ ↑⟨r, hr⟩ = ↑‖r‖₊

Proof state:
case a
r : ℝ
hr : 0 ≤ r
⊢ ↑⟨r, hr⟩ = ↑‖r‖₊

Tactic:
rw [coe_mk, coe_nnnorm r, Real.norm_eq_abs r, abs_of_nonneg hr]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem IsQuadratic.pow_char {χ : MulChar R R'} (hχ : χ.IsQuadratic) (p : ℕ) [hp : Fact p.Prime]
    [CharP R' p] : χ ^ p = χ

Proof state:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ χ ↑x ^ p = χ ↑x

Tactic:
rcases hχ x with (hx | hx | hx) <;> rw [hx]

Result:
case h.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 0
⊢ 0 ^ p = 0

case h.inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 1
⊢ 1 ^ p = 1

case h.inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
⊢ χ ^ p = χ

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ (χ ^ p) ↑x = χ ↑x

Proof state:
case h.inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1

Tactic:
exact neg_one_pow_char R' p

Result:
no goals

Proof state:
case h.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 0
⊢ 0 ^ p = 0

Tactic:
rw [zero_pow (@Fact.out p.Prime).ne_zero]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ (χ ^ p) ↑x = χ ↑x

Tactic:
rw [pow_apply_coe]

Result:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ χ ↑x ^ p = χ ↑x

Proof state:
case h.inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 1
⊢ 1 ^ p = 1

Tactic:
rw [one_pow]

Result:
no goals
-- Mathlib/RingTheory/Unramified/Basic.lean
theorem ext_of_iInf [FormallyUnramified R A] (hI : ⨅ i, I ^ i = ⊥) {g₁ g₂ : A →ₐ[R] B}
    (H : ∀ x, Ideal.Quotient.mk I (g₁ x) = Ideal.Quotient.mk I (g₂ x)) : g₁ = g₂

Proof state:
case pos
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : i = 0
⊢ (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂

Tactic:
ext x

Result:
case pos.H
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
i : ℕ
hi : i = 0
x : A
⊢ ((Ideal.Quotient.mkₐ R (I ^ i)).comp g₁) x = ((Ideal.Quotient.mkₐ R (I ^ i)).comp g₂) x
-- Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean
theorem pow_mul_meas_ge_le_eLpNorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    (hf : AEStronglyMeasurable f μ) (ε : ℝ≥0∞) :
    (ε * μ { x | ε ≤ (‖f x‖₊ : ℝ≥0∞) ^ p.toReal }) ^ (1 / p.toReal) ≤ eLpNorm f p μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
gcongr

Result:
case h₁
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal} ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ eLpNorm f p μ

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm hp_ne_zero hp_ne_top]

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Proof state:
case h₁
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal} ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
exact mul_meas_ge_le_lintegral₀ (hf.enorm.pow_const _) ε

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Stream.lean
theorem take_eq_takeTR : @take = @takeTR

Proof state:
⊢ @take = @takeTR

Tactic:
funext

Result:
case h.h.h.h.h
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ take x✝¹ x✝ = takeTR x✝¹ x✝

Proof state:
case h.h.h.h.h
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ take x✝¹ x✝ = takeTR x✝¹ x✝

Tactic:
ext : 1

Result:
case h.h.h.h.h.fst
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ (take x✝¹ x✝).fst = (takeTR x✝¹ x✝).fst

case h.h.h.h.h.snd
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ (take x✝¹ x✝).snd = (takeTR x✝¹ x✝).snd

Proof state:
case h.h.h.h.h.fst
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ (take x✝¹ x✝).fst = (takeTR x✝¹ x✝).fst

case h.h.h.h.h.snd
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ (take x✝¹ x✝).snd = (takeTR x✝¹ x✝).snd

Tactic:
rw [fst_takeTR]

Result:
case h.h.h.h.h.snd
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ (take x✝¹ x✝).snd = (takeTR x✝¹ x✝).snd

Proof state:
case h.h.h.h.h.snd
x✝⁴ : Type u_2
x✝³ : Type u_1
x✝² : Stream x✝⁴ x✝³
x✝¹ : x✝⁴
x✝ : Nat
⊢ (take x✝¹ x✝).snd = (takeTR x✝¹ x✝).snd

Tactic:
rw [snd_takeTR, snd_take_eq_drop]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
lemma map_symm_eq_iff_eq_map {M : BooleanSubalgebra β} {e : β ≃o α} :
    L.map ↑e.symm = M ↔ L = M.map ↑e

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ map
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L =
      M ↔
    L =
      map
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        M

Tactic:
simp_rw [← coe_inj]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ } M)

Tactic:
exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
lemma cochainsMap_f_map_mono (hf : Function.Surjective f) [Mono φ] (i : ℕ) :
    Mono ((cochainsMap f φ).f i)

Proof state:
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
hf : Function.Surjective ⇑f
inst✝ : Mono φ
i : ℕ
⊢ Mono ((cochainsMap f φ).f i)

Tactic:
simpa [ModuleCat.mono_iff_injective] using
  ((Rep.mono_iff_injective φ).1 inferInstance).comp_left.comp <|
  LinearMap.funLeft_injective_of_surjective k A _ hf.comp_left

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem units_apply_inv_apply (f : CircleDeg1Liftˣ) (x : ℝ) :
    f ((f⁻¹ : CircleDeg1Liftˣ) x) = x

Proof state:
f : CircleDeg1Liftˣ
x : ℝ
⊢ ↑f (↑f⁻¹ x) = x

Tactic:
simp only [← mul_apply, f.mul_inv, coe_one, id]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem order_single_mul_of_isRegular {g : Γ} {r : R} (hr : IsRegular r)
    {x : HahnSeries Γ R} (hx : x ≠ 0) : (((single g) r) * x).order = g + x.order

Proof state:
case inl
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
h✝ : Subsingleton R
⊢ ((single g) r * x).order = g + x.order

Tactic:
exact (hx <| Subsingleton.eq_zero x).elim

Result:
no goals

Proof state:
case inr
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ((single g) r * x).order = g + x.order

Tactic:
have hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0 := by
  rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_iff]

Result:
case inr
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
h✝ : Nontrivial R
hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0
⊢ ((single g) r * x).order = g + x.order

Proof state:
case inr
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
h✝ : Nontrivial R
hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0
⊢ ((single g) r * x).order = g + x.order

Tactic:
rw [order_mul_of_nonzero hrx, order_single <| IsRegular.ne_zero hr]

Result:
no goals

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
⊢ ((single g) r * x).order = g + x.order

Tactic:
obtain _|_ := subsingleton_or_nontrivial R

Result:
case inl
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
h✝ : Subsingleton R
⊢ ((single g) r * x).order = g + x.order

case inr
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ((single g) r * x).order = g + x.order

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : HahnSeries Γ R
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0

Tactic:
rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [HasSummableGeomSeries A] (a : A) :
    HasFPowerSeriesOnBall (fun z : 𝕜 => Ring.inverse (1 - z • a))
      (fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 ‖a‖₊⁻¹ :=
  { r_le

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
⊢ ‖y‖₊ < ‖a‖₊⁻¹

Tactic:
simpa only [← coe_inv h, mem_ball_zero_iff, Metric.emetric_ball_nnreal] using hy

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
@[reassoc (attr := simp)]
lemma tensorμ_tensorδ (X₁ X₂ Y₁ Y₂ : C) :
    tensorμ X₁ X₂ Y₁ Y₂ ≫ tensorδ X₁ X₂ Y₁ Y₂ = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
⊢ tensorμ X₁ X₂ Y₁ Y₂ ≫ tensorδ X₁ X₂ Y₁ Y₂ = 𝟙 ((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂)

Tactic:
simp only [tensorμ, tensorδ, assoc, Iso.inv_hom_id_assoc,
  ← MonoidalCategory.whiskerLeft_comp_assoc, Iso.hom_inv_id_assoc,
  hom_inv_whiskerRight_assoc, Iso.hom_inv_id, Iso.inv_hom_id,
  MonoidalCategory.whiskerLeft_id, id_comp]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
/-- Same as `add_comp` except that it uses `⇑κ + ⇑η` instead of `⇑(κ + η)` in order to have
a simp-normal form on the left of the equality. -/
@[simp]
lemma add_comp' : (⇑κ + ⇑η) ∘ₘ μ = κ ∘ₘ μ + η ∘ₘ μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ (⇑κ + ⇑η) ∘ₘ μ = ⇑κ ∘ₘ μ + ⇑η ∘ₘ μ

Tactic:
rw [← Kernel.coe_add, add_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem mkPiRing_eq_iff [Fintype ι] {z₁ z₂ : M₂} :
    MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂

Proof state:
case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
h : z₁ = z₂
⊢ ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂

Tactic:
intro x

Result:
case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
h : z₁ = z₂
x : ι → R
⊢ (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂

Proof state:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂

Tactic:
simp_rw [MultilinearMap.ext_iff, mkPiRing_apply]

Result:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂) ↔ z₁ = z₂

Proof state:
case mp
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
h : ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
⊢ z₁ = z₂

Tactic:
simpa using h fun _ => 1

Result:
no goals

Proof state:
case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
h : z₁ = z₂
x : ι → R
⊢ (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂) ↔ z₁ = z₂

Tactic:
constructor <;> intro h

Result:
case mp
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
h : ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
⊢ z₁ = z₂

case mpr
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
h : z₁ = z₂
⊢ ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
-- Mathlib/LinearAlgebra/Projection.lean
theorem codRestrict_apply_cod {f : M →ₗ[S] M} (h : IsProj m f) (x : m) : h.codRestrict x = x

Proof state:
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ h.codRestrict ↑x = x

Tactic:
ext

Result:
case a
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ ↑(h.codRestrict ↑x) = ↑x

Proof state:
case a
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ ↑(h.codRestrict ↑x) = ↑x

Tactic:
rw [codRestrict_apply]

Result:
case a
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ f ↑x = ↑x

Proof state:
case a
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : ↥m
⊢ f ↑x = ↑x

Tactic:
exact h.map_id x x.2

Result:
no goals