harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem associated_linMulLin [Invertible (2 : R)] (f g : M →ₗ[R] R) :
    associated (R := R) (N := R) (linMulLin f g) =
      ⅟ (2 : R) • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)

Proof state:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ ((associated (linMulLin f g)) x✝¹) x✝ = ((⅟2 • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)) x✝¹) x✝

Tactic:
simp only [associated_apply, linMulLin_apply, map_add, smul_add, LinearMap.add_apply,
  LinearMap.smul_apply, compl₁₂_apply, mul_apply', smul_eq_mul, invOf_smul_eq_iff]

Result:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ (f x✝¹ + f x✝) * (g x✝¹ + g x✝) - f x✝¹ * g x✝¹ - f x✝ * g x✝ = 2 • (⅟2 * (f x✝¹ * g x✝)) + 2 • (⅟2 * (g x✝¹ * f x✝))

Proof state:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ (f x✝¹ + f x✝) * (g x✝¹ + g x✝) - f x✝¹ * g x✝¹ - f x✝ * g x✝ = 2 • (⅟2 * (f x✝¹ * g x✝)) + 2 • (⅟2 * (g x✝¹ * f x✝))

Tactic:
simp only [smul_add, LinearMap.smul_def, Module.End.ofNat_apply, nsmul_eq_mul, Nat.cast_ofNat,
  mul_invOf_cancel_left']

Result:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ (f x✝¹ + f x✝) * (g x✝¹ + g x✝) - f x✝¹ * g x✝¹ - f x✝ * g x✝ = f x✝¹ * g x✝ + g x✝¹ * f x✝

Proof state:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ (f x✝¹ + f x✝) * (g x✝¹ + g x✝) - f x✝¹ * g x✝¹ - f x✝ * g x✝ = f x✝¹ * g x✝ + g x✝¹ * f x✝

Tactic:
ring_nf

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
⊢ associated (linMulLin f g) = ⅟2 • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)

Tactic:
ext

Result:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ ((associated (linMulLin f g)) x✝¹) x✝ = ((⅟2 • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)) x✝¹) x✝
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem inter_nonempty_of_nonempty_of_sup_direction_eq_top {s₁ s₂ : AffineSubspace k P}
    (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty)
    (hd : s₁.direction ⊔ s₂.direction = ⊤) : ((s₁ : Set P) ∩ s₂).Nonempty

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
hlt : ⊤ < (s₁ ⊔ s₂).direction
⊢ False

Tactic:
exact not_top_lt hlt

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
⊢ (↑s₁ ∩ ↑s₂).Nonempty

Tactic:
by_contra h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ¬(↑s₁ ∩ ↑s₂).Nonempty
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
hlt : s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ False

Tactic:
rw [hd] at hlt

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
hlt : ⊤ < (s₁ ⊔ s₂).direction
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
⊢ False

Tactic:
have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
hlt : s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ¬(↑s₁ ∩ ↑s₂).Nonempty
⊢ False

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_or {x : BitVec w} : 0#w ||| x = x

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (0#w ||| x).getLsbD i = x.getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ 0#w ||| x = x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (0#w ||| x).getLsbD i = x.getLsbD i
-- Mathlib/Algebra/Algebra/Tower.lean
theorem span_smul_of_span_eq_top {s : Set S} (hs : span R s = ⊤) (t : Set A) :
    span R (s • t) = (span S t).restrictScalars R :=
  le_antisymm
    (span_le.2 fun _x ⟨p, _hps, _q, hqt, hpqx⟩ ↦ hpqx ▸ (span S t).smul_mem p (subset_span hqt))
    fun _ hp ↦ closure_induction (hx := hp) (zero_mem _) (fun _ _ _ _ ↦ add_mem) fun s0 y hy ↦ by
      refine span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
        (hs ▸ mem_top : s0 ∈ span R s)
      · rw [zero_smul]; apply zero_mem
      · intro _ _ _ _; rw [add_smul]; apply add_mem
      · intro r s0 _ hy; rw [IsScalarTower.smul_assoc]; exact smul_mem _ r hy

Proof state:
case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 ∈ span R (s • t)

Tactic:
apply zero_mem

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.realSize_tail? {s : Heap α} : s.tail? le = some s' →
    s.realSize = s'.realSize + 1

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s.realSize = s'.realSize + 1

Tactic:
intro eq

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s.realSize = s'.realSize + 1

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ tail? le s = some s' → s.realSize = s'.realSize + 1

Tactic:
simp only [Heap.tail?]

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s.realSize = s'.realSize + 1

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s.realSize = s'.realSize + 1

Tactic:
match eq₂ : s.deleteMin le, eq with
| some (a, tl), rfl => exact realSize_deleteMin eq₂

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
a : α
tl : Heap α
eq₂ : deleteMin le s = some (a, tl)
⊢ s.realSize = ((fun x => x.snd) (a, tl)).realSize + 1

Tactic:
exact realSize_deleteMin eq₂

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem charpoly_sub_diagonal_degree_lt :
    (M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n - 1)

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ↑↑(Equiv.Perm.sign c) * ∏ i : n, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)

Tactic:
rw [← C_eq_intCast, C_mul']

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ↑↑(Equiv.Perm.sign c) • ∏ i : n, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n - 1)

Tactic:
rw [charpoly, det_apply', ← insert_erase (mem_univ (Equiv.refl n)),
  sum_insert (not_mem_erase (Equiv.refl n) univ), add_comm]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (∑ x ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign x) * ∏ i : n, M.charmatrix (x i) i +
          ↑↑(Equiv.Perm.sign (Equiv.refl n)) * ∏ i : n, M.charmatrix ((Equiv.refl n) i) i -
        ∏ i : n, (X - C (M i i))).degree <
    ↑(Fintype.card n - 1)
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem closure_induction₂ {s : Set R} {p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop}
    (mem_mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy))
    (zero_left : ∀ x hx, p 0 x (zero_mem _) hx) (zero_right : ∀ x hx, p x 0 hx (zero_mem _))
    (neg_left : ∀ x y hx hy, p x y hx hy → p (-x) y (neg_mem hx) hy)
    (neg_right : ∀ x y hx hy, p x y hx hy → p x (-y) hx (neg_mem hy))
    (add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz)
    (add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz))
    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
    (mul_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
    {x y : R} (hx : x ∈ closure s) (hy : y ∈ closure s) :
    p x y hx hy

Proof state:
case mem.mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem restrict_toMeasure_support [MeasurableSingletonClass α] (p : PMF α) :
    Measure.restrict (toMeasure p) (support p) = toMeasure p

Proof state:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ (p.toMeasure.restrict p.support) s = p.toMeasure s

Tactic:
apply (MeasureTheory.Measure.restrict_apply hs).trans

Result:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ p.toMeasure (s ∩ p.support) = p.toMeasure s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
⊢ p.toMeasure.restrict p.support = p.toMeasure

Tactic:
ext s hs

Result:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ (p.toMeasure.restrict p.support) s = p.toMeasure s

Proof state:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
s : Set α
hs : MeasurableSet s
⊢ p.toMeasure (s ∩ p.support) = p.toMeasure s

Tactic:
apply toMeasure_apply_inter_support p s hs p.support_countable.measurableSet

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem self_sub_mod (n k : Nat) [NeZero k] : (n - k) % n = n - k

Proof state:
n k : Nat
inst✝ : NeZero k
⊢ (n - k) % n = n - k

Tactic:
cases n with
| zero => simp
| succ n =>
  rw [mod_eq_of_lt]
  cases k with
  | zero => simp_all
  | succ k => omega

Result:
no goals

Proof state:
case zero
k : Nat
inst✝ : NeZero k
⊢ (0 - k) % 0 = 0 - k

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ
n k : Nat
inst✝ : NeZero (k + 1)
⊢ n + 1 - (k + 1) < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case succ
k : Nat
inst✝ : NeZero k
n : Nat
⊢ (n + 1 - k) % (n + 1) = n + 1 - k

Tactic:
rw [mod_eq_of_lt]

Result:
case succ
k : Nat
inst✝ : NeZero k
n : Nat
⊢ n + 1 - k < n + 1

Proof state:
case succ.zero
n : Nat
inst✝ : NeZero 0
⊢ n + 1 - 0 < n + 1

Tactic:
simp_all

Result:
no goals

Proof state:
case succ
k : Nat
inst✝ : NeZero k
n : Nat
⊢ n + 1 - k < n + 1

Tactic:
cases k with
| zero => simp_all
| succ k => omega

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem sub_convs_eq {ifp : IntFractPair K}
    (stream_nth_eq : IntFractPair.stream v n = some ifp) :
    let g := of v
    let B := (g.contsAux (n + 1)).b
    let pB := (g.contsAux n).b
    v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Proof state:
case succ
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]

Result:
case succ
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
this : IntFractPair.stream v (n' + 1) ≠ none
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Proof state:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices v - g.convs n = 0 by simpa [ifp_fr_eq_zero]

Result:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ v - g.convs n = 0
-- Mathlib/NumberTheory/FLT/MasonStothers.lean
theorem Polynomial.abc
    {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
    (hab : IsCoprime a b) (hsum : a + b + c = 0) :
    ( natDegree a + 1 ≤ (radical (a * b * c)).natDegree ∧
      natDegree b + 1 ≤ (radical (a * b * c)).natDegree ∧
      natDegree c + 1 ≤ (radical (a * b * c)).natDegree ) ∨
      derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
⊢ IsCoprime c a

Tactic:
rw [add_eq_zero_iff_neg_eq] at hsum'

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : -(b + c) = a
⊢ IsCoprime c a

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
set w := wronskian a b with wab

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ w
⊢ divRadical (a * b * c) ∣ w

Tactic:
rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ w
⊢ divRadical a * divRadical b * divRadical c ∣ w
-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem exp_neg_one_gt_d9 : 0.36787944116 < exp (-1)

Proof state:
⊢ rexp 1 < 0.36787944116⁻¹

Tactic:
refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_

Result:
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 0.36787944116⁻¹

Proof state:
⊢ 0.36787944116 < rexp (-1)

Tactic:
rw [exp_neg, lt_inv_comm₀ _ (exp_pos _)]

Result:
⊢ rexp 1 < 0.36787944116⁻¹


⊢ 0 < 0.36787944116

Proof state:
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 0.36787944116⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 0 < 0.36787944116

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem slice_sum [AddCommMonoid α] {β : Type} (i : ℕ) (hid : i < d) (s : Finset β)
    (f : β → Holor α (d :: ds)) : (∑ x ∈ s, slice (f x) i hid) = slice (∑ x ∈ s, f x) i hid

Proof state:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ ∑ x ∈ insert a✝ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid

Tactic:
rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]

Result:
no goals

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
⊢ ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid

Tactic:
letI := Classical.decEq β

Result:
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid

Proof state:
case refine_1
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ ∅, (f x).slice i hid = (∑ x ∈ ∅, f x).slice i hid

Tactic:
simp [slice_zero]

Result:
no goals

Proof state:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid

Tactic:
intro _ _ h_not_in ih

Result:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ ∑ x ∈ insert a✝ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid

Tactic:
refine Finset.induction_on s ?_ ?_

Result:
case refine_1
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ ∅, (f x).slice i hid = (∑ x ∈ ∅, f x).slice i hid

case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid