harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem orthonormal (b : OrthonormalBasis ι 𝕜 E) : Orthonormal 𝕜 b

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ inner (b i) (b j) = if i = j then 1 else 0

Tactic:
rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
  EuclideanSpace.inner_single_left, EuclideanSpace.single_apply, map_one, one_mul]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ Orthonormal 𝕜 ⇑b

Tactic:
rw [orthonormal_iff_ite]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ ∀ (i j : ι), inner (b i) (b j) = if i = j then 1 else 0

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ Orthonormal 𝕜 ⇑b

Tactic:
classical
  rw [orthonormal_iff_ite]
  intro i j
  rw [← b.repr.inner_map_map (b i) (b j), b.repr_self i, b.repr_self j,
    EuclideanSpace.inner_single_left, EuclideanSpace.single_apply, map_one, one_mul]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ ∀ (i j : ι), inner (b i) (b j) = if i = j then 1 else 0

Tactic:
intro i j

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
i j : ι
⊢ inner (b i) (b j) = if i = j then 1 else 0
-- Mathlib/Algebra/Order/Monovary.lean
@[simp] lemma antivary_inv_right₀ (hg : StrongLT 0 g) : Antivary f g⁻¹ ↔ Monovary f g :=
  forall_swap.trans <| forall₂_congr fun i j ↦ by simp [inv_lt_inv₀ (hg _) (hg _)]

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
f : ι → α
g : ι → β
hg : StrongLT 0 g
i j : ι
⊢ g⁻¹ j < g⁻¹ i → f i ≤ f j ↔ g i < g j → f i ≤ f j

Tactic:
simp [inv_lt_inv₀ (hg _) (hg _)]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_neg_one (n : ℕ) : (-1 : ZMod n.succ).val = n

Proof state:
n : ℕ
⊢ (-1).val = n

Tactic:
dsimp [val, Fin.coe_neg]

Result:
n : ℕ
⊢ ↑(-1) = n

Proof state:
case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
rw [Fin.coe_neg_one]

Result:
no goals

Proof state:
n : ℕ
⊢ ↑(-1) = n

Tactic:
cases n

Result:
case zero

⊢ ↑(-1) = 0

case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Proof state:
case zero

⊢ ↑(-1) = 0

Tactic:
simp [Nat.mod_one]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem finSuccEquiv_eq :
    (finSuccEquiv R n : MvPolynomial (Fin (n + 1)) R →+* Polynomial (MvPolynomial (Fin n) R)) =
      eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R)) fun i : Fin (n + 1) =>
        Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i

Proof state:
case hX.a
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X i)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i) (X i)).coeff n✝

Tactic:
refine Fin.cases ?_ ?_ i <;> simp [finSuccEquiv]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(finSuccEquiv R n) = eval₂Hom (Polynomial.C.comp C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i

Tactic:
ext i : 2

Result:
case hC.a
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ((↑(finSuccEquiv R n)).comp C) i =
    ((eval₂Hom (Polynomial.C.comp C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i).comp C) i

case hX.a
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X i)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i) (X i)).coeff n✝

Proof state:
case hC.a
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ (algebraMap R (MvPolynomial (Fin n) R)[X]) i = Polynomial.C (C i)

Tactic:
rfl

Result:
no goals

Proof state:
case hC.a
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ((↑(finSuccEquiv R n)).comp C) i =
    ((eval₂Hom (Polynomial.C.comp C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i).comp C) i

Tactic:
simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe,
  coe_eval₂Hom, comp_apply, renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]

Result:
case hC.a
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ (algebraMap R (MvPolynomial (Fin n) R)[X]) i = Polynomial.C (C i)
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem changeOrigin_toFormalMultilinearSeries [DecidableEq ι] :
    continuousMultilinearCurryFin1 𝕜 (∀ i, E i) F (f.toFormalMultilinearSeries.changeOrigin x 1) =
    f.linearDeriv x

Proof state:
case h.inr.refine_3
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ f (Function.update x i (y i)) = f fun i_1 => if i_1 = i then y i_1 else x i_1

Tactic:
congr

Result:
case h.inr.refine_3.h.e_6.h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
i : ι
⊢ Function.update x i (y i) = fun i_1 => if i_1 = i then y i_1 else x i_1

Proof state:
case h.inr.refine_3.h.e_6.h.h.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
j : ι
⊢ Function.update x j (y j) j = if j = j then y j else x j

Tactic:
rw [Function.update_self, if_pos rfl]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mulVec_injective_iff_isUnit {A : Matrix m m K} :
    Function.Injective A.mulVec ↔ IsUnit A

Proof state:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ Function.Injective A.mulVec ↔ IsUnit A

Tactic:
rw [← isUnit_transpose, ← vecMul_injective_iff_isUnit]

Result:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ Function.Injective A.mulVec ↔ Function.Injective fun v => v ᵥ* Aᵀ

Proof state:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ Function.Injective A.mulVec ↔ Function.Injective fun v => v ᵥ* Aᵀ

Tactic:
simp_rw [vecMul_transpose]

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
lemma isInt_ediv {a b q m a' : ℤ} {b' r : ℕ}
    (ha : IsInt a a') (hb : IsNat b b')
    (hm : q * b' = m) (h : r + m = a') (h₂ : Nat.blt r b' = true) :
    IsInt (a / b) q := ⟨by
  obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
  simp only [Nat.blt_eq] at h₂; simp only [← h, ← hm, Int.cast_id]
  rw [Int.add_mul_ediv_right _ _ (Int.ofNat_ne_zero.2 ((Nat.zero_le ..).trans_lt h₂).ne')]
  rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]⟩

Proof state:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r / ↑b' + q = q

Tactic:
rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]

Result:
no goals

Proof state:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ (↑r + q * ↑b') / ↑b' = q

Tactic:
rw [Int.add_mul_ediv_right _ _ (Int.ofNat_ne_zero.2 ((Nat.zero_le ..).trans_lt h₂).ne')]

Result:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r / ↑b' + q = q

Proof state:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a / ↑b' = ↑q

Tactic:
simp only [Nat.blt_eq] at h₂

Result:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ a / ↑b' = ↑q

Proof state:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ a / ↑b' = ↑q

Tactic:
simp only [← h, ← hm, Int.cast_id]

Result:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ (↑r + q * ↑b') / ↑b' = q

Proof state:
a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a / b = ↑q

Tactic:
obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb

Result:
case mk.mk
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a / ↑b' = ↑q
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Build/Key.lean
theorem eq_of_quickCmp {k k' : BuildKey}  :
quickCmp k k' = Ordering.eq → k = k'

Proof state:
case targetFacet.customTarget
p t f package✝ target✝ : Name
⊢ (match targetFacet p t f with
      | moduleFacet m f =>
        match customTarget package✝ target✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match customTarget package✝ target✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match customTarget package✝ target✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match customTarget package✝ target✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    targetFacet p t f = customTarget package✝ target✝

Tactic:
intro

Result:
case targetFacet.customTarget
p t f package✝ target✝ : Name
a✝ :
  (match targetFacet p t f with
    | moduleFacet m f =>
      match customTarget package✝ target✝ with
      | moduleFacet m' f' =>
        match m.quickCmp m' with
        | Ordering.eq => f.quickCmp f'
        | ord => ord
      | x => Ordering.lt
    | packageFacet p f =>
      match customTarget package✝ target✝ with
      | moduleFacet module facet => Ordering.gt
      | packageFacet p' f' =>
        match p.quickCmp p' with
        | Ordering.eq => f.quickCmp f'
        | ord => ord
      | x => Ordering.lt
    | targetFacet p t f =>
      match customTarget package✝ target✝ with
      | customTarget package target => Ordering.lt
      | targetFacet p' t' f' =>
        match p.quickCmp p' with
        | Ordering.eq =>
          match t.quickCmp t' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | ord => ord
      | x => Ordering.gt
    | customTarget p t =>
      match customTarget package✝ target✝ with
      | customTarget p' t' =>
        match p.quickCmp p' with
        | Ordering.eq => t.quickCmp t'
        | ord => ord
      | x => Ordering.gt) =
    Ordering.eq
⊢ targetFacet p t f = customTarget package✝ target✝
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Build/Key.lean
theorem eq_of_quickCmp {k k' : BuildKey}  :
quickCmp k k' = Ordering.eq → k = k'

Proof state:
case customTarget.targetFacet
p t package✝ target✝ facet✝ : Name
a✝ :
  (match customTarget p t with
    | moduleFacet m f =>
      match targetFacet package✝ target✝ facet✝ with
      | moduleFacet m' f' =>
        match m.quickCmp m' with
        | Ordering.eq => f.quickCmp f'
        | ord => ord
      | x => Ordering.lt
    | packageFacet p f =>
      match targetFacet package✝ target✝ facet✝ with
      | moduleFacet module facet => Ordering.gt
      | packageFacet p' f' =>
        match p.quickCmp p' with
        | Ordering.eq => f.quickCmp f'
        | ord => ord
      | x => Ordering.lt
    | targetFacet p t f =>
      match targetFacet package✝ target✝ facet✝ with
      | customTarget package target => Ordering.lt
      | targetFacet p' t' f' =>
        match p.quickCmp p' with
        | Ordering.eq =>
          match t.quickCmp t' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | ord => ord
      | x => Ordering.gt
    | customTarget p t =>
      match targetFacet package✝ target✝ facet✝ with
      | customTarget p' t' =>
        match p.quickCmp p' with
        | Ordering.eq => t.quickCmp t'
        | ord => ord
      | x => Ordering.gt) =
    Ordering.eq
⊢ customTarget p t = targetFacet package✝ target✝ facet✝

Tactic:
contradiction

Result:
no goals

Proof state:
case packageFacet.customTarget
p f package✝ target✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match customTarget package✝ target✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match customTarget package✝ target✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match customTarget package✝ target✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match customTarget package✝ target✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = customTarget package✝ target✝

Tactic:
(intro; contradiction)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Build/Key.lean
theorem eq_of_quickCmp {k k' : BuildKey}  :
quickCmp k k' = Ordering.eq → k = k'

Proof state:
p t f p' t' f' : Name
⊢ (match targetFacet p t f with
      | moduleFacet m f =>
        match targetFacet p' t' f' with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match targetFacet p' t' f' with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match targetFacet p' t' f' with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match targetFacet p' t' f' with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    targetFacet p t f = targetFacet p' t' f'

Tactic:
dsimp only

Result:
p t f p' t' f' : Name
⊢ (match p.quickCmp p' with
      | Ordering.eq =>
        match t.quickCmp t' with
        | Ordering.eq => f.quickCmp f'
        | ord => ord
      | ord => ord) =
      Ordering.eq →
    targetFacet p t f = targetFacet p' t' f'

Proof state:
p t p' t' : Name
⊢ (match p.quickCmp p' with
      | Ordering.eq => t.quickCmp t'
      | ord => ord) =
      Ordering.eq →
    customTarget p t = customTarget p' t'

Tactic:
split

Result:
case h_1
p t p' t' : Name
x✝ : Ordering
heq✝ : p.quickCmp p' = Ordering.eq
⊢ t.quickCmp t' = Ordering.eq → customTarget p t = customTarget p' t'

case h_2
p t p' t' : Name
x✝¹ : Ordering
x✝ : p.quickCmp p' = Ordering.eq → False
⊢ p.quickCmp p' = Ordering.eq → customTarget p t = customTarget p' t'

Proof state:
m f m' f' : Name
x✝ : Ordering
m_eq : m.quickCmp m' = Ordering.eq
f_eq : f.quickCmp f' = Ordering.eq
⊢ moduleFacet m f = moduleFacet m' f'

Tactic:
rw [eq_of_cmp m_eq, eq_of_cmp f_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_sub_posLog_inv {r : ℝ} : log⁺ r - log⁺ r⁻¹ = log r

Proof state:
r : ℝ
⊢ log⁺ r - log⁺ r⁻¹ = log r

Tactic:
rw [posLog_def, posLog_def, log_inv]

Result:
r : ℝ
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

Proof state:
r : ℝ
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

Tactic:
by_cases h : 0 ≤ log r

Result:
case pos
r : ℝ
h : 0 ≤ log r
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

case neg
r : ℝ
h : ¬0 ≤ log r
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

Proof state:
case neg
r : ℝ
h : log r < 0
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

Tactic:
simp [neg_nonneg.1 (Left.nonneg_neg_iff.2 h.le)]

Result:
no goals

Proof state:
case neg
r : ℝ
h : ¬0 ≤ log r
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

Tactic:
rw [not_le] at h

Result:
case neg
r : ℝ
h : log r < 0
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

Proof state:
case pos
r : ℝ
h : 0 ≤ log r
⊢ 0 ⊔ log r - 0 ⊔ -log r = log r

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_succ [AddGroupWithOne α] (n) : ((succ n : ZNum) : α) = n + 1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.succ = ↑n + 1

Tactic:
rw [← add_one, cast_add, cast_one]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The function `n ↦ Λ n / n`, restricted to non-primes in a residue class, is summable.
This is used to convert results on `ArithmeticFunction.vonMangoldt.residueClass` to results
on primes in an arithmetic progression. -/
lemma summable_residueClass_non_primes_div :
    Summable fun n : ℕ ↦ (if n.Prime then 0 else residueClass a n) / n

Proof state:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
⊢ Summable fun n => (if Nat.Prime n then 0 else residueClass a n) / ↑n

Tactic:
have hleF₀ (n : ℕ) : (if n.Prime then 0 else residueClass a n) / n ≤ F₀ n := by
  refine div_le_div_of_nonneg_right ?_ n.cast_nonneg
  split_ifs; exacts [le_rfl, residueClass_le a n]

Result:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ ArithmeticFunction.vonMangoldt.F₀ n
⊢ Summable fun n => (if Nat.Prime n then 0 else residueClass a n) / ↑n
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@[simp] lemma map_fst_prod : (μ.prod ν).map Prod.fst = ν univ • μ

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (μ.prod ν).map Prod.fst = ν univ • μ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ↑((μ.prod ν).map Prod.fst) s✝ = ↑(ν univ • μ) s✝

Proof state:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ↑((μ.prod ν).map Prod.fst) s✝ = ↑(ν univ • μ) s✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toLeft_disjSum : (s.disjSum t).toLeft = s

Proof state:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α
⊢ x ∈ (s.disjSum t).toLeft ↔ x ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toLeft = s

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α
⊢ x ∈ (s.disjSum t).toLeft ↔ x ∈ s
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem mul_prod_erase' (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ i : α, g i 0 = 1) :
    g y (f y) * (erase y f).prod g = f.prod g

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
by_cases hyf : y ∈ f.support

Result:
case pos
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Proof state:
case pos
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∈ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
exact Finsupp.mul_prod_erase f y g hyf

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
rw [not_mem_support_iff.mp hyf, hg y, erase_of_not_mem_support hyf, one_mul]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem isPrime_map_C_iff_isPrime (P : Ideal R) :
    IsPrime (map (C : R →+* R[X]) P : Ideal R[X]) ↔ IsPrime P

Proof state:
case mpr.mem_or_mem'.intro
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
⊢ ∃ n, (f * g).coeff n ∉ P

Tactic:
let n := Nat.find hg

Result:
case mpr.mem_or_mem'.intro
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∃ n, (f * g).coeff n ∉ P

Proof state:
case mpr.mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ f * g ∈ map C P → f ∈ map C P ∨ g ∈ map C P

Tactic:
simp only [mem_map_C_iff]

Result:
case mpr.mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ (∀ (n : ℕ), (f * g).coeff n ∈ P) → (∀ (n : ℕ), f.coeff n ∈ P) ∨ ∀ (n : ℕ), g.coeff n ∈ P
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem maximal_iff_forall_insert (hP : ∀ ⦃s t⦄, P t → s ⊆ t → P s) :
    Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬ P (insert x s)

Proof state:
α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ P s → ((∀ ⦃y : Finset α⦄, P y → s ≤ y → y ≤ s) ↔ ∀ x ∉ s, ¬P (insert x s))

Tactic:
exact fun _ ↦ ⟨fun h x hxs hx ↦ hxs <| h hx (subset_insert _ _) (mem_insert_self x s),
  fun h t ht hst x hxt ↦ by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

Tactic:
simp only [Maximal, and_congr_right_iff]

Result:
α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ P s → ((∀ ⦃y : Finset α⦄, P y → s ≤ y → y ≤ s) ↔ ∀ x ∉ s, ¬P (insert x s))
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem mem_leftCoset_leftCoset {a : α} (ha : a • (s : Set α) = s) : a ∈ s

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ s

Tactic:
rw [← SetLike.mem_coe, ← ha]

Result:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s

Tactic:
exact mem_own_leftCoset s a

Result:
no goals