harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2

Proof state:
x : Nat
xz : x = 0
⊢ x &&& 1 = x % 2

Tactic:
simp [xz, zero_and]

Result:
no goals

Proof state:
x : Nat
xz : ¬x = 0
andz : x / 2 &&& 0 = 0
⊢ x &&& 1 = x % 2

Tactic:
simp only [HAnd.hAnd, AndOp.and, land] at andz

Result:
x : Nat
xz : ¬x = 0
andz : bitwise and (x / 2) 0 = 0
⊢ x &&& 1 = x % 2

Proof state:
x : Nat
⊢ x &&& 1 = x % 2

Tactic:
if xz : x = 0 then
  simp [xz, zero_and]
else
  have andz := and_zero (x/2)
  simp only [HAnd.hAnd, AndOp.and, land] at andz
  simp only [HAnd.hAnd, AndOp.and, land]
  unfold bitwise
  cases mod_two_eq_zero_or_one x with | _ p =>
    simp [xz, p, andz, one_div_two, mod_eq_of_lt]

Result:
no goals

Proof state:
x : Nat
xz : ¬x = 0
⊢ x &&& 1 = x % 2

Tactic:
have andz := and_zero (x/2)

Result:
x : Nat
xz : ¬x = 0
andz : x / 2 &&& 0 = 0
⊢ x &&& 1 = x % 2

Proof state:
x : Nat
xz : ¬x = 0
andz : bitwise and (x / 2) 0 = 0
⊢ bitwise and x 1 = x % 2

Tactic:
unfold bitwise

Result:
x : Nat
xz : ¬x = 0
andz : bitwise and (x / 2) 0 = 0
⊢ (if x = 0 then if (false && true) = true then 1 else 0
    else
      if 1 = 0 then if (true && false) = true then x else 0
      else
        let n' := x / 2;
        let m' := 1 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 1 % 2 = 1;
        let r := bitwise and n' m';
        if (decide b₁ && decide b₂) = true then r + r + 1 else r + r) =
    x % 2

Proof state:
x : Nat
xz : ¬x = 0
andz : bitwise and (x / 2) 0 = 0
⊢ x &&& 1 = x % 2

Tactic:
simp only [HAnd.hAnd, AndOp.and, land]

Result:
x : Nat
xz : ¬x = 0
andz : bitwise and (x / 2) 0 = 0
⊢ bitwise and x 1 = x % 2

Proof state:
x : Nat
xz : ¬x = 0
andz : bitwise and (x / 2) 0 = 0
⊢ (if x = 0 then if (false && true) = true then 1 else 0
    else
      if 1 = 0 then if (true && false) = true then x else 0
      else
        let n' := x / 2;
        let m' := 1 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 1 % 2 = 1;
        let r := bitwise and n' m';
        if (decide b₁ && decide b₂) = true then r + r + 1 else r + r) =
    x % 2

Tactic:
cases mod_two_eq_zero_or_one x with | _ p =>
  simp [xz, p, andz, one_div_two, mod_eq_of_lt]

Result:
no goals

Proof state:
case inr
x : Nat
xz : ¬x = 0
andz : bitwise and (x / 2) 0 = 0
p : x % 2 = 1
⊢ (if x = 0 then if (false && true) = true then 1 else 0
    else
      if 1 = 0 then if (true && false) = true then x else 0
      else
        let n' := x / 2;
        let m' := 1 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 1 % 2 = 1;
        let r := bitwise and n' m';
        if (decide b₁ && decide b₂) = true then r + r + 1 else r + r) =
    x % 2

Tactic:
simp [xz, p, andz, one_div_two, mod_eq_of_lt]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_succ_row {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ) :
    det A =
      ∑ j : Fin n.succ, (-1) ^ (i + j : ℕ) * A i j * det (A.submatrix i.succAbove j.succAbove)

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
have : det A = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by
  calc
    det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
    _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ A.det = (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem dist_div_sin_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [eq_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, norm_div_sin_angle_add_of_inner_eq_zero h h0]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem liftIco_continuous [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p))
    (hc : ContinuousOn f <| Icc a (a + p)) : Continuous (liftIco p a f)

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous (liftIco p a f)

Tactic:
rw [liftIco_eq_lift_Icc hf]

Result:
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous (Quot.lift ((Icc a (a + p)).restrict f) ⋯ ∘ ⇑(equivIccQuot p a))

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous (Quot.lift ((Icc a (a + p)).restrict f) ⋯ ∘ ⇑(equivIccQuot p a))

Tactic:
refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun

Result:
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous (Quot.lift ((Icc a (a + p)).restrict f) ⋯)

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous (Quot.lift ((Icc a (a + p)).restrict f) ⋯)

Tactic:
exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_restrict.mp hc)

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean
/-- `IsLocalization.mk'` agrees with `IsLocalizedModule.mk'`. -/
lemma IsLocalization.mk'_algebraMap_eq_mk' [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ]
    {x : A} {s : S} : IsLocalization.mk' Aₛ x ⟨_, Algebra.mem_algebraMapSubmonoid_of_mem s⟩ =
      IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x s

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ (algebraMap R A) ↑s • mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x

Tactic:
exact IsLocalization.smul_mk'_self (m := ⟨_, _⟩)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = IsLocalizedModule.mk' (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x s

Tactic:
rw [← IsLocalizedModule.smul_inj (IsScalarTower.toAlgHom R A Aₛ).toLinearMap s,
  IsLocalizedModule.mk'_cancel', Submonoid.smul_def, ← algebraMap_smul A]

Result:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : CommSemiring Aₛ
inst✝³ : Algebra A Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R A Aₛ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
x : A
s : ↥S
⊢ (algebraMap R A) ↑s • mk' Aₛ x ⟨(algebraMap R A) ↑s, ⋯⟩ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).size ≤ m.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).size ≤ m.size + 1

Tactic:
simp_to_raw using Raw₀.size_insert_le ⟨m, _⟩ h

Result:
no goals
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem det_vandermonde {n : ℕ} (v : Fin n → R) :
    det (vandermonde v) = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih : ∀ (v : Fin n → R), (of fun i j => v i ^ ↑j).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)
v : Fin (n + 1) → R
⊢ (of fun i j => vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i).det =
    (of fun i j => vecCons (v 0 ^ ↑j.succ) (fun i => v i.succ ^ ↑j.succ - v 0 ^ ↑j.succ) (Fin.succAbove 0 i)).det

Tactic:
simp_rw [det_succ_column_zero, Fin.sum_univ_succ, of_apply, Matrix.cons_val_zero, submatrix,
  of_apply, Matrix.cons_val_succ, Fin.val_zero, pow_zero, one_mul, sub_self,
  mul_zero, zero_mul, Finset.sum_const_zero, add_zero]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
    (h1 : TendstoUniformlyOnFilter F f p p') (h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i)))
    (h3 : Tendsto L p (𝓝 ℓ)) : Tendsto f p' (𝓝 ℓ)

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
i : ι
p4 : (L i, ℓ) ∈ t
p5 : ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p6 : ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Basic.lean
@[to_additive] lemma eq_one_iff (h : SemiconjBy a x y): x = 1 ↔ y = 1

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ x = 1 ↔ y = 1

Tactic:
rw [← conj_eq_one_iff (a := a) (b := x), h.eq, mul_inv_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean
lemma ShortExact.op (h : S.ShortExact) : S.op.ShortExact where
  exact := h.exact.op
  mono_f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Epi S.g
⊢ Mono S.g.op

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Mono S.f
⊢ Epi S.op.g

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Mono S.f
⊢ Epi S.f.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
⊢ Epi S.op.g

Tactic:
have := h.mono_f

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Mono S.f
⊢ Epi S.op.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Epi S.g
⊢ Mono S.op.f

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Epi S.g
⊢ Mono S.g.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
⊢ Mono S.op.f

Tactic:
have := h.epi_g

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Epi S.g
⊢ Mono S.op.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
this : Mono S.f
⊢ Epi S.f.op

Tactic:
infer_instance

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem integerNormalization_eval₂_eq_zero (g : S →+* R') (p : S[X]) {x : R'}
    (hx : eval₂ g x p = 0) : eval₂ (g.comp (algebraMap R S)) x (integerNormalization M p) = 0 :=
  let ⟨b, hb⟩ := integerNormalization_map_to_map M p
  _root_.trans (eval₂_map (algebraMap R S) g x).symm
    (by rw [hb, ← IsScalarTower.algebraMap_smul S (b : R) p, eval₂_smul, hx, mul_zero])

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
R' : Type u_3
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : ↥M
hb : Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0

Tactic:
rw [hb, ← IsScalarTower.algebraMap_smul S (b : R) p, eval₂_smul, hx, mul_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
@[simp]
lemma detp_neg_one_one : detp (-1) (1 : Matrix n n R) = 0

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ = 1
⊢ σ ∉ ofSign (-1)

Tactic:
rw [hσ, mem_ofSign, sign_one]

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ = 1
⊢ ¬1 = -1

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ = 1
⊢ ¬1 = -1

Tactic:
decide

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ σ ≠ 1

Tactic:
contrapose! hσ

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ = 1
⊢ σ ∉ ofSign (-1)

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ detp (-1) 1 = 0

Tactic:
rw [detp, sum_eq_zero]

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ ∀ x ∈ ofSign (-1), ∏ k : n, 1 k (x k) = 0

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
⊢ ∏ k : n, 1 k (σ k) = 0

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)

Result:
case intro
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k : n, 1 k (σ k) = 0

Proof state:
case intro
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
i : n
hi : ¬σ i = 1 i
⊢ ∏ k : n, 1 k (σ k) = 0

Tactic:
exact prod_eq_zero (mem_univ i) (one_apply_ne' hi)

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ ∏ k : n, 1 k (σ k) = 0

Tactic:
have hσ1 : σ ≠ 1 := by
  contrapose! hσ
  rw [hσ, mem_ofSign, sign_one]
  decide

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ ∈ ofSign (-1)
hσ1 : σ ≠ 1
⊢ ∏ k : n, 1 k (σ k) = 0

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ ∀ x ∈ ofSign (-1), ∏ k : n, 1 k (x k) = 0

Tactic:
intro σ hσ

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ ∏ k : n, 1 k (σ k) = 0
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_not_mem_null_le_laverage (hμ : μ ≠ 0) (hf : AEMeasurable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ f x ≤ ⨍⁻ a, f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N)
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N)
x : α
hx : x ∈ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N)
x : α
hx : x ∈ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
exact ⟨x, hxN, hx⟩

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
have := measure_le_laverage_pos hμ hf

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
this : 0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
this : 0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
rw [← measure_diff_null hN] at this

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N)
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
-- Mathlib/Data/Nat/Dist.lean
theorem dist_eq_sub_of_le_right {n m : ℕ} (h : m ≤ n) : dist n m = n - m

Proof state:
n m : ℕ
h : m ≤ n
⊢ m.dist n = n - m

Tactic:
apply dist_eq_sub_of_le h

Result:
no goals

Proof state:
n m : ℕ
h : m ≤ n
⊢ n.dist m = n - m

Tactic:
rw [dist_comm]

Result:
n m : ℕ
h : m ≤ n
⊢ m.dist n = n - m
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
private lemma LFunction_ne_zero_of_not_quadratic_or_ne_one {t : ℝ} (h : χ ^ 2 ≠ 1 ∨ t ≠ 0) :
    LFunction χ (1 + I * t) ≠ 0

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖x‖
⊢ False

Tactic:
exact isLittleO_irrefl (.of_forall (fun _ ↦ one_ne_zero)) <|
  (H.of_norm_right (F' := ℝ)).trans_isLittleO <| isLittleO_id_one.mono nhdsWithin_le_nhds

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
⊢ LFunction χ (1 + I * ↑t) ≠ 0

Tactic:
intro Hz

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
⊢ False

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖↑x‖
⊢ False

Tactic:
simp only [norm_real] at H

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x => 1) =O[𝓝[>] 0] fun x =>
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖x‖
⊢ False