harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
@[simp]
lemma Gammaℂ_one : Gammaℂ 1 = 1 / π

Proof state:
⊢ 2 * (2 * ↑π)⁻¹ * 1 = 1 / ↑π

Tactic:
field_simp [pi_ne_zero]

Result:
no goals

Proof state:
⊢ Gammaℂ 1 = 1 / ↑π

Tactic:
rw [Gammaℂ_def, cpow_neg_one, Complex.Gamma_one]

Result:
⊢ 2 * (2 * ↑π)⁻¹ * 1 = 1 / ↑π
-- Mathlib/NumberTheory/ZetaValues.lean
theorem fourierCoeff_bernoulli_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) :
    fourierCoeff ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) n = -k ! / (2 * π * I * n) ^ k

Proof state:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeffOn ⋯ (ofReal ∘ bernoulliFun k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
simpa only [zero_add] using bernoulliFourierCoeff_eq hk n

Result:
no goals

Proof state:
case h
k : ℕ
hk : k ≠ 0
n : ℤ
x : 𝕌
⊢ (ofReal ∘ periodizedBernoulli k) x = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k) x

Tactic:
rfl

Result:
no goals

Proof state:
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)

Tactic:
ext1 x

Result:
case h
k : ℕ
hk : k ≠ 0
n : ℤ
x : 𝕌
⊢ (ofReal ∘ periodizedBernoulli k) x = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k) x

Proof state:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
rw [this, fourierCoeff_liftIco_eq]

Result:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeffOn ⋯ (ofReal ∘ bernoulliFun k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Proof state:
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
have : ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) = AddCircle.liftIco 1 0 ((↑) ∘ bernoulliFun k) := by
  ext1 x; rfl

Result:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma div_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s / t ⊆ range m

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s / t ⊆ range ⇑m

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩

Result:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (fun x1 x2 => x1 / x2) a b ∈ range ⇑m

Proof state:
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
b : β
hb : b ∈ t
a : α
ha : m a ∈ s
⊢ (fun x1 x2 => x1 / x2) (m a) b ∈ range ⇑m

Tactic:
obtain ⟨b, rfl⟩ := ht hb

Result:
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : α
ha : m a ∈ s
b : α
hb : m b ∈ t
⊢ (fun x1 x2 => x1 / x2) (m a) (m b) ∈ range ⇑m

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (fun x1 x2 => x1 / x2) a b ∈ range ⇑m

Tactic:
obtain ⟨a, rfl⟩ := hs ha

Result:
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
b : β
hb : b ∈ t
a : α
ha : m a ∈ s
⊢ (fun x1 x2 => x1 / x2) (m a) b ∈ range ⇑m

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : α
ha : m a ∈ s
b : α
hb : m b ∈ t
⊢ (fun x1 x2 => x1 / x2) (m a) (m b) ∈ range ⇑m

Tactic:
exact ⟨a / b, map_div ..⟩

Result:
no goals
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma ε₁_ε₂ {i₁ i₁' : I₁} {i₂ i₂' : I₂} (h₁ : c₁.Rel i₁ i₁') (h₂ : c₂.Rel i₂ i₂') :
    ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ * ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ =
      - ε₂ c₁ c₂ c₁₂ ⟨i₁', i₂⟩ * ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ :=
  Eq.trans (mul_one _).symm (by
    rw [← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')), mul_assoc]
    conv_lhs =>
      arg 2
      rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]
    rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
      Int.units_mul_self, one_mul])

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁, i₂) * 1 = -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
rw [← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')), mul_assoc]

Result:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc,
  Int.units_mul_self, one_mul]

Result:
no goals

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * (c₁.ε₁ c₂ c₁₂ (i₁, i₂') * c₁.ε₁ c₂ c₁₂ (i₁, i₂'))) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')

Tactic:
conv_lhs =>
  arg 2
  rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]

Result:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel i₁ i₁'
h₂ : c₂.Rel i₂ i₂'
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) * (-c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')) =
    -c₁.ε₂ c₂ c₁₂ (i₁', i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂')
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_of_matrix_vecMul (b : ι → B) (P : Matrix ι ι A) :
    discr A (b ᵥ* P.map (algebraMap A B)) = P.det ^ 2 * discr A b

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ discr A (b ᵥ* P.map ⇑(algebraMap A B)) = P.det ^ 2 * discr A b

Tactic:
rw [discr_def, traceMatrix_of_matrix_vecMul, det_mul, det_mul, det_transpose, mul_comm, ←
  mul_assoc, discr_def, pow_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_filter (p q : α → Bool) (l : List α) :
    (l.filter p).takeWhile q = (l.takeWhile fun a => !p a || q a).filter p

Proof state:
α : Type u_1
p q : α → Bool
l : List α
⊢ takeWhile q (filter p l) = filter p (takeWhile (fun a => !p a || q a) l)

Tactic:
simp [← filterMap_eq_filter, takeWhile_filterMap]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_ite_eq (b : β) [DecidablePred (· = b)] (a : α) :
    ∏' b', (if b' = b then a else 1) = a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ ∀ (b' : β), b' ≠ b → (if b' = b then a else 1) = 1

Tactic:
intro b' hb'

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a else 1) = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ (∏' (b' : β), if b' = b then a else 1) = a

Tactic:
rw [tprod_eq_mulSingle b]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ (if b = b then a else 1) = a

α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ ∀ (b' : β), b' ≠ b → (if b' = b then a else 1) = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a else 1) = 1

Tactic:
simp [hb']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ (if b = b then a else 1) = a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_div_iff_mul_eq_mul : a / b = c / d ↔ a * d = c * b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']

Result:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b

Tactic:
simp only [mul_comm, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
lemma star_lt_iff {x y : R} : star x < y ↔ x < star y

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
⊢ star x < y ↔ x < star y

Tactic:
rw [← star_lt_star_iff, star_star]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem natCast (n : ℕ) : mapFun f (n : 𝕎 R) = n :=
  show mapFun f n.unaryCast = (n : WittVector p S) by
    induction n <;> simp [*, Nat.unaryCast, add, one, zero] <;> rfl

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
⊢ mapFun (⇑f) n.unaryCast = ↑n

Tactic:
induction n <;> simp [*, Nat.unaryCast, add, one, zero] <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Tower.lean
theorem Algebra.fg_trans' {R S A : Type*} [CommSemiring R] [CommSemiring S] [Semiring A]
    [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).FG)
    (hSA : (⊤ : Subalgebra S A).FG) : (⊤ : Subalgebra R A).FG

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R ↑(Finset.image (⇑(algebraMap S A)) s ∪ t) = ⊤

Tactic:
rw [Finset.coe_union, Finset.coe_image,
    Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
    hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
    Subalgebra.restrictScalars_top
   ]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ ⊤.FG

Tactic:
exact ⟨s.image (algebraMap S A) ∪ t, by
  rw [Finset.coe_union, Finset.coe_image,
      Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
      hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
      Subalgebra.restrictScalars_top
     ]
  ⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hRS : ⊤.FG
hSA : ⊤.FG
⊢ ⊤.FG

Tactic:
rcases hRS with ⟨s, hs⟩

Result:
case intro
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hSA : ⊤.FG
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ⊤.FG

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hRS : ⊤.FG
hSA : ⊤.FG
⊢ ⊤.FG

Tactic:
classical
rcases hRS with ⟨s, hs⟩
rcases hSA with ⟨t, ht⟩
exact ⟨s.image (algebraMap S A) ∪ t, by
  rw [Finset.coe_union, Finset.coe_image,
      Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
      hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
      Subalgebra.restrictScalars_top
     ]
  ⟩

Result:
no goals

Proof state:
case intro
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hSA : ⊤.FG
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ⊤.FG

Tactic:
rcases hSA with ⟨t, ht⟩

Result:
case intro.intro
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ ⊤.FG
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_add_one {s : ℝ} (hs : s ≠ 0) : Gamma (s + 1) = s * Gamma s

Proof state:
case h2
s : ℝ
hs : s ≠ 0
⊢ ↑s ≠ 0

Tactic:
rwa [Complex.ofReal_ne_zero]

Result:
no goals

Proof state:
s : ℝ
hs : s ≠ 0
⊢ (Complex.Gamma ↑(s + 1)).re = s * (Complex.Gamma ↑s).re

Tactic:
rw [Complex.ofReal_add, Complex.ofReal_one, Complex.Gamma_add_one, Complex.re_ofReal_mul]

Result:
case h2
s : ℝ
hs : s ≠ 0
⊢ ↑s ≠ 0

Proof state:
s : ℝ
hs : s ≠ 0
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
simp_rw [Gamma]

Result:
s : ℝ
hs : s ≠ 0
⊢ (Complex.Gamma ↑(s + 1)).re = s * (Complex.Gamma ↑s).re
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem MetricSpace.replaceBornology_eq {α} [m : MetricSpace α] [B : Bornology α]
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
    MetricSpace.replaceBornology _ H = m

Proof state:
α : Type u_3
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ m.replaceBornology H = m

Tactic:
ext

Result:
case h.dist.h.h
α : Type u_3
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Proof state:
case h.dist.h.h
α : Type u_3
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_sub_eq_of_lt_left {x y : R} (hx : v x < v y) :
    v (x - y) = v x

Proof state:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : v x < v y
⊢ v x < v (-y)

Tactic:
rwa [map_neg]

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : v x < v y
⊢ v (x - y) = v x

Tactic:
rw [sub_eq_add_neg]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : v x < v y
⊢ v (x + -y) = v x

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : v x < v y
⊢ v (x + -y) = v x

Tactic:
apply map_add_eq_of_lt_left

Result:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : v x < v y
⊢ v x < v (-y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i))

Proof state:
n x i : Nat
h : x < 2 ^ n
⊢ (x#'h).getMsbD i = (decide (i < n) && x.testBit (n - 1 - i))

Tactic:
simp [getMsbD, getLsbD]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem IsVonNBounded.neg (hs : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕜 (-s) := fun U hU ↦ by
  rw [← neg_neg U]
  exact (hs <| neg_mem_nhds_zero _ hU).neg_neg

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U (-s)

Tactic:
rw [← neg_neg U]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 (- -U) (-s)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 (- -U) (-s)

Tactic:
exact (hs <| neg_mem_nhds_zero _ hU).neg_neg

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem IsPreconnected.infinite_of_nontrivial [T1Space X] {s : Set X} (h : IsPreconnected s)
    (hs : s.Nontrivial) : s.Infinite

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
this : DiscreteTopology ↑s
⊢ Subsingleton ↑s

Tactic:
exact @PreconnectedSpace.trivial_of_discrete _ _ (Subtype.preconnectedSpace h) _

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
⊢ Subsingleton ↑s

Tactic:
haveI := @Finite.instDiscreteTopology s _ _ hf.to_subtype

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
this : DiscreteTopology ↑s
⊢ Subsingleton ↑s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
⊢ s.Infinite

Tactic:
refine mt (fun hf => (subsingleton_coe s).mp ?_) (not_subsingleton_iff.mpr hs)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
h : IsPreconnected s
hs : s.Nontrivial
hf : s.Finite
⊢ Subsingleton ↑s
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
theorem mk {s t : Set α} (hs : μ s = 0) (ht : ν t = 0) (hst : univ ⊆ s ∪ t) :
    MutuallySingular μ ν

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ s = 0
ht : ν t = 0
hst : univ ⊆ s ∪ t
⊢ μ ⟂ₘ ν

Tactic:
use toMeasurable μ s, measurableSet_toMeasurable _ _, (measure_toMeasurable _).trans hs

Result:
case right
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ s = 0
ht : ν t = 0
hst : univ ⊆ s ∪ t
⊢ ν (toMeasurable μ s)ᶜ = 0

Proof state:
case right
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ s = 0
ht : ν t = 0
hst : univ ⊆ s ∪ t
⊢ ν (toMeasurable μ s)ᶜ = 0

Tactic:
refine measure_mono_null (fun x hx => (hst trivial).resolve_left fun hxs => hx ?_) ht

Result:
case right
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ s = 0
ht : ν t = 0
hst : univ ⊆ s ∪ t
x : α
hx : x ∈ (toMeasurable μ s)ᶜ
hxs : x ∈ s
⊢ x ∈ toMeasurable μ s

Proof state:
case right
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : μ s = 0
ht : ν t = 0
hst : univ ⊆ s ∪ t
x : α
hx : x ∈ (toMeasurable μ s)ᶜ
hxs : x ∈ s
⊢ x ∈ toMeasurable μ s

Tactic:
exact subset_toMeasurable _ _ hxs

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_union_mem_openSegment {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t)
    (ht : NullMeasurableSet t μ) (hs₀ : μ s ≠ 0) (ht₀ : μ t ≠ 0) (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞)
    (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
    ⨍ x in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ x in s, f x ∂μ) (⨍ x in t, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : μ s ≠ 0
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Tactic:
replace hs₀ : 0 < (μ s).toReal := ENNReal.toReal_pos hs₀ hsμ

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < (μ s).toReal
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < (μ s).toReal
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Tactic:
replace ht₀ : 0 < (μ t).toReal := ENNReal.toReal_pos ht₀ htμ

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < (μ s).toReal
ht₀ : 0 < (μ t).toReal
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < (μ s).toReal
ht₀ : 0 < (μ t).toReal
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Tactic:
exact mem_openSegment_iff_div.mpr
  ⟨(μ s).toReal, (μ t).toReal, hs₀, ht₀, (average_union hd ht hsμ htμ hfs hft).symm⟩

Result:
no goals
-- Mathlib/Algebra/Ring/Units.lean
theorem divp_add_divp [CommRing α] (a b : α) (u₁ u₂ : αˣ) :
    a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂)

Proof state:
α : Type u
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)

Tactic:
simp only [divp, add_mul, mul_inv_rev, val_mul]

Result:
α : Type u
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)

Proof state:
α : Type u
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)

Tactic:
rw [mul_comm (↑u₁ * b), mul_comm b]

Result:
α : Type u
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)

Proof state:
α : Type u
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)

Tactic:
rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
  mul_one]

Result:
no goals