harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem testBit_ofBits_lt (f : Fin n → Bool) (i : Nat) (h : i < n) :
    (ofBits f).testBit i = f ⟨i, h⟩

Proof state:
case succ
n : Nat
ih : ∀ (f : Fin n → Bool) (i : Nat) (h : i < n), (ofBits f).testBit i = f ⟨i, h⟩
f : Fin (n + 1) → Bool
i : Nat
h : i < n + 1
⊢ (ofBits f).testBit i = f ⟨i, h⟩

Tactic:
simp only [ofBits_succ]

Result:
case succ
n : Nat
ih : ∀ (f : Fin n → Bool) (i : Nat) (h : i < n), (ofBits f).testBit i = f ⟨i, h⟩
f : Fin (n + 1) → Bool
i : Nat
h : i < n + 1
⊢ (2 * ofBits (f ∘ Fin.succ) + (f 0).toNat).testBit i = f ⟨i, h⟩

Proof state:
n : Nat
ih : ∀ (f : Fin n → Bool) (i : Nat) (h : i < n), (ofBits f).testBit i = f ⟨i, h⟩
f : Fin (n + 1) → Bool
i : Nat
h : 0 < n + 1
⊢ (2 * ofBits (f ∘ Fin.succ) + (f 0).toNat).testBit 0 = f ⟨0, h⟩

Tactic:
simp [mod_eq_of_lt (Bool.toNat_lt _)]

Result:
no goals

Proof state:
n : Nat
ih : ∀ (f : Fin n → Bool) (i : Nat) (h : i < n), (ofBits f).testBit i = f ⟨i, h⟩
f : Fin (n + 1) → Bool
i✝ i : Nat
h : i + 1 < n + 1
⊢ (2 * ofBits (f ∘ Fin.succ) + (f 0).toNat).testBit (i + 1) = f ⟨i + 1, h⟩

Tactic:
rw [testBit_add_one, mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt (Bool.toNat_lt _)]

Result:
n : Nat
ih : ∀ (f : Fin n → Bool) (i : Nat) (h : i < n), (ofBits f).testBit i = f ⟨i, h⟩
f : Fin (n + 1) → Bool
i✝ i : Nat
h : i + 1 < n + 1
⊢ (ofBits (f ∘ Fin.succ) + 0).testBit i = f ⟨i + 1, h⟩

Proof state:
n : Nat
ih : ∀ (f : Fin n → Bool) (i : Nat) (h : i < n), (ofBits f).testBit i = f ⟨i, h⟩
f : Fin (n + 1) → Bool
i✝ i : Nat
h : i + 1 < n + 1
⊢ (ofBits (f ∘ Fin.succ) + 0).testBit i = f ⟨i + 1, h⟩

Tactic:
exact ih (f ∘ Fin.succ) i (Nat.lt_of_succ_lt_succ h)

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ (f : Fin n → Bool) (i : Nat) (h : i < n), (ofBits f).testBit i = f ⟨i, h⟩
f : Fin (n + 1) → Bool
i : Nat
h : i < n + 1
⊢ (2 * ofBits (f ∘ Fin.succ) + (f 0).toNat).testBit i = f ⟨i, h⟩

Tactic:
match i with
| 0 => simp [mod_eq_of_lt (Bool.toNat_lt _)]
| i+1 =>
  rw [testBit_add_one, mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt (Bool.toNat_lt _)]
  exact ih (f ∘ Fin.succ) i (Nat.lt_of_succ_lt_succ h)

Result:
no goals

Proof state:
n : Nat
f : Fin n → Bool
i : Nat
h : i < n
⊢ (ofBits f).testBit i = f ⟨i, h⟩

Tactic:
induction n generalizing i with
| zero => contradiction
| succ n ih =>
  simp only [ofBits_succ]
  match i with
  | 0 => simp [mod_eq_of_lt (Bool.toNat_lt _)]
  | i+1 =>
    rw [testBit_add_one, mul_add_div Nat.zero_lt_two, Nat.div_eq_of_lt (Bool.toNat_lt _)]
    exact ih (f ∘ Fin.succ) i (Nat.lt_of_succ_lt_succ h)

Result:
no goals

Proof state:
case zero
f : Fin 0 → Bool
i : Nat
h : i < 0
⊢ (ofBits f).testBit i = f ⟨i, h⟩

Tactic:
contradiction

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma cross_comm (v w : ℙ F (Fin 3 → F)) : cross v w = cross w v

Proof state:
case inr.h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ (mk F v hv).cross (mk F w hw) = (mk F w hw).cross (mk F v hv)

Tactic:
rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
  ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

Result:
no goals

Proof state:
case inl
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v.cross v

Tactic:
rfl

Result:
no goals

Proof state:
case inr.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
w : ℙ F (Fin 3 → F)
v : Fin 3 → F
hv : v ≠ 0
h : mk F v hv ≠ w
⊢ (mk F v hv).cross w = w.cross (mk F v hv)

Tactic:
induction w with | h w hw =>
rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
  ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
⊢ v.cross w = w.cross v

Tactic:
rcases eq_or_ne v w with rfl | h

Result:
case inl
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v.cross v

case inr
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ v.cross w = w.cross v

Proof state:
case inr
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ v.cross w = w.cross v

Tactic:
induction v with | h v hv =>
induction w with | h w hw =>
rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
  ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma FermatLastTheoremWith.mono (hmn : m ∣ n) (hm : FermatLastTheoremWith α m) :
    FermatLastTheoremWith α n

Proof state:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : NoZeroDivisors α
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremWith α m
⊢ FermatLastTheoremWith α n

Tactic:
rintro a b c ha hb hc

Result:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : NoZeroDivisors α
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremWith α m
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ n + b ^ n ≠ c ^ n

Proof state:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : NoZeroDivisors α
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremWith α m
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
obtain ⟨k, rfl⟩ := hmn

Result:
case intro
α : Type u_1
inst✝¹ : Semiring α
inst✝ : NoZeroDivisors α
m : ℕ
hm : FermatLastTheoremWith α m
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ (m * k) + b ^ (m * k) ≠ c ^ (m * k)

Proof state:
case intro
α : Type u_1
inst✝¹ : Semiring α
inst✝ : NoZeroDivisors α
m : ℕ
hm : FermatLastTheoremWith α m
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ (m * k) + b ^ (m * k) ≠ c ^ (m * k)

Tactic:
simp_rw [pow_mul']

Result:
case intro
α : Type u_1
inst✝¹ : Semiring α
inst✝ : NoZeroDivisors α
m : ℕ
hm : FermatLastTheoremWith α m
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ (a ^ k) ^ m + (b ^ k) ^ m ≠ (c ^ k) ^ m

Proof state:
case intro
α : Type u_1
inst✝¹ : Semiring α
inst✝ : NoZeroDivisors α
m : ℕ
hm : FermatLastTheoremWith α m
a b c : α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ (a ^ k) ^ m + (b ^ k) ^ m ≠ (c ^ k) ^ m

Tactic:
refine hm _ _ _ ?_ ?_ ?_ <;> exact pow_ne_zero _ ‹_›

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem exists_isBasis_disjoint_isBasis_of_subset (M : Matroid α) {X Y : Set α} (hXY : X ⊆ Y)
    (hY : Y ⊆ M.E

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J

Tactic:
refine ⟨I, I' \ I, hI, by rwa [union_diff_self, union_eq_self_of_subset_left hII'], ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ Disjoint X (I' \ I)

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
e : α
heX : e ∈ X
heI' : e ∈ I'
heI : e ∉ I
⊢ False

Tactic:
exact heI <| hI.mem_of_insert_indep heX (hI'.indep.subset (insert_subset heI' hII'))

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ ∀ ⦃a : α⦄, a ∈ X → ∀ ⦃b : α⦄, b ∈ I' \ I → a ≠ b

Tactic:
rintro e heX _ ⟨heI', heI⟩ rfl

Result:
case intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
e : α
heX : e ∈ X
heI' : e ∈ I'
heI : e ∉ I
⊢ False

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J

Tactic:
obtain ⟨I, I', hI, hI', hII'⟩ := M.exists_isBasis_subset_isBasis hXY

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ M.IsBasis (I ∪ I' \ I) Y

Tactic:
rwa [union_diff_self, union_eq_self_of_subset_left hII']

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ Disjoint X (I' \ I)

Tactic:
rw [disjoint_iff_forall_ne]

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ ∀ ⦃a : α⦄, a ∈ X → ∀ ⦃b : α⦄, b ∈ I' \ I → a ≠ b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y

Proof state:
w : Nat
x y : BitVec w
⊢ ~~~x = y ↔ x = ~~~y

Tactic:
constructor

Result:
case mp
w : Nat
x y : BitVec w
⊢ ~~~x = y → x = ~~~y

case mpr
w : Nat
x y : BitVec w
⊢ x = ~~~y → ~~~x = y

Proof state:
case mp
w : Nat
x y : BitVec w
h : ~~~x = y
⊢ x = ~~~~~~x

Tactic:
simp

Result:
no goals

Proof state:
case mpr
w : Nat
x y : BitVec w
h : x = ~~~y
⊢ ~~~~~~y = y

Tactic:
simp

Result:
no goals

Proof state:
case mp
w : Nat
x y : BitVec w
⊢ ~~~x = y → x = ~~~y

Tactic:
intro h

Result:
case mp
w : Nat
x y : BitVec w
h : ~~~x = y
⊢ x = ~~~y

Proof state:
case mpr
w : Nat
x y : BitVec w
h : x = ~~~y
⊢ ~~~x = y

Tactic:
rw [h]

Result:
case mpr
w : Nat
x y : BitVec w
h : x = ~~~y
⊢ ~~~~~~y = y

Proof state:
case mpr
w : Nat
x y : BitVec w
⊢ x = ~~~y → ~~~x = y

Tactic:
intro h

Result:
case mpr
w : Nat
x y : BitVec w
h : x = ~~~y
⊢ ~~~x = y

Proof state:
case mp
w : Nat
x y : BitVec w
h : ~~~x = y
⊢ x = ~~~y

Tactic:
rw [← h]

Result:
case mp
w : Nat
x y : BitVec w
h : ~~~x = y
⊢ x = ~~~~~~x
-- Mathlib/Data/List/Basic.lean
theorem replicate_right_inj' {a b : α} : ∀ {n},
    replicate n a = replicate n b ↔ n = 0 ∨ a = b
  | 0 => by simp
  | n + 1 => (replicate_right_inj n.succ_ne_zero).trans <| by simp only [n.succ_ne_zero, false_or]

Proof state:
α : Type u
a b : α
⊢ replicate 0 a = replicate 0 b ↔ 0 = 0 ∨ a = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a b : α
n : ℕ
⊢ a = b ↔ n + 1 = 0 ∨ a = b

Tactic:
simp only [n.succ_ne_zero, false_or]

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
lemma analyticOnNhd_iteratedDeriv_mgf (n : ℕ) :
    AnalyticOnNhd ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
exact analyticOnNhd_mgf.iterated_deriv n

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))

Tactic:
rw [iteratedDeriv_eq_iterate]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
⊢ AnalyticOnNhd ℝ (deriv^[n] (mgf X μ)) (interior (integrableExpSet X μ))
-- Mathlib/CategoryTheory/Limits/Sifted.lean
/-- Being sifted is preserved by equivalences of categories -/
lemma isSifted_of_equiv [IsSifted C] {D : Type u₁} [Category.{v₁} D] (e : D ≌ C) : IsSifted D :=
  letI : Final (diag D)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
sq : e.inverse ⋙ Functor.diag D ⋙ this.functor ≅ Functor.diag C
⊢ (Functor.diag D).Final

Tactic:
apply_rules [final_iff_comp_equivalence _ this.functor|>.mpr,
  final_iff_final_comp e.inverse _ |>.mpr, final_of_natIso sq.symm]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
c : C
⊢ (e.functor.obj (e.inverse.obj c), e.functor.obj (e.inverse.obj c)) ≅ (c, c)

Tactic:
exact Iso.prod (e.counitIso.app c) (e.counitIso.app c)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
⊢ (Functor.diag D).Final

Tactic:
have sq : (e.inverse ⋙ diag D ⋙ this.functor ≅ diag C) :=
    NatIso.ofComponents (fun c ↦ by dsimp [this]
                                    exact Iso.prod (e.counitIso.app c) (e.counitIso.app c))

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
sq : e.inverse ⋙ Functor.diag D ⋙ this.functor ≅ Functor.diag C
⊢ (Functor.diag D).Final

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
c : C
⊢ (e.inverse ⋙ Functor.diag D ⋙ this.functor).obj c ≅ (Functor.diag C).obj c

Tactic:
dsimp [this]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
c : C
⊢ (e.functor.obj (e.inverse.obj c), e.functor.obj (e.inverse.obj c)) ≅ (c, c)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
⊢ (Functor.diag D).Final

Tactic:
letI : D × D ≌ C × C:= Equivalence.prod e e

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
⊢ (Functor.diag D).Final
-- Mathlib/RingTheory/LaurentSeries.lean
theorem intValuation_le_iff_coeff_lt_eq_zero {d : ℕ} (f : K⟦X⟧) :
    Valued.v (f : K⸨X⸩) ≤ Multiplicative.ofAdd (-d : ℤ) ↔
      ∀ n : ℕ, n < d → coeff K n f = 0

Proof state:
K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0
⊢ Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0

Tactic:
erw [← this, valuation_of_algebraMap (PowerSeries.idealX K) f, ←
  span_singleton_dvd_span_singleton_iff_dvd, ← Ideal.span_singleton_pow]

Result:
K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0
⊢ (PowerSeries.idealX K).intValuation f ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔
    Ideal.span {PowerSeries.X} ^ d ∣ Ideal.span {f}

Proof state:
K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
⊢ Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0

Tactic:
have : PowerSeries.X ^ d ∣ f ↔ ∀ n : ℕ, n < d → (PowerSeries.coeff K n) f = 0 :=
  ⟨PowerSeries.X_pow_dvd_iff.mp, PowerSeries.X_pow_dvd_iff.mpr⟩

Result:
K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0
⊢ Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0

Proof state:
K : Type u_2
inst✝ : Field K
d : ℕ
f : K⟦X⟧
this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0
⊢ (PowerSeries.idealX K).intValuation f ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔
    Ideal.span {PowerSeries.X} ^ d ∣ Ideal.span {f}

Tactic:
apply intValuation_le_pow_iff_dvd

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem radical_mul : radical (I * J) = radical I ⊓ radical J

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Tactic:
have := radical_mono <| @mul_le_inf _ _ I J

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
this : (I * J).radical ≤ (I ⊓ J).radical
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
refine le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
  ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
this : (I * J).radical ≤ I.radical ⊓ J.radical
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
this : (I * J).radical ≤ (I ⊓ J).radical
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Tactic:
simp_rw [radical_inf I J] at this

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
this : (I * J).radical ≤ I.radical ⊓ J.radical
⊢ (I * J).radical ≤ I.radical ⊓ J.radical
-- Mathlib/Data/NNReal/Defs.lean
theorem image_real_toNNReal (h : s.OrdConnected) : (Real.toNNReal '' s).OrdConnected

Proof state:
case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

Tactic:
rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz

Result:
case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : x.toNNReal ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

Proof state:
case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : x.toNNReal ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

Tactic:
exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩

Result:
no goals

Proof state:
case inr
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s

Tactic:
lift y to ℝ≥0 using hy₀

Result:
case inr.intro
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc x.toNNReal (↑y).toNNReal
⊢ z ∈ toNNReal '' s

Proof state:
s : Set ℝ
h : s.OrdConnected
⊢ (toNNReal '' s).OrdConnected

Tactic:
refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩

Result:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
⊢ z ∈ toNNReal '' s

Proof state:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
⊢ z ∈ toNNReal '' s

Tactic:
rcases le_total y 0 with hy₀ | hy₀

Result:
case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

case inr
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s

Proof state:
case inr.intro
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc x.toNNReal y
⊢ z ∈ toNNReal '' s

Tactic:
exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩

Result:
no goals

Proof state:
case inr.intro
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc x.toNNReal (↑y).toNNReal
⊢ z ∈ toNNReal '' s

Tactic:
rw [toNNReal_coe] at hz

Result:
case inr.intro
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc x.toNNReal y
⊢ z ∈ toNNReal '' s
-- Mathlib/Data/TypeVec.lean
theorem subtypeVal_toSubtype {α : TypeVec n} (p : α ⟹ «repeat» n Prop) :
    subtypeVal p ⊚ toSubtype p = fun _ => Subtype.val

Proof state:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ subtypeVal p ⊚ toSubtype p = fun x => Subtype.val

Tactic:
ext i x

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (p i x) }) i
⊢ (subtypeVal p ⊚ toSubtype p) i x = ↑x

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (p i x) }) i
⊢ (subtypeVal p ⊚ toSubtype p) i x = ↑x

Tactic:
induction i <;> simp only [toSubtype, comp, subtypeVal] at *

Result:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : { x // ofRepeat (p a✝ x) }),
    subtypeVal p a✝ (toSubtype p a✝ x) = ↑x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p a✝.fs x) }
⊢ subtypeVal (dropFun p) a✝ (toSubtype (dropFun p) a✝ x) = ↑x

Proof state:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : { x // ofRepeat (p a✝ x) }),
    subtypeVal p a✝ (toSubtype p a✝ x) = ↑x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p a✝.fs x) }
⊢ subtypeVal (dropFun p) a✝ (toSubtype (dropFun p) a✝ x) = ↑x

Tactic:
simp [*]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isCompact :
    IsCompact (U : Set X)

Proof state:
case h.e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U = ⇑(ConcreteCategory.hom hU.fromSpec.base) '' Set.univ

Tactic:
convert hU.range_fromSpec.symm

Result:
case h.e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) '' Set.univ = Set.range ⇑(ConcreteCategory.hom hU.fromSpec.base)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Continuous ⇑(ConcreteCategory.hom hU.fromSpec.base)

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) '' Set.univ = Set.range ⇑(ConcreteCategory.hom hU.fromSpec.base)

Tactic:
exact Set.image_univ

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact ↑U

Tactic:
convert @IsCompact.image _ _ _ _ Set.univ hU.fromSpec.base PrimeSpectrum.compactSpace.1
  (by fun_prop)

Result:
case h.e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U = ⇑(ConcreteCategory.hom hU.fromSpec.base) '' Set.univ
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_ldiff : ∀ m n : Num, (ldiff m n : ℕ) = Nat.ldiff m n

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff (PosNum.bit b✝ n✝) = bit (a✝ && !b✝) (m✝.ldiff n✝)

Tactic:
try cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit false n✝) = bit (false && !false) (m✝.ldiff n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit true n✝) = bit (false && !true) (m✝.ldiff n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit false n✝) = bit (true && !false) (m✝.ldiff n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit true n✝) = bit (true && !true) (m✝.ldiff n✝)

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ (PosNum.bit a✝ m✝).ldiff (PosNum.bit b✝ n✝) = bit (a✝ && !b✝) (m✝.ldiff n✝)

Tactic:
cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit false n✝) = bit (false && !false) (m✝.ldiff n✝)

case pbb.false.true
m✝ n✝ : PosNum
⊢ (PosNum.bit false m✝).ldiff (PosNum.bit true n✝) = bit (false && !true) (m✝.ldiff n✝)

case pbb.true.false
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit false n✝) = bit (true && !false) (m✝.ldiff n✝)

case pbb.true.true
m✝ n✝ : PosNum
⊢ (PosNum.bit true m✝).ldiff (PosNum.bit true n✝) = bit (true && !true) (m✝.ldiff n✝)

Proof state:
⊢ ∀ (m n : Num), ↑(m.ldiff n) = (↑m).ldiff ↑n

Tactic:
apply castNum_eq_bitwise PosNum.ldiff <;> intros <;> (try cases_type* Bool) <;> rfl

Result:
no goals