harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TMToPartrec.lean
theorem head_stack_ok {q s L₁ L₂ L₃} :
    Reaches₁ (TM2.step tr)
      ⟨some (head stack q), s, K'.elim (trList L₁) [] [] (trList L₂ ++ Γ'.consₗ :: L₃)⟩
      ⟨some q, none, K'.elim (trList (L₂.headI :: L₁)) [] [] L₃⟩

Proof state:
case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux
      (tr
        ((fun x =>
            Λ'.read fun s =>
              (if s = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.cons)))
      (some Γ'.cons)
      (update
        (update
          (update (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack (trList L₂ ++ Γ'.consₗ :: L₃)) rev
          ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun s => ((fun x => some Γ'.cons) s).iget) (some Γ'.cons) ::
          update
            (update (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack (trList L₂ ++ Γ'.consₗ :: L₃))
            rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)) rev)))
    { l := some q, var := none, stk := elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃ }

Tactic:
simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_false, trList, List.append_assoc,
  List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_self,
  List.headI_cons]

Result:
case cons
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux
      (tr
        (Λ'.read fun s =>
          (if s = some Γ'.consₗ then id else Λ'.clear (fun x => decide (x = Γ'.consₗ)) stack) (unrev q)))
      (some Γ'.cons)
      (elim (trList L₁) ((some Γ'.cons).iget :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    { l := some q, var := none, stk := elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
  x.signExtend v = x.setWidth v

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : v ≤ w
⊢ signExtend v x = setWidth v x

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
v : Nat
hv : v ≤ w
i : Nat
h : i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
v : Nat
hv : v ≤ w
i : Nat
h : i < v
⊢ (signExtend v x).getLsbD i = (setWidth v x).getLsbD i

Tactic:
simp only [getLsbD_signExtend, h, decide_true, Bool.true_and, getLsbD_setWidth,
  ite_eq_left_iff, Nat.not_lt]

Result:
case pred
w : Nat
x : BitVec w
v : Nat
hv : v ≤ w
i : Nat
h : i < v
⊢ w ≤ i → x.msb = x.getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
v : Nat
hv : v ≤ w
i : Nat
h : i < v
⊢ w ≤ i → x.msb = x.getLsbD i

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem degree_quadratic_le : degree (C a * X ^ 2 + C b * X + C c) ≤ 2

Proof state:
R : Type u
a b c : R
inst✝ : Semiring R
⊢ (C a * X ^ 2 + C b * X + C c).degree ≤ 2

Tactic:
simpa only [add_assoc] using
  degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
    (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/List.lean
/-- If zero is an element of a list `l`, then `List.prod l = 0`. If the domain is a nontrivial
monoid with zero with no divisors, then this implication becomes an `iff`, see
`List.prod_eq_zero_iff`. -/
lemma prod_eq_zero : ∀ {l : List M₀}, (0 : M₀) ∈ l → l.prod = 0
  -- |  absurd h (not_mem_nil _)
  | a :: l, h => by
    rw [prod_cons]
    rcases mem_cons.1 h with ha | hl
    exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (prod_eq_zero hl)]

Proof state:
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ a * l.prod = 0

Tactic:
rcases mem_cons.1 h with ha | hl

Result:
case inl
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
ha : 0 = a
⊢ a * l.prod = 0

case inr
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
hl : 0 ∈ l
⊢ a * l.prod = 0

Proof state:
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ (a :: l).prod = 0

Tactic:
rw [prod_cons]

Result:
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ a * l.prod = 0

Proof state:
case inl
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
ha : 0 = a
⊢ a * l.prod = 0

case inr
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
hl : 0 ∈ l
⊢ a * l.prod = 0

Tactic:
exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (prod_eq_zero hl)]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_norm_right : (f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g'

Tactic:
simp only [IsLittleO_def]

Result:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f fun x => ‖g' x‖) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f fun x => ‖g' x‖) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_norm_right

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
    a ∈ m.insert k v → (k == a) = false → a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ a ∈ m.insert k v → (k == a) = false → a ∈ m

Tactic:
simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem perm_replicate_append_replicate
    [DecidableEq α] {l : List α} {a b : α} {m n : ℕ} (h : a ≠ b) :
    l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x✝ : α
⊢ x✝ ∈ l → x✝ = b ∨ x✝ = a ↔ x✝ ≠ b → x✝ ≠ a → ¬x✝ ∈ l

Tactic:
rw [← and_imp, ← not_or, not_imp_not]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
suffices l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by
  simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a

Tactic:
simp [subset_def, or_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
this : l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
trans ∀ c, c ∈ l → c = b ∨ c = a

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a

α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
lemma sum_nat_mod (l : List ℕ) (n : ℕ) : l.sum % n = (l.map (· % n)).sum % n

Proof state:
case cons
n a : ℕ
l : List ℕ
ih : l.sum % n = (map (fun x => x % n) l).sum % n
⊢ (a :: l).sum % n = (map (fun x => x % n) (a :: l)).sum % n

Tactic:
simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

Result:
no goals

Proof state:
l : List ℕ
n : ℕ
⊢ l.sum % n = (map (fun x => x % n) l).sum % n

Tactic:
induction l with
| nil => simp only [Nat.zero_mod, map_nil]
| cons a l ih =>
  simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

Result:
no goals

Proof state:
case nil
n : ℕ
⊢ [].sum % n = (map (fun x => x % n) []).sum % n

Tactic:
simp only [Nat.zero_mod, map_nil]

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem diophFn_iff_pFun (f : (α → ℕ) → ℕ) : DiophFn f = @DiophPFun α f

Proof state:
α : Type u
f : (α → ℕ) → ℕ
⊢ DiophFn f = DiophPFun ↑f

Tactic:
refine congr_arg Dioph (Set.ext fun v => ?_)

Result:
α : Type u
f : (α → ℕ) → ℕ
v : Option α → ℕ
⊢ v ∈ {v | f (v ∘ some) = v none} ↔ v ∈ {v | (↑f).graph (v ∘ some, v none)}

Proof state:
α : Type u
f : (α → ℕ) → ℕ
v : Option α → ℕ
⊢ v ∈ {v | f (v ∘ some) = v none} ↔ v ∈ {v | (↑f).graph (v ∘ some, v none)}

Tactic:
exact PFun.lift_graph.symm

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_comp_mul_left_iff (f : ℝ → E) (c : ℝ) {a : ℝ} (ha : 0 < a) :
    IntegrableOn (fun x => f (a * x)) (Ioi c) ↔ IntegrableOn f (Ioi <| a * c)

Proof state:
case h.e'_1.h.e'_6.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ (Ioi c).indicator (fun x => f (a * x)) x = (Ioi c).indicator (f ∘ HMul.hMul a) x

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_1.h.e'_6
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ ((Ioi c).indicator fun x => f (a * x)) = fun x => (Ioi (a * c)).indicator f (a * x)

Tactic:
ext1 x

Result:
case h.e'_1.h.e'_6.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ (Ioi c).indicator (fun x => f (a * x)) x = (Ioi (a * c)).indicator f (a * x)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable ((Ioi c).indicator fun x => f (a * x)) volume ↔ IntegrableOn f (Ioi (a * c)) volume

Tactic:
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi <| a * c)]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable ((Ioi c).indicator fun x => f (a * x)) volume ↔ Integrable ((Ioi (a * c)).indicator f) volume

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => f (a * x)) (Ioi c) volume ↔ IntegrableOn f (Ioi (a * c)) volume

Tactic:
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi c)]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable ((Ioi c).indicator fun x => f (a * x)) volume ↔ IntegrableOn f (Ioi (a * c)) volume

Proof state:
case h.e'_1.h.e'_6.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ (Ioi c).indicator (fun x => f (a * x)) x = (Ioi (a * c)).indicator f (a * x)

Tactic:
rw [← indicator_comp_right, preimage_const_mul_Ioi _ ha, mul_comm a c,
  mul_div_cancel_right₀ _ ha.ne']

Result:
case h.e'_1.h.e'_6.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ (Ioi c).indicator (fun x => f (a * x)) x = (Ioi c).indicator (f ∘ HMul.hMul a) x

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable ((Ioi c).indicator fun x => f (a * x)) volume ↔ Integrable ((Ioi (a * c)).indicator f) volume

Tactic:
convert integrable_comp_mul_left_iff ((Ioi (a * c)).indicator f) ha.ne' using 2

Result:
case h.e'_1.h.e'_6
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ ((Ioi c).indicator fun x => f (a * x)) = fun x => (Ioi (a * c)).indicator f (a * x)
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Ioo : (fun x => x - a) '' Ioo b c = Ioo (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) '' Ioo b c = Ioo (b - a) (c - a)

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_cons_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    getValueCast? k (⟨k, v⟩ :: l) = some v

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ getValueCast? k (⟨k, v⟩ :: l) = some v

Tactic:
rw [getValueCast?_cons_of_true BEq.refl, cast_eq]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem mul_moveLeft_inr {x y : PGame} {i j} :
    (x * y).moveLeft (toLeftMovesMul (Sum.inr (i, j))) =
      x.moveRight i * y + x * y.moveRight j - x.moveRight i * y.moveRight j

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesMul (Sum.inr (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveRight j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * (mk α✝ β✝ a✝¹ a✝).moveRight j

Tactic:
rfl

Result:
no goals

Proof state:
x y : PGame
i : x.RightMoves
j : y.RightMoves
⊢ (x * y).moveLeft (toLeftMovesMul (Sum.inr (i, j))) =
    x.moveRight i * y + x * y.moveRight j - x.moveRight i * y.moveRight j

Tactic:
cases x

Result:
case mk
y : PGame
j : y.RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveLeft (toLeftMovesMul (Sum.inr (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveRight i * y + mk α✝ β✝ a✝¹ a✝ * y.moveRight j - (mk α✝ β✝ a✝¹ a✝).moveRight i * y.moveRight j

Proof state:
case mk
y : PGame
j : y.RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveLeft (toLeftMovesMul (Sum.inr (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveRight i * y + mk α✝ β✝ a✝¹ a✝ * y.moveRight j - (mk α✝ β✝ a✝¹ a✝).moveRight i * y.moveRight j

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesMul (Sum.inr (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveRight j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * (mk α✝ β✝ a✝¹ a✝).moveRight j
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem toFinsupp_algebraMap (r : R) : (algebraMap R A[X] r).toFinsupp = algebraMap R _ r :=
  show toFinsupp (C (algebraMap _ _ r)) = _ by
    rw [toFinsupp_C]
    rfl

Proof state:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ AddMonoidAlgebra.single 0 ((algebraMap R A) r) = (algebraMap R (AddMonoidAlgebra A ℕ)) r

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (C ((algebraMap R A) r)).toFinsupp = (algebraMap R (AddMonoidAlgebra A ℕ)) r

Tactic:
rw [toFinsupp_C]

Result:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ AddMonoidAlgebra.single 0 ((algebraMap R A) r) = (algebraMap R (AddMonoidAlgebra A ℕ)) r
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem exists_memBaseSet_isPartition (l : IntegrationParams) (I : Box ι) (hc : I.distortion ≤ c)
    (r : (ι → ℝ) → Ioi (0 : ℝ)) : ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Proof state:
ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : ⊤.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Tactic:
have hc' : (⊤ : Prepartition I).compl.distortion ≤ c := by simp

Result:
ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : ⊤.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
hc' : ⊤.compl.distortion ≤ c
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Proof state:
ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : I.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Tactic:
rw [← Prepartition.distortion_top] at hc

Result:
ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : ⊤.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Proof state:
ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : ⊤.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ ⊤.compl.distortion ≤ c

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
c : ℝ≥0
l : IntegrationParams
I : Box ι
hc : ⊤.distortion ≤ c
r : (ι → ℝ) → ↑(Set.Ioi 0)
hc' : ⊤.compl.distortion ≤ c
⊢ ∃ π, l.MemBaseSet I c r π ∧ π.IsPartition

Tactic:
simpa [isPartition_iff_iUnion_eq] using l.exists_memBaseSet_le_iUnion_eq ⊤ hc hc' r

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma exists_not_self_orthogonal (v : ℙ F (m → F)) : ∃ w, ¬ orthogonal v w

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv✝ : v ≠ 0
hv : ∃ x, ¬v ⬝ᵥ x = 0
⊢ ∃ w, ¬(mk F v hv✝).orthogonal w

Tactic:
obtain ⟨w, hw⟩ := hv

Result:
case h.intro
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
⊢ ∃ w, ¬(mk F v hv).orthogonal w

Proof state:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : ℙ F (m → F)
⊢ ∃ w, ¬v.orthogonal w

Tactic:
induction v with | h v hv =>
rw [ne_eq, ← dotProduct_eq_zero_iff, not_forall] at hv
obtain ⟨w, hw⟩ := hv
exact ⟨mk F w fun h ↦ hw (by rw [h, dotProduct_zero]), hw⟩

Result:
no goals

Proof state:
case h.intro
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
⊢ ∃ w, ¬(mk F v hv).orthogonal w

Tactic:
exact ⟨mk F w fun h ↦ hw (by rw [h, dotProduct_zero]), hw⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
h : w = 0
⊢ v ⬝ᵥ w = 0

Tactic:
rw [h, dotProduct_zero]

Result:
no goals

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
⊢ ∃ w, ¬(mk F v hv).orthogonal w

Tactic:
rw [ne_eq, ← dotProduct_eq_zero_iff, not_forall] at hv

Result:
case h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv✝ : v ≠ 0
hv : ∃ x, ¬v ⬝ᵥ x = 0
⊢ ∃ w, ¬(mk F v hv✝).orthogonal w
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.def [BEq α] {l : List ((a : α) × β a)} :
    DistinctKeys l ↔ l.Pairwise (fun a b => (a.1 == b.1) = false) :=
  ⟨fun h => by simpa [keys_eq_map, List.pairwise_map] using h.distinct,
   fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
h : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ List.Pairwise (fun a b => (a == b) = false) (keys l)

Tactic:
simpa [keys_eq_map, List.pairwise_map] using h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
h : DistinctKeys l
⊢ List.Pairwise (fun a b => (a.fst == b.fst) = false) l

Tactic:
simpa [keys_eq_map, List.pairwise_map] using h.distinct

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem disc_ne_zero_iff_roots_nodup (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    P.disc ≠ 0 ↔ (map φ P).roots.Nodup

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ {x, y, z}.Nodup

Tactic:
change _ ↔ (x ::ₘ y ::ₘ {z}).Nodup

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ (x ::ₘ y ::ₘ {z}).Nodup

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ (x ::ₘ y ::ₘ {z}).Nodup

Tactic:
rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ {z}.Nodup

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ {z}.Nodup

Tactic:
simp only [nodup_singleton]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ P.disc ≠ 0 ↔ (map φ P).roots.Nodup

Tactic:
rw [disc_ne_zero_iff_roots_ne ha h3, h3]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ {x, y, z}.Nodup

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True

Tactic:
tauto

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma norm_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) :
    ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / n ^ s.re

Proof state:
case inr
f : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

Tactic:
simp [hn, norm_natCast_cpow_of_pos <| Nat.pos_of_ne_zero hn]

Result:
no goals

Proof state:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
f : ℕ → ℂ
s : ℂ
⊢ ‖term f s 0‖ = if 0 = 0 then 0 else ‖f 0‖ / ↑0 ^ s.re

case inr
f : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

Proof state:
case inl
f : ℕ → ℂ
s : ℂ
⊢ ‖term f s 0‖ = if 0 = 0 then 0 else ‖f 0‖ / ↑0 ^ s.re

Tactic:
simp

Result:
no goals