harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
/-- Reformulation of the reflection formula in terms of `Gammaℝ`. -/
lemma Gammaℝ_one_sub_mul_Gammaℝ_one_add (s : ℂ) :
    Gammaℝ (1 - s) * Gammaℝ (1 + s) = (cos (π * s / 2))⁻¹ :=
  calc Gammaℝ (1 - s) * Gammaℝ (1 + s)
  _ = (π ^ ((s - 1) / 2) * π ^ ((-1 - s) / 2)) *
        (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))

Proof state:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos (↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Tactic:
ring_nf

Result:
s : ℂ
⊢ ↑π ^ 0 * (cos (s * ↑π * (1 / 2)))⁻¹ = (cos (s * ↑π * (1 / 2)))⁻¹

Proof state:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2)) =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2)

Tactic:
rw [Complex.Gamma_mul_Gamma_one_sub, cpow_one]

Result:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (↑π / sin (↑π * ((1 - s) / 2))) =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π / sin (↑π / 2 - ↑π * s / 2)

Proof state:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (↑π / sin (↑π * ((1 - s) / 2))) =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π / sin (↑π / 2 - ↑π * s / 2)

Tactic:
ring_nf

Result:
no goals

Proof state:
s : ℂ
⊢ ↑π ^ 0 * (cos (s * ↑π * (1 / 2)))⁻¹ = (cos (s * ↑π * (1 / 2)))⁻¹

Tactic:
rw [cpow_zero, one_mul]

Result:
no goals

Proof state:
s : ℂ
⊢ ↑π ^ (-(1 - s) / 2) * Gamma ((1 - s) / 2) * (↑π ^ (-(1 + s) / 2) * Gamma ((1 + s) / 2)) =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))

Tactic:
ring_nf

Result:
no goals

Proof state:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Tactic:
simp_rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero),
  Complex.sin_pi_div_two_sub]

Result:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos (↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Proof state:
s : ℂ
⊢ (1 - s).Gammaℝ * (1 + s).Gammaℝ =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))

Tactic:
simp only [Gammaℝ_def]

Result:
s : ℂ
⊢ ↑π ^ (-(1 - s) / 2) * Gamma ((1 - s) / 2) * (↑π ^ (-(1 + s) / 2) * Gamma ((1 + s) / 2)) =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma binEntropy_pos (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < binEntropy p

Proof state:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Tactic:
have : 0 < 1 - p := sub_pos.2 hp₁

Result:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this : 0 < 1 - p
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Proof state:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this✝¹ : 0 < 1 - p
this✝ : 0 < log p⁻¹
this : 0 < log (1 - p)⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < binEntropy p

Tactic:
unfold binEntropy

Result:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Proof state:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this✝ : 0 < 1 - p
this : 0 < log p⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Tactic:
have : 0 < log (1 - p)⁻¹ := log_pos <| (one_lt_inv₀ ‹_›).2 (sub_lt_self _ hp₀)

Result:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this✝¹ : 0 < 1 - p
this✝ : 0 < log p⁻¹
this : 0 < log (1 - p)⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Proof state:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this : 0 < 1 - p
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Tactic:
have : 0 < log p⁻¹ := log_pos <| (one_lt_inv₀ hp₀).2 hp₁

Result:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this✝ : 0 < 1 - p
this : 0 < log p⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_def [DecidableEq σ] (p : MvPolynomial σ R) : p.vars = p.degrees.toFinset

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.vars = p.degrees.toFinset

Tactic:
rw [vars]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees.toFinset = p.degrees.toFinset

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees.toFinset = p.degrees.toFinset

Tactic:
convert rfl

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
lemma Real.summable_one_div_nat_add_rpow (a : ℝ) (s : ℝ) :
    Summable (fun n : ℕ ↦ 1 / |n + a| ^ s) ↔ 1 < s

Proof state:
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
⊢ ((fun x => 1 + (b - c) / x) ∘ fun x => id x + c) =ᶠ[atTop] fun x => (x + b) / (x + c)

Tactic:
filter_upwards [eventually_gt_atTop (-c)] with x hx

Result:
case h
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
this : Tendsto (fun x => 1 + (b - c) / x) atTop (𝓝 1)
x : ℝ
hx : -c < x
⊢ ((fun x => 1 + (b - c) / x) ∘ fun x => id x + c) x = (x + b) / (x + c)

Proof state:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ Tendsto (fun i => |↑i + b| ^ s / |↑i + c| ^ s) atTop (𝓝 1)

Tactic:
refine (?_ : Tendsto (fun x : ℝ ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)).comp
  tendsto_natCast_atTop_atTop

Result:
case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ Tendsto (fun x => |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)

Proof state:
a s : ℝ
this : ∀ (b c : ℝ), (Summable fun n => 1 / |↑n + b| ^ s) → Summable fun n => 1 / |↑n + c| ^ s
⊢ (Summable fun n => 1 / |↑n + a| ^ s) ↔ 1 < s

Tactic:
simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]

Result:
no goals

Proof state:
a s : ℝ
⊢ ∀ (b c : ℝ), (Summable fun n => 1 / |↑n + b| ^ s) → Summable fun n => 1 / |↑n + c| ^ s

Tactic:
refine fun b c h ↦ summable_of_isBigO_nat h (isBigO_of_div_tendsto_nhds ?_ 1 ?_)

Result:
case refine_1
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ ∀ᶠ (x : ℕ) in atTop, 1 / |↑x + b| ^ s = 0 → 1 / |↑x + c| ^ s = 0

case refine_2
a s b c : ℝ
h : Summable fun n => 1 / |↑n + b| ^ s
⊢ Tendsto ((fun n => 1 / |↑n + c| ^ s) / fun n => 1 / |↑n + b| ^ s) atTop (𝓝 1)
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_left_injOn {x : ℝ} (hx : x ≠ 0) : InjOn (fun y : ℝ => y ^ x) { y : ℝ | 0 ≤ y }

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y = z

Tactic:
rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
⊢ InjOn (fun y => y ^ x) {y | 0 ≤ y}

Tactic:
rintro y hy z hz (hyz : y ^ x = z ^ x)

Result:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y = z
-- Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean
theorem Module.rank_linearMap :
    Module.rank S (M →ₗ[R] N) = lift.{w} (Module.rank R M) * lift.{v} (Module.rank S N)

Proof state:
R : Type u
S : Type u'
M : Type v
N : Type w
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
inst✝³ : SMulCommClass R S N
inst✝² : StrongRankCondition R
inst✝¹ : StrongRankCondition S
inst✝ : Free S N
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)

Tactic:
rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
  ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_eq_map (p : α → Prop) (f : α → β) (l : Vector α n) (H) :
    @pmap _ _ _ p (fun a _ => f a) l H = map f l

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ pmap (fun a x => f a) { toArray := toArray✝, size_toArray := size_toArray✝ } H =
    map f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : α → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (fun a x => f a) l H = map f l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ pmap (fun a x => f a) { toArray := toArray✝, size_toArray := size_toArray✝ } H =
    map f { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Topology/Instances/ENat.lean
theorem tendsto_nhds_top_iff_natCast_lt {α : Type*} {l : Filter α} {f : α → ℕ∞} :
    Tendsto f l (𝓝 ⊤) ↔ ∀ n : ℕ, ∀ᶠ a in l, n < f a

Proof state:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ (∀ (i : ℕ∞), i ≠ ⊤ → ∀ᶠ (a : α) in l, f a ∈ Ioi i) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

Tactic:
exact Option.ball_ne_none

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

Tactic:
simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal]

Result:
α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ (∀ (i : ℕ∞), i ≠ ⊤ → ∀ᶠ (a : α) in l, f a ∈ Ioi i) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a
-- Mathlib/Analysis/Complex/Angle.lean
@[simp] lemma angle_mul_right (ha : a ≠ 0) (x y : ℂ) : angle (x * a) (y * a) = angle x y

Proof state:
a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (x * a) (y * a) = angle x y

Tactic:
simp [mul_comm, angle_mul_left ha]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem le_one_toAddSubmonoid : 1 ≤ (1 : Submodule R A).toAddSubmonoid

Proof state:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
⊢ 1 ≤ toAddSubmonoid 1

Tactic:
rintro x ⟨n, rfl⟩

Result:
case intro
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
n : ℕ
⊢ (Nat.castAddMonoidHom A) n ∈ toAddSubmonoid 1

Proof state:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
n : ℕ
⊢ ↑n • 1 = ↑n

Tactic:
rw [Nat.cast_smul_eq_nsmul, nsmul_one]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
n : ℕ
⊢ (Nat.castAddMonoidHom A) n ∈ toAddSubmonoid 1

Tactic:
exact ⟨n, show (n : R) • (1 : A) = n by rw [Nat.cast_smul_eq_nsmul, nsmul_one]⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.lowerBound?_exists [@TransCmp α cmp] [IsCut cmp cut] (h : Ordered cmp t) :
    (∃ x, t.lowerBound? cut = some x) ↔ ∃ x ∈ t, cut x ≠ .lt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
⊢ (∃ x, lowerBound? cut t = some x) ↔ ∃ x, x ∈ t ∧ cut x ≠ Ordering.lt

Tactic:
conv => enter [2, 1, x]; rw [Ne, ← Ordering.swap_inj]

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
⊢ (∃ x, lowerBound? cut t = some x) ↔ ∃ x, x ∈ t ∧ ¬(cut x).swap = Ordering.lt.swap

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
⊢ (∃ x, lowerBound? cut t = some x) ↔ ∃ x, x ∈ t ∧ ¬(cut x).swap = Ordering.lt.swap

Tactic:
rw [← reverse_reverse t, lowerBound?_reverse]

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
⊢ (∃ x, upperBound? (fun x => (cut x).swap) t.reverse = some x) ↔
    ∃ x, x ∈ t.reverse.reverse ∧ ¬(cut x).swap = Ordering.lt.swap
-- Mathlib/FieldTheory/Separable.lean
theorem separable_C_mul_X_pow_add_C_mul_X_add_C
    {n : ℕ} (a b c : R) (hn : (n : R) = 0) (hb : IsUnit b) :
    (C a * X ^ n + C b * X + C c).Separable

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
⊢ f.Separable

Tactic:
obtain ⟨e, hb⟩ := hb.exists_left_inv

Result:
case intro
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
⊢ f.Separable

Proof state:
case intro
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
⊢ -derivative f * f + (f + C e) * derivative f = 1

Tactic:
have hderiv : derivative f = C b := by
  simp [hn, f, map_add derivative, derivative_C, derivative_X_pow]

Result:
case intro
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
hderiv : derivative f = C b
⊢ -derivative f * f + (f + C e) * derivative f = 1

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
⊢ derivative f = C b

Tactic:
simp [hn, f, map_add derivative, derivative_C, derivative_X_pow]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
⊢ f.Separable

Tactic:
refine ⟨-derivative f, f + C e, ?_⟩

Result:
case intro
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
⊢ -derivative f * f + (f + C e) * derivative f = 1

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb : IsUnit b
⊢ (C a * X ^ n + C b * X + C c).Separable

Tactic:
set f := C a * X ^ n + C b * X + C c

Result:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
⊢ f.Separable

Proof state:
case intro
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
hderiv : derivative f = C b
⊢ -derivative f * f + (f + C e) * derivative f = 1

Tactic:
rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
  ← map_mul, hb, map_one]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem _root_.integral_eq_zero_of_forall_integral_inner_eq_zero (f : α → E) (hf : Integrable f μ)
    (hf_int : ∀ c : E, ∫ x, ⟪c, f x⟫ ∂μ = 0) : ∫ x, f x ∂μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ∀ (c : E), ∫ (x : α), inner c (f x) ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0

Tactic:
specialize hf_int (∫ x, f x ∂μ)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ∫ (x : α), inner (∫ (x : α), f x ∂μ) (f x) ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ∫ (x : α), inner (∫ (x : α), f x ∂μ) (f x) ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0

Tactic:
rwa [integral_inner hf, inner_self_eq_zero] at hf_int

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
theorem coeff_mem (hf : f.IsEisensteinAt 𝓟) {n : ℕ} (hn : n ≠ f.natDegree) : f.coeff n ∈ 𝓟

Proof state:
case inl
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₁ : n < f.natDegree
⊢ f.coeff n ∈ 𝓟

Tactic:
exact hf.mem h₁

Result:
no goals

Proof state:
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : n > f.natDegree
⊢ f.coeff n ∈ 𝓟

Tactic:
rw [coeff_eq_zero_of_natDegree_lt h₂]

Result:
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : n > f.natDegree
⊢ 0 ∈ 𝓟

Proof state:
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
⊢ f.coeff n ∈ 𝓟

Tactic:
rcases ne_iff_lt_or_gt.1 hn with h₁ | h₂

Result:
case inl
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₁ : n < f.natDegree
⊢ f.coeff n ∈ 𝓟

case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : n > f.natDegree
⊢ f.coeff n ∈ 𝓟

Proof state:
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : n > f.natDegree
⊢ 0 ∈ 𝓟

Tactic:
exact Ideal.zero_mem _

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem Disjoint.sdiff_eq_left (h : Disjoint a b) : a \ b = a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a \ b = a

Tactic:
conv_rhs => rw [← @sdiff_bot _ _ a]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a \ b = a \ ⊥

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a \ b = a \ ⊥

Tactic:
rw [← h.eq_bot, sdiff_inf_self_left]

Result:
no goals
-- Mathlib/Data/Finset/Slice.lean
theorem subset_powersetCard_univ_iff : 𝒜 ⊆ powersetCard r univ ↔ (𝒜 : Set (Finset α)).Sized r :=
  forall_congr' fun A => by rw [mem_powersetCard_univ, mem_coe]

Proof state:
α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
A : Finset α
⊢ A ∈ 𝒜 → A ∈ powersetCard r univ ↔ A ∈ ↑𝒜 → #A = r

Tactic:
rw [mem_powersetCard_univ, mem_coe]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem transcendental (i : ι) : Transcendental R (x i)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
⊢ Transcendental R (x i)

Tactic:
have := hx.comp ![i] (Function.injective_of_subsingleton _)

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ Transcendental R (x i)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ Transcendental R (x i)

Tactic:
have : AlgebraicIndependent R ![x i] := by rwa [← FinVec.map_eq] at this

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
this✝ : AlgebraicIndependent R (x ∘ ![i])
this : AlgebraicIndependent R ![x i]
⊢ Transcendental R (x i)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ AlgebraicIndependent R ![x i]

Tactic:
rwa [← FinVec.map_eq] at this

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
this✝ : AlgebraicIndependent R (x ∘ ![i])
this : AlgebraicIndependent R ![x i]
⊢ Transcendental R (x i)

Tactic:
rwa [← algebraicIndependent_iff_transcendental]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_modifyKey_self [EquivBEq α] {k : α} [Inhabited (β)] {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
    getValue! k (modifyKey k f l) = ((getValue? k l).map f).get!

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
k : α
inst✝ : Inhabited β
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValue! k (modifyKey k f l) = (Option.map f (getValue? k l)).get!

Tactic:
simp [getValue!_modifyKey, hl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem ofList_nil :
    ofList ([] : List ((a : α) × (β a))) = ∅

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ (Raw₀.empty.insertMany []).val.val = Raw₀.empty.val

Tactic:
rw [Raw₀.insertMany_empty_list_nil]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ ofList [] = ∅

Tactic:
simp_to_raw

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ (Raw₀.empty.insertMany []).val.val = Raw₀.empty.val
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem fst_eq_of_mem_zipIdx {x : α × Nat} {l : Vector α n} {k : Nat} (h : x ∈ zipIdx l k) :
    x.1 = l[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega)

Proof state:
α : Type u_1
n : Nat
x : α × Nat
k : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k
⊢ x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type ?u.28011
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd - k < n

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.28011
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
this : k ≤ x.snd
⊢ x.snd - k < n

Proof state:
α : Type ?u.28011
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
this : k ≤ x.snd
⊢ x.snd - k < n

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.28011
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
this✝ : k ≤ x.snd
this : x.snd < k + n
⊢ x.snd - k < n

Proof state:
α : Type ?u.28011
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
this✝ : k ≤ x.snd
this : x.snd < k + n
⊢ x.snd - k < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α × Nat
l : Vector α n
k : Nat
h : x ∈ l.zipIdx k
⊢ x.fst = l[x.snd - k]

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
x : α × Nat
k : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k
⊢ x.fst = { toArray := toArray✝, size_toArray := size_toArray✝ }[x.snd - k]

Proof state:
case mk
α : Type u_1
n : Nat
x : α × Nat
k : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.zipIdx k
⊢ x.fst = { toArray := toArray✝, size_toArray := size_toArray✝ }[x.snd - k]

Tactic:
exact Array.fst_eq_of_mem_zipIdx (by simpa using h)

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem zero_def : (0 : X[S⁻¹]) = 0 /ₒ 1

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : Zero X
inst✝ : MulAction R X
⊢ 0 = 0 /ₒ 1

Tactic:
with_unfolding_all rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : Zero X
inst✝ : MulAction R X
⊢ 0 = 0 /ₒ 1

Tactic:
rfl

Result:
no goals