harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem dvd_antisymm {a b : Ordinal} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b :=
  if a0 : a = 0 then by subst a; exact (eq_zero_of_zero_dvd h₁).symm
  else
    if b0 : b = 0 then by subst b; exact eq_zero_of_zero_dvd h₂
    else (le_of_dvd b0 h₁).antisymm (le_of_dvd a0 h₂)

Proof state:
b : Ordinal.{u_4}
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b

Tactic:
exact (eq_zero_of_zero_dvd h₁).symm

Result:
no goals

Proof state:
a : Ordinal.{u_4}
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0

Tactic:
exact eq_zero_of_zero_dvd h₂

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : a = 0
⊢ a = b

Tactic:
subst a

Result:
b : Ordinal.{u_4}
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b

Proof state:
a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : ¬a = 0
b0 : b = 0
⊢ a = b

Tactic:
subst b

Result:
a : Ordinal.{u_4}
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem hasBasis_cobounded_compl_ball (c : α) :
    (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (ball c r)ᶜ) :=
  ⟨compl_surjective.forall.2 fun _ ↦ (isBounded_iff_subset_ball c).trans <| by simp⟩

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝ : Set α
⊢ (∃ r, x✝ ⊆ ball c r) ↔ ∃ i, True ∧ (ball c i)ᶜ ⊆ x✝ᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l) :
    getKey! (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (insertManyIfNewUnit empty l).val.getKey! k' = k

Tactic:
exact getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
  contains_empty distinct mem

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem _root_.List.toList_toAssocList (l : List (α × β)) : l.toAssocList.toList = l

Proof state:
α : Type u_1
β : Type u_2
l : List (α × β)
⊢ l.toAssocList.toList = l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem gronwallBound_x0 (δ K ε : ℝ) : gronwallBound δ K ε 0 = δ

Proof state:
δ K ε : ℝ
⊢ gronwallBound δ K ε 0 = δ

Tactic:
by_cases hK : K = 0

Result:
case pos
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ

case neg
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ

Proof state:
case pos
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ

Tactic:
simp only [gronwallBound, if_pos hK, mul_zero, add_zero]

Result:
no goals

Proof state:
case neg
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ

Tactic:
simp only [gronwallBound, if_neg hK, mul_zero, exp_zero, sub_self, mul_one,
  add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldl_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : β → { x // p x } → β} {g : β → α → β} {x : β}
    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
    l.foldl f x = l.unattach.foldl g x

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
toList✝ : List { x // p x }
⊢ List.foldl f x toList✝ = List.foldl g x toList✝.unattach

Tactic:
rw [List.foldl_subtype]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
toList✝ : List { x // p x }
⊢ ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
toList✝ : List { x // p x }
⊢ ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x

Tactic:
simp [hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldl f x l = foldl g x l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
toList✝ : List { x // p x }
⊢ foldl f x { toList := toList✝ } = foldl g x { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
toList✝ : List { x // p x }
⊢ foldl f x { toList := toList✝ } = foldl g x { toList := toList✝ }.unattach

Tactic:
simp only [List.foldl_toArray', List.unattach_toArray]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : β → { x // p x } → β
g : β → α → β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
toList✝ : List { x // p x }
⊢ List.foldl f x toList✝ = List.foldl g x toList✝.unattach
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis.exchange (hIX : M.IsBasis I X) (hJX : M.IsBasis J X) (he : e ∈ I \ J) :
    ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Tactic:
obtain ⟨y,hy, h⟩ := hIX.restrict_isBase.exchange hJX.restrict_isBase he

Result:
case intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Tactic:
exact ⟨y, hy, by rwa [isBase_restrict_iff] at h⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ M.IsBasis (insert y (I \ {e})) X

Tactic:
rwa [isBase_restrict_iff] at h

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem sign_neg : ∀ x : EReal, sign (-x) = -sign x
  | ⊤ => rfl
  | ⊥ => rfl
  | (x : ℝ) => by rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]

Proof state:
x : ℝ
⊢ sign (-↑x) = -sign ↑x

Tactic:
rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
@[reassoc]
lemma XOpIso_hom_d_op (i j : Option ι) :
    (XOpIso K i).hom ≫ (d K j i).op =
      d K.op i j ≫ (XOpIso K j).hom :=
  match i, j with
  | none, _ => by
      simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]
  | some i, some j => by
      dsimp [XOpIso]
      simp only [d_eq _ rfl rfl, Option.some.injEq, d_eq, op_comp, assoc,
        id_comp, comp_id]
      rfl
  | some _, none => by
      simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i j x✝ : Option ι
⊢ (XOpIso K none).hom ≫ (d K x✝ none).op = d K.op none x✝ ≫ (XOpIso K x✝).hom

Tactic:
simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ (XOpIso K (some i)).hom ≫ (d K (some j) (some i)).op = d K.op (some i) (some j) ≫ (XOpIso K (some j)).hom

Tactic:
dsimp [XOpIso]

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ 𝟙 (X K.op (some i)) ≫ (d K (some j) (some i)).op = d K.op (some i) (some j) ≫ 𝟙 (X K.op (some j))

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ (XIso K ⋯).inv.op ≫ (K.d j i).op ≫ (XIso K ⋯).hom.op = (XIso K.op ⋯).hom ≫ K.op.d i j ≫ (XIso K.op ⋯).inv

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i j : Option ι
val✝ : ι
⊢ (XOpIso K (some val✝)).hom ≫ (d K none (some val✝)).op = d K.op (some val✝) none ≫ (XOpIso K none).hom

Tactic:
simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ 𝟙 (X K.op (some i)) ≫ (d K (some j) (some i)).op = d K.op (some i) (some j) ≫ 𝟙 (X K.op (some j))

Tactic:
simp only [d_eq _ rfl rfl, Option.some.injEq, d_eq, op_comp, assoc,
  id_comp, comp_id]

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ (XIso K ⋯).inv.op ≫ (K.d j i).op ≫ (XIso K ⋯).hom.op = (XIso K.op ⋯).hom ≫ K.op.d i j ≫ (XIso K.op ⋯).inv
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.elim_directed_family_closed {ι : Type v} [Nonempty ι] (hs : IsCompact s)
    (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅)
    (hdt : Directed (· ⊇ ·) t) : ∃ i : ι, s ∩ t i = ∅ :=
  let ⟨t, ht⟩ :=
    hs.elim_directed_cover (compl ∘ t) (fun i => (htc i).isOpen_compl)
      (by
        simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
          mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using hst)
      (hdt.mono_comp _ fun _ _ => compl_subset_compl.mpr)
  ⟨t, by
    simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
      mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using ht⟩

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
hdt : Directed (fun x1 x2 => x1 ⊇ x2) t
⊢ s ⊆ ⋃ i, (compl ∘ t) i

Tactic:
simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
  mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using hst

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsCompact s
t✝ : ι → Set X
htc : ∀ (i : ι), IsClosed (t✝ i)
hst : s ∩ ⋂ i, t✝ i = ∅
hdt : Directed (fun x1 x2 => x1 ⊇ x2) t✝
t : ι
ht : s ⊆ (compl ∘ t✝) t
⊢ s ∩ t✝ t = ∅

Tactic:
simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_iUnion, exists_prop,
  mem_inter_iff, not_and, mem_iInter, mem_compl_iff] using ht

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem row_add [Add α] (v w : m → α) : row ι (v + w) = row ι v + row ι w

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
⊢ row ι (v + w) = row ι v + row ι w

Tactic:
ext

Result:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : ι
j✝ : m
⊢ row ι (v + w) i✝ j✝ = (row ι v + row ι w) i✝ j✝

Proof state:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : ι
j✝ : m
⊢ row ι (v + w) i✝ j✝ = (row ι v + row ι w) i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negDblY_of_Z_eq_zero {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.negDblY P = -(P x ^ 2) ^ 3

Proof state:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negDblY P - -(P x ^ 2) ^ 3 - ((8 * P y ^ 2 - 12 * P x ^ 3) * P y ^ 2 - (8 * P x ^ 3 - 12 * P x ^ 3) * P x ^ 3) = 0

Tactic:
rw [negDblY, dblU_of_Z_eq_zero hPz, dblX_of_Z_eq_zero hP hPz, negY_of_Z_eq_zero hPz]

Result:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * P x ^ 2) * ((P x ^ 2) ^ 2 - P x * (P y - -P y) ^ 2) + P y * (P y - -P y) ^ 3 - -(P x ^ 2) ^ 3 -
      ((8 * P y ^ 2 - 12 * P x ^ 3) * P y ^ 2 - (8 * P x ^ 3 - 12 * P x ^ 3) * P x ^ 3) =
    0

Proof state:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * P x ^ 2) * ((P x ^ 2) ^ 2 - P x * (P y - -P y) ^ 2) + P y * (P y - -P y) ^ 3 - -(P x ^ 2) ^ 3 -
      ((8 * P y ^ 2 - 12 * P x ^ 3) * P y ^ 2 - (8 * P x ^ 3 - 12 * P x ^ 3) * P x ^ 3) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negDblY P = -(P x ^ 2) ^ 3

Tactic:
linear_combination' (norm :=
    (rw [negDblY, dblU_of_Z_eq_zero hPz, dblX_of_Z_eq_zero hP hPz, negY_of_Z_eq_zero hPz]; ring1))
  (8 * (equation_of_Z_eq_zero hPz).mp hP - 12 * P x ^ 3) * (equation_of_Z_eq_zero hPz).mp hP

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {b : β a} :
    (m.insert a b).getKeyD a fallback = a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a fallback : α
b : β a
⊢ (m.insert a b).getKeyD a fallback = a

Tactic:
simp_to_raw using Raw₀.getKeyD_insert_self

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
lemma pderiv_rename {τ : Type*} {f : σ → τ} (hf : Function.Injective f)
    (x : σ) (p : MvPolynomial σ R) :
    pderiv (f x) (rename f p) = rename f (pderiv x p)

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
⊢ (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)

Tactic:
induction' p using MvPolynomial.induction_on with a p q hp hq p a h

Result:
case h_C
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
a : R
⊢ (pderiv (f x)) ((rename f) (C a)) = (rename f) ((pderiv x) (C a))

case h_add
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p q : MvPolynomial σ R
hp : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
hq : (pderiv (f x)) ((rename f) q) = (rename f) ((pderiv x) q)
⊢ (pderiv (f x)) ((rename f) (p + q)) = (rename f) ((pderiv x) (p + q))

case h_X
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
⊢ (pderiv (f x)) ((rename f) (p * X a)) = (rename f) ((pderiv x) (p * X a))

Proof state:
case h_X
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
⊢ (pderiv (f x)) ((rename f) (p * X a)) = (rename f) ((pderiv x) (p * X a))

Tactic:
simp only [map_mul, MvPolynomial.rename_X, Derivation.leibniz, MvPolynomial.pderiv_X,
  Pi.single_apply, hf.eq_iff, smul_eq_mul, mul_ite, mul_one, mul_zero, h, map_add, add_left_inj]

Result:
case h_X
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
⊢ (if a = x then (rename f) p else 0) + X (f a) * (rename f) ((pderiv x) p) =
    (rename f) (if a = x then p else 0) + X (f a) * (rename f) ((pderiv x) p)

Proof state:
case h_X
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p : MvPolynomial σ R
a : σ
h : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
⊢ (if a = x then (rename f) p else 0) + X (f a) * (rename f) ((pderiv x) p) =
    (rename f) (if a = x then p else 0) + X (f a) * (rename f) ((pderiv x) p)

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
case h_add
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
p q : MvPolynomial σ R
hp : (pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
hq : (pderiv (f x)) ((rename f) q) = (rename f) ((pderiv x) q)
⊢ (pderiv (f x)) ((rename f) (p + q)) = (rename f) ((pderiv x) (p + q))

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
case h_C
R : Type u
σ : Type v
inst✝ : CommSemiring R
τ : Type u_1
f : σ → τ
hf : Injective f
x : σ
a : R
⊢ (pderiv (f x)) ((rename f) (C a)) = (rename f) ((pderiv x) (C a))

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli_eq_bernoulli'_of_ne_one {n : ℕ} (hn : n ≠ 1) : bernoulli n = bernoulli' n

Proof state:
case neg
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n

Tactic:
rcases mod_two_eq_zero_or_one n with h | h

Result:
case neg.inl
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n

case neg.inr
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 1
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n

Proof state:
case neg
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ bernoulli n = bernoulli' n

Tactic:
rw [bernoulli, neg_one_pow_eq_pow_mod_two]

Result:
case neg
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n

Proof state:
case neg.inl
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
n : ℕ
hn : n ≠ 1
h0 : n = 0
⊢ bernoulli n = bernoulli' n

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg.inr
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 1
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n

Tactic:
simp [bernoulli'_odd_eq_zero (odd_iff.mpr h) (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, hn⟩)]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 1
⊢ bernoulli n = bernoulli' n

Tactic:
by_cases h0 : n = 0

Result:
case pos
n : ℕ
hn : n ≠ 1
h0 : n = 0
⊢ bernoulli n = bernoulli' n

case neg
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ bernoulli n = bernoulli' n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y

Proof state:
w : Nat
x y : BitVec w
⊢ x.smtUDiv y = if y = 0#w then allOnes w else x / y

Tactic:
simp [smtUDiv]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := gcongr)]
lemma mulEnergy_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : Eₘ[s₁, t₁] ≤ Eₘ[s₂, t₂]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s₁ ×ˢ s₁) ×ˢ t₁ ×ˢ t₁)) ≤
    #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s₂ ×ˢ s₂) ×ˢ t₂ ×ˢ t₂))

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ Eₘ[s₁, t₁] ≤ Eₘ[s₂, t₂]

Tactic:
unfold mulEnergy

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s₁ ×ˢ s₁) ×ˢ t₁ ×ˢ t₁)) ≤
    #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) ((s₂ ×ˢ s₂) ×ˢ t₂ ×ˢ t₂))
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_rightAngleRotation_swap (x y : E) : ⟪x, J y⟫ = -⟪J x, y⟫

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x (o.rightAngleRotation y) = -inner (o.rightAngleRotation x) y

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp] lemma isMaximumIndepSet_compl [Fintype α] (s : Finset α) :
    Gᶜ.IsMaximumIndepSet s ↔ G.IsMaximumClique s

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
⊢ Gᶜ.IsMaximumIndepSet s ↔ G.IsMaximumClique s

Tactic:
simp [isMaximumIndepSet_iff, isMaximumClique_iff]

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
    Tendsto f atTop (𝓝 (⨆ i, f i))

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : IsEmpty ι
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : Nonempty ι
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Proof state:
case inl
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : IsEmpty ι
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : Nonempty ι
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
exacts [tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_ciSup hbdd)]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem coe_int_ofDigits (b : ℕ) (L : List ℕ) : ((ofDigits b L : ℕ) : ℤ) = ofDigits (b : ℤ) L

Proof state:
case nil
b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ofDigits (↑b) L = ↑d + ↑b * ofDigits (↑b) L

Tactic:
simp only

Result:
no goals

Proof state:
case cons
b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(ofDigits b (d :: L)) = ofDigits (↑b) (d :: L)

Tactic:
dsimp [ofDigits]

Result:
case cons
b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Proof state:
b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L

Tactic:
induction' L with d L _

Result:
case nil
b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []

case cons
b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(ofDigits b (d :: L)) = ofDigits (↑b) (d :: L)

Proof state:
case cons
b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Tactic:
push_cast

Result:
case cons
b d : ℕ
L : List ℕ
tail_ih✝ : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ofDigits (↑b) L = ↑d + ↑b * ofDigits (↑b) L