harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
@[simp] lemma comp_neg_X_leadingCoeff_eq [Ring R] (p : R[X]) :
    (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : p = 0
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Proof state:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Tactic:
rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree] <;>
simp [((Commute.neg_one_left _).pow_left _).eq, h]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : p = 0
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Closed.lean
theorem pullback_close {X Y : C} (f : Y ⟶ X) (S : Sieve X) :
    J₁.close (S.pullback f) = (J₁.close S).pullback f

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ (J₁.close (Sieve.pullback f S)).arrows g

Tactic:
change _ ∈ J₁ _

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ J₁ Z

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ J₁ Z

Tactic:
rw [← Sieve.pullback_comp]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ Sieve.pullback (g ≫ f) S ∈ J₁ Z

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ J₁.close (Sieve.pullback f S) = Sieve.pullback f (J₁.close S)

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)

case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (J₁.close S) ≤ J₁.close (Sieve.pullback f S)

Tactic:
intro Z g hg

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ (J₁.close (Sieve.pullback f S)).arrows g

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ J₁.IsClosed (Sieve.pullback f (J₁.close S))

Tactic:
apply J₁.isClosed_pullback _ _ (J₁.close_isClosed _)

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ J₁.close (Sieve.pullback f S) ≤ Sieve.pullback f (J₁.close S)

Tactic:
refine J₁.le_close_of_isClosed (Sieve.pullback_monotone _ (J₁.le_close S)) ?_

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ J₁.IsClosed (Sieve.pullback f (J₁.close S))

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ Sieve.pullback (g ≫ f) S ∈ J₁ Z

Tactic:
apply hg

Result:
no goals
-- Mathlib/Data/List/Zip.lean
theorem zipWith_congr (f g : α → β → γ) (la : List α) (lb : List β)
    (h : List.Forall₂ (fun a b => f a b = g a b) la lb) : zipWith f la lb = zipWith g la lb

Proof state:
case nil
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
h : Forall₂ (fun a b => f a b = g a b) la lb
⊢ zipWith f la lb = zipWith g la lb

Tactic:
induction' h with a b as bs hfg _ ih

Result:
case nil
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []

case cons
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
a : α
b : β
as : List α
bs : List β
hfg : f a b = g a b
a✝ : Forall₂ (fun a b => f a b = g a b) as bs
ih : zipWith f as bs = zipWith g as bs
⊢ zipWith f (a :: as) (b :: bs) = zipWith g (a :: as) (b :: bs)

Proof state:
case cons
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
a : α
b : β
as : List α
bs : List β
hfg : f a b = g a b
a✝ : Forall₂ (fun a b => f a b = g a b) as bs
ih : zipWith f as bs = zipWith g as bs
⊢ zipWith f (a :: as) (b :: bs) = zipWith g (a :: as) (b :: bs)

Tactic:
exact congr_arg₂ _ hfg ih

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem isLUB_Ico {a b : γ} (hab : a < b) : IsLUB (Ico a b) b

Proof state:
γ : Type v
inst✝¹ : SemilatticeInf γ
inst✝ : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ico a b) b

Tactic:
simpa only [dual_Ioc] using isGLB_Ioc hab.dual

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem lnot_bit (b) : ∀ n, lnot (bit b n) = bit (not b) (lnot n)
  | (n : ℕ) => by simp [lnot]
  | -[n+1] => by simp [lnot]

Proof state:
b : Bool
n : ℕ
⊢ (bit b ↑n).lnot = bit (!b) (↑n).lnot

Tactic:
simp [lnot]

Result:
no goals

Proof state:
b : Bool
n : ℕ
⊢ (bit b -[n+1]).lnot = bit (!b) -[n+1].lnot

Tactic:
simp [lnot]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem hom_eq_desc (g : widePushout _ _ arrows ⟶ X) :
    g =
      desc (head arrows ≫ g) (fun j => ι arrows j ≫ g) fun j => by
        rw [← Category.assoc]
        simp

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g : widePushout B objs arrows ⟶ X
⊢ g = desc (head arrows ≫ g) (fun j => ι arrows j ≫ g) ⋯

Tactic:
apply eq_desc_of_comp_eq

Result:
case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g : widePushout B objs arrows ⟶ X
⊢ ∀ (j : J), ι arrows j ≫ g = ι arrows j ≫ g

case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g : widePushout B objs arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g

Proof state:
case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g : widePushout B objs arrows ⟶ X
⊢ head arrows ≫ g = head arrows ≫ g

Tactic:
rfl

Result:
no goals

Proof state:
case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g : widePushout B objs arrows ⟶ X
⊢ ∀ (j : J), ι arrows j ≫ g = ι arrows j ≫ g

Tactic:
simp

Result:
no goals

Proof state:
J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ arrows j ≫ (fun j => ι arrows j ≫ g) j = head arrows ≫ g

Tactic:
rw [← Category.assoc]

Result:
J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g

Proof state:
J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Pi.lean
lemma _root_.Multiset.pi_coe (l : List ι) (fs : ∀ i, List (α i)) :
    (l : Multiset ι).pi (fs ·) = (↑(pi l fs) : Multiset (∀ i ∈ l, α i))

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
⊢ ((↑l).pi fun x => ↑(fs x)) = ↑(l.pi fs)

Tactic:
induction' l with i l ih

Result:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ ((↑[]).pi fun x => ↑(fs x)) = ↑([].pi fs)

case cons
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
l : List ι
ih : ((↑l).pi fun x => ↑(fs x)) = ↑(l.pi fs)
⊢ ((↑(i :: l)).pi fun x => ↑(fs x)) = ↑((i :: l).pi fs)

Proof state:
case cons
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
l : List ι
ih : ((↑l).pi fun x => ↑(fs x)) = ↑(l.pi fs)
⊢ ((↑(i :: l)).pi fun x => ↑(fs x)) = ↑((i :: l).pi fs)

Tactic:
change Multiset.pi (i ::ₘ ↑l) _ = _

Result:
case cons
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
l : List ι
ih : ((↑l).pi fun x => ↑(fs x)) = ↑(l.pi fs)
⊢ ((i ::ₘ ↑l).pi fun x => ↑(fs x)) = ↑((i :: l).pi fs)

Proof state:
case cons
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
l : List ι
ih : ((↑l).pi fun x => ↑(fs x)) = ↑(l.pi fs)
⊢ ((i ::ₘ ↑l).pi fun x => ↑(fs x)) = ↑((i :: l).pi fs)

Tactic:
simp [ih, Multiset.coe_bind, - Multiset.cons_coe]

Result:
no goals

Proof state:
case nil.h.h
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
hi : i ∈ 0
⊢ Multiset.Pi.empty α i hi = Pi.nil α i hi

Tactic:
simp at hi

Result:
no goals

Proof state:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ Multiset.Pi.empty α = Pi.nil α

Tactic:
ext i hi

Result:
case nil.h.h
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
hi : i ∈ 0
⊢ Multiset.Pi.empty α i hi = Pi.nil α i hi

Proof state:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ ((↑[]).pi fun x => ↑(fs x)) = ↑([].pi fs)

Tactic:
change Multiset.pi 0 _ = _

Result:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ (Multiset.pi 0 fun x => ↑(fs x)) = ↑([].pi fs)

Proof state:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ (Multiset.pi 0 fun x => ↑(fs x)) = ↑([].pi fs)

Tactic:
simp only [Multiset.coe_singleton, Multiset.pi_zero, pi_nil, Multiset.singleton_inj]

Result:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
⊢ Multiset.Pi.empty α = Pi.nil α
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey_eq_self' {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)}
    (h : containsKey k l = false) (h' : (f (getValue? k l)).isNone) :
    (alterKey k f l).length = l.length

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
h : containsKey k l = false
h' : (f (getValue? k l)).isNone = true
⊢ (alterKey k f l).length = l.length

Tactic:
simp [length_alterKey', h, h']

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Asymptotics.IsLittleO.sum_range {α : Type*} [NormedAddCommGroup α] {f : ℕ → α} {g : ℕ → ℝ}
    (h : f =o[atTop] g) (hg : 0 ≤ g) (h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop) :
    (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
n : ℕ
hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i = ε * ‖∑ i ∈ range n, g i‖

Tactic:
simp only [B]

Result:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
n : ℕ
hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ε / 2 * ∑ i ∈ range n, g i + ε / 2 * ∑ i ∈ range n, g i = ε * ∑ i ∈ range n, g i
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isAffine_of_isIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] [h : IsAffine Y] : IsAffine X

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X

Tactic:
exact Functor.essImage.ofIso (asIso f).symm h

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : IsAffine Y
⊢ IsAffine X

Tactic:
rw [← mem_Spec_essImage] at h ⊢

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem SubgroupNormal.mem_comm {H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal]
    {a b : G} (hb : b ∈ K) (h : a * b ∈ H) : b * a ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
⊢ b * a ∈ H

Tactic:
rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
⊢ b * a ∈ H

Tactic:
have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
⊢ b * a ∈ H
-- Mathlib/Algebra/Order/Kleene.lean
lemma natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1

Proof state:
case base
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : n ≠ 0
x✝ : ℕ
⊢ ↑1 = 1

Tactic:
exact Nat.cast_one

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : n ≠ 0
x✝ x : ℕ
hmn✝ : 1 ≤ x
hx : ↑x = 1
⊢ ↑(x + 1) = 1

Tactic:
rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : n ≠ 0
⊢ ↑n = 1

Tactic:
induction n, Nat.one_le_iff_ne_zero.mpr nezero using Nat.le_induction with
| base => exact Nat.cast_one
| succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_mul' (h : p.trailingCoeff * q.trailingCoeff ≠ 0) :
    (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

Tactic:
rw [hp, trailingCoeff_zero, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

Tactic:
rw [hq, trailingCoeff_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
apply natTrailingDegree_eq_of_trailingDegree_eq_some

Result:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = ↑(p.natTrailingDegree + q.natTrailingDegree)

Proof state:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = ↑(p.natTrailingDegree + q.natTrailingDegree)

Tactic:
rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
  WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
  ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem univ_pi_Ioo_ae_eq_Icc {f g : ∀ i, α i} :
    (pi univ fun i => Ioo (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)

Tactic:
exact pi_Ioo_ae_eq_pi_Icc

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g

Tactic:
rw [← pi_univ_Icc]

Result:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem isUnit_iff_eq_bot {a : Associates M} : IsUnit a ↔ a = ⊥

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : Associates M
⊢ IsUnit a ↔ a = ⊥

Tactic:
rw [Associates.isUnit_iff_eq_one, bot_eq_one]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean
lemma aemeasurable_of_aemeasurable_exp_mul {t : ℝ}
    (ht : t ≠ 0) (hf : AEMeasurable (fun x ↦ exp (t * f x)) μ) :
    AEMeasurable f μ

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
t : ℝ
ht : t ≠ 0
hf : AEMeasurable (fun x => rexp (t * f x)) μ
⊢ AEMeasurable f μ

Tactic:
simpa only [mul_div_cancel_left₀ _ ht]
  using (aemeasurable_of_aemeasurable_exp hf).div (aemeasurable_const (b := t))

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem sigma_nonempty : (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
simp [Finset.Nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate w

Proof state:
assign : Assignment
w idx : Nat
h : (assign.get idx).w = w
⊢ h ▸ (assign.get idx).bv = BitVec.truncate w (assign.get idx).bv

Tactic:
subst h

Result:
assign : Assignment
idx : Nat
⊢ ⋯ ▸ (assign.get idx).bv = BitVec.truncate (assign.get idx).w (assign.get idx).bv

Proof state:
assign : Assignment
w idx : Nat
⊢ eval assign (var idx) = BitVec.truncate w (assign.get idx).bv

Tactic:
rw [eval]

Result:
assign : Assignment
w idx : Nat
⊢ (if h : (assign.get idx).w = w then h ▸ (assign.get idx).bv else BitVec.truncate w (assign.get idx).bv) =
    BitVec.truncate w (assign.get idx).bv

Proof state:
assign : Assignment
w idx : Nat
⊢ (if h : (assign.get idx).w = w then h ▸ (assign.get idx).bv else BitVec.truncate w (assign.get idx).bv) =
    BitVec.truncate w (assign.get idx).bv

Tactic:
split

Result:
case isTrue
assign : Assignment
w idx : Nat
h✝ : (assign.get idx).w = w
⊢ h✝ ▸ (assign.get idx).bv = BitVec.truncate w (assign.get idx).bv

case isFalse
assign : Assignment
w idx : Nat
h✝ : ¬(assign.get idx).w = w
⊢ BitVec.truncate w (assign.get idx).bv = BitVec.truncate w (assign.get idx).bv

Proof state:
case isFalse
assign : Assignment
w idx : Nat
h✝ : ¬(assign.get idx).w = w
⊢ BitVec.truncate w (assign.get idx).bv = BitVec.truncate w (assign.get idx).bv

Tactic:
rfl

Result:
no goals

Proof state:
assign : Assignment
idx : Nat
⊢ ⋯ ▸ (assign.get idx).bv = BitVec.truncate (assign.get idx).w (assign.get idx).bv

Tactic:
simp

Result:
no goals

Proof state:
case isTrue
assign : Assignment
w idx : Nat
h✝ : (assign.get idx).w = w
⊢ h✝ ▸ (assign.get idx).bv = BitVec.truncate w (assign.get idx).bv

Tactic:
next h =>
subst h
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
    (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat))

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
i : Nat
⊢ (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat))

Tactic:
simp [shiftLeft_eq', getLsbD_shiftLeft]

Result:
no goals
-- Mathlib/Order/Height.lean
theorem cons_mem_subchain_iff :
    (a::l) ∈ s.subchain ↔ a ∈ s ∧ l ∈ s.subchain ∧ ∀ b ∈ l.head?, a < b

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
l : List α
a : α
⊢ a :: l ∈ s.subchain ↔ a ∈ s ∧ l ∈ s.subchain ∧ ∀ b ∈ l.head?, a < b

Tactic:
simp only [subchain, mem_setOf_eq, forall_mem_cons, chain'_cons', and_left_comm, and_comm,
  and_assoc]

Result:
no goals