harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem primitive_element_inf_aux_of_finite_intermediateField
    [Finite (IntermediateField F E)] : ∃ γ : E, F⟮α, β⟯ = F⟮γ⟯

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : (x - y)⁻¹ • (x - y) • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
rw [smul_smul, inv_mul_eq_div, div_self (sub_ne_zero.2 hneq), one_smul] at β_in_K

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ α + x • β ∈ F⟮α, β⟯

Tactic:
have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
α_in_Fαβ : α ∈ F⟮α, β⟯
⊢ α + x • β ∈ F⟮α, β⟯

Proof state:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ α + x • β - (α + y • β) = (x - y) • β

Tactic:
rw [sub_smul]

Result:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ α + x • β - (α + y • β) = x • β - y • β
-- Mathlib/Algebra/Prime/Defs.lean
theorem dvd_of_dvd_pow {a : M} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a

Proof state:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
⊢ p ∣ a

Tactic:
have := isUnit_of_dvd_one h

Result:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this : IsUnit p
⊢ p ∣ a

Proof state:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this : IsUnit p
⊢ p ∣ a

Tactic:
have := not_unit hp

Result:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this✝ : IsUnit p
this : ¬IsUnit p
⊢ p ∣ a

Proof state:
case succ
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a ^ (n + 1)
⊢ p ∣ a

Tactic:
rw [pow_succ'] at h

Result:
case succ
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
⊢ p ∣ a

Proof state:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ a ^ 0
⊢ p ∣ a

Tactic:
rw [pow_zero] at h

Result:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
⊢ p ∣ a

Proof state:
case succ
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
⊢ p ∣ a

Tactic:
rcases dvd_or_dvd hp h with dvd_a | dvd_pow

Result:
case succ.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a

Proof state:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
this✝ : IsUnit p
this : ¬IsUnit p
⊢ p ∣ a

Tactic:
contradiction

Result:
no goals

Proof state:
case succ.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

Tactic:
assumption

Result:
no goals

Proof state:
case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a

Tactic:
exact ih dvd_pow

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_inv_hom_id' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
    (g ⊗ inv f) ≫ (h ⊗ f) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ inv f) ≫ (h ⊗ f) = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

Tactic:
rw [← tensor_comp, IsIso.inv_hom_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 W = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 W = (g ⊗ 𝟙 W) ≫ (h ⊗ 𝟙 W)

Tactic:
simp [tensorHom_id]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generatePiSystem_mono {S T : Set (Set α)} (hST : S ⊆ T) :
    generatePiSystem S ⊆ generatePiSystem T := fun t ht => by
  induction ht with
  | base h_s => exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
  | inter _ _ h_nonempty h_s h_u => exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty

Proof state:
case base
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s✝ : Set α
h_s : s✝ ∈ S
⊢ s✝ ∈ generatePiSystem T

Tactic:
exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)

Result:
no goals

Proof state:
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t : Set α
ht : t ∈ generatePiSystem S
⊢ t ∈ generatePiSystem T

Tactic:
induction ht with
| base h_s => exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
| inter _ _ h_nonempty h_s h_u => exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty

Result:
no goals

Proof state:
case inter
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty : (s✝ ∩ t✝).Nonempty
h_s : s✝ ∈ generatePiSystem T
h_u : t✝ ∈ generatePiSystem T
⊢ s✝ ∩ t✝ ∈ generatePiSystem T

Tactic:
exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_beq_push [BEq α] {a b : α} {v : Array α} {w : Array α} :
    (v.push a == w.push b) = (v == w && a == b)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
v w : Array α
⊢ (v.push a == w.push b) = (v == w && a == b)

Tactic:
cases v

Result:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
w : Array α
toList✝ : List α
⊢ ({ toList := toList✝ }.push a == w.push b) = ({ toList := toList✝ } == w && a == b)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
w : Array α
toList✝ : List α
⊢ ({ toList := toList✝ }.push a == w.push b) = ({ toList := toList✝ } == w && a == b)

Tactic:
cases w

Result:
case mk.mk
α : Type u_1
inst✝ : BEq α
a b : α
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ }.push a == { toList := toList✝ }.push b) =
    ({ toList := toList✝¹ } == { toList := toList✝ } && a == b)

Proof state:
case mk.mk
α : Type u_1
inst✝ : BEq α
a b : α
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ }.push a == { toList := toList✝ }.push b) =
    ({ toList := toList✝¹ } == { toList := toList✝ } && a == b)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblZ_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
    (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) : W'.dblZ P = 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblZ P = 0

Tactic:
rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, mul_zero]

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq [CompleteSpace E] {v : ℝ → E → E}
    {tMin t₀ tMax : ℝ} (x₀ : E) {C R : ℝ} {L : ℝ≥0}
    (hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
    ∃ f : ℝ → E, f t₀ = x₀ ∧
      ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin t₀ tMax : ℝ
x₀ : E
C R : ℝ
L : ℝ≥0
hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C
⊢ ∃ f, f t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t

Tactic:
lift C to ℝ≥0 using (norm_nonneg _).trans hpl.norm_le₀

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin t₀ tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R ↑C
⊢ ∃ f, f t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
t₀ : { x // x ∈ Icc tMin tMax }
hpl : IsPicardLindelof v tMin (↑t₀) tMax x₀ L R ↑C
⊢ ∃ f, f ↑t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t

Tactic:
exact PicardLindelof.exists_solution
  ⟨v, tMin, tMax, t₀, x₀, C, ⟨R, hpl.hR⟩, L, { hpl with ht₀ := t₀.property }⟩

Result:
no goals

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin t₀ tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R ↑C
⊢ ∃ f, f t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t

Tactic:
lift t₀ to Icc tMin tMax using hpl.ht₀

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
v : ℝ → E → E
tMin tMax : ℝ
x₀ : E
R : ℝ
L C : ℝ≥0
t₀ : { x // x ∈ Icc tMin tMax }
hpl : IsPicardLindelof v tMin (↑t₀) tMax x₀ L R ↑C
⊢ ∃ f, f ↑t₀ = x₀ ∧ ∀ t ∈ Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Icc tMin tMax) t
-- Mathlib/ModelTheory/Basic.lean
theorem refl_apply (x : M) : refl L M x = x

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ { toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } x = x

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ (refl L M) x = x

Tactic:
simp [refl]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ { toEquiv := _root_.Equiv.refl M, map_fun' := ⋯, map_rel' := ⋯ } x = x
-- Mathlib/Data/Nat/ModEq.lean
theorem dvd_iff (h : a ≡ b [MOD m]) (hdm : d ∣ m) : d ∣ a ↔ d ∣ b

Proof state:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]

Tactic:
replace h := h.of_dvd hdm

Result:
m a b d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]

Proof state:
m a b d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]

Tactic:
exact ⟨h.symm.trans, h.trans⟩

Result:
no goals

Proof state:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b

Tactic:
simp only [← modEq_zero_iff_dvd]

Result:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv (h : S.LeftHomologyData) :
    h.homologyIso.hom ≫ h.leftHomologyIso.inv = S.leftHomologyIso.inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.homologyIso.hom ≫ h.leftHomologyIso.inv = S.leftHomologyIso.inv

Tactic:
dsimp only [homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom ≫ h.leftHomologyIso.inv = S.leftHomologyIso.inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom ≫ h.leftHomologyIso.inv = S.leftHomologyIso.inv

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem join_join (SS : WSeq (WSeq (WSeq α))) : join (join SS) ~ʷ join (map join SS)

Proof state:
α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ SS.join.join = nil.append (nil.append SS.join).join

Tactic:
simp

Result:
no goals

Proof state:
case h1.h2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1 SS_1,
    (s.append (S.append SS.join).join).destruct = (s_1.append (S_1.append SS_1.join).join).destruct ∧
      (s.append (S.join.append (map join SS).join)).destruct =
        (s_1.append (S_1.join.append (map join SS_1).join)).destruct

Tactic:
exact ⟨s, S, SS, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ SS.join.join ~ʷ (map join SS).join

Tactic:
refine
  ⟨fun s1 s2 =>
    ∃ s S SS,
      s1 = append s (join (append S (join SS))) ∧
        s2 = append s (append (join S) (join (map join SS))),
    ⟨nil, nil, SS, by simp, by simp⟩, ?_⟩

Result:
α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 => ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)) s
        t →
      Computation.LiftRel
        (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
          ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
        s.destruct t.destruct
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_sdiv {x : BitVec w} : (0#w).sdiv x = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ (0#w).sdiv x = 0#w

Tactic:
simp only [sdiv_eq]

Result:
w : Nat
x : BitVec w
⊢ (match (0#w).msb, x.msb with
    | false, false => (0#w).udiv x
    | false, true => -(0#w).udiv (-x)
    | true, false => -(-0#w).udiv x
    | true, true => (-0#w).udiv (-x)) =
    0#w

Proof state:
w : Nat
x : BitVec w
⊢ (match (0#w).msb, x.msb with
    | false, false => (0#w).udiv x
    | false, true => -(0#w).udiv (-x)
    | true, false => -(-0#w).udiv x
    | true, true => (-0#w).udiv (-x)) =
    0#w

Tactic:
rcases x.msb with msb | msb <;> simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem _root_.String.validFor_toSubstring (s : String) : ValidFor [] s.1 [] s :=
  .of_eq _ (by simp [toSubstring]) rfl (by simp [toSubstring, endPos, utf8ByteSize])

Proof state:
s : String
⊢ s.toSubstring.stopPos.byteIdx = utf8Len [] + utf8Len s.data

Tactic:
simp [toSubstring, endPos, utf8ByteSize]

Result:
no goals

Proof state:
s : String
⊢ s.toSubstring.str.data = [] ++ s.data ++ []

Tactic:
simp [toSubstring]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
lemma localized₀_le_localized₀_of_smul_le {P Q : Submodule R M} (x : p) (h : x • P ≤ Q) :
    P.localized₀ p f ≤ Q.localized₀ p f

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f a r ∈ localized₀ p f Q

Tactic:
refine ⟨x • a, h ⟨a, ha, rfl⟩, x * r, ?_⟩

Result:
case intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f (x • a) (x * r) = IsLocalizedModule.mk' f a r

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
⊢ localized₀ p f P ≤ localized₀ p f Q

Tactic:
rintro - ⟨a, ha, r, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f a r ∈ localized₀ p f Q

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f (x • a) (x * r) = IsLocalizedModule.mk' f a r

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrableOn_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :
    IntegrableOn (fun x : ℝ => x ^ s * exp (-b * x ^ 2)) (Ioi 0)

Proof state:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x => x ^ s * rexp (-b * x ^ 2)) (Ioi 0) volume

Tactic:
exact integrableOn_rpow_mul_exp_neg_mul_rpow hs one_le_two hb

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive sum_lt_sum_of_nonempty]
lemma prod_lt_prod_of_nonempty' (hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) :
    (s.map f).prod < (s.map g).prod

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ i ∈ s, f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
obtain ⟨i, hi⟩ := exists_mem_of_ne_zero hs

Result:
case intro
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ i ∈ s, f i < g i
i : ι
hi : i ∈ s
⊢ (map f s).prod < (map g s).prod

Proof state:
case intro
ι : Type u_1
α : Type u_2
inst✝ : OrderedCancelCommMonoid α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ i ∈ s, f i < g i
i : ι
hi : i ∈ s
⊢ (map f s).prod < (map g s).prod

Tactic:
exact prod_lt_prod' (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem nonneg (q : ℚ) : 0 ≤ padicNorm p q :=
  if hq : q = 0 then by simp [hq, padicNorm]
  else by
    unfold padicNorm
    split_ifs
    apply zpow_nonneg
    exact mod_cast Nat.zero_le _

Proof state:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ if q = 0 then 0 else ↑p ^ (-padicValRat p q)

Tactic:
split_ifs

Result:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)

Proof state:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)

Tactic:
apply zpow_nonneg

Result:
case ha
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p

Proof state:
p : ℕ
q : ℚ
hq : q = 0
⊢ 0 ≤ padicNorm p q

Tactic:
simp [hq, padicNorm]

Result:
no goals

Proof state:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ padicNorm p q

Tactic:
unfold padicNorm

Result:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ if q = 0 then 0 else ↑p ^ (-padicValRat p q)

Proof state:
case ha
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p

Tactic:
exact mod_cast Nat.zero_le _

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- For `1 < s`, the topological sum of `ZetaAsymptotics.term (n + 1) s` over all `n : ℕ` is
`1 / (s - 1) - ζ s / s`.
-/
lemma term_tsum_of_lt {s : ℝ} (hs : 1 < s) :
    term_tsum s = (1 / (s - 1) - 1 / s * ∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s)

Proof state:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)

Tactic:
apply le_of_eq

Result:
case hab
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = (1 / ↑(n + 1)) ^ (s - 1)

Proof state:
case ha
s : ℝ
hs : 1 < s
⊢ HasSum (fun b => term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)

Tactic:
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) s)]

Result:
case ha
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, term (i + 1) s) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Proof state:
case hab
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) / ↑(n + 1) ^ s

Tactic:
norm_cast

Result:
no goals

Proof state:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 0)

Tactic:
rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]

Result:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 (0 ^ (s - 1)))
-- Mathlib/RingTheory/FractionalIdeal/Extended.lean
lemma mem_extended_iff (x : L) : (x ∈ I.extended L hf) ↔ x ∈ span B (map_f '' I)

Proof state:
case mpr
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
x : L
hx : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
⊢ x ∈ extended L hf I

Tactic:
simpa

Result:
no goals

Proof state:
case mpr
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
x : L
⊢ x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I) → x ∈ extended L hf I

Tactic:
intro hx

Result:
case mpr
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
x : L
hx : x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)
⊢ x ∈ extended L hf I

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
x : L
⊢ x ∈ extended L hf I ↔ x ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
constructor <;> { intro hx; simpa }

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem convs'Aux_succ_none {s : Stream'.Seq (Pair K)} (h : s.head = none) (n : ℕ) :
    convs'Aux s (n + 1) = 0

Proof state:
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
h : s.head = none
n : ℕ
⊢ convs'Aux s (n + 1) = 0

Tactic:
simp [convs'Aux, h]

Result:
no goals