harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem monic_descPochhammer (n : ℕ) [Nontrivial R] [NoZeroDivisors R] :
    Monic <| descPochhammer R n

Proof state:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
⊢ (descPochhammer R (n + 1)).Monic

Tactic:
have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)

Result:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
this : (X - 1).natDegree ≠ 0
⊢ (descPochhammer R (n + 1)).Monic

Proof state:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
this : (X - 1).natDegree ≠ 0
⊢ (descPochhammer R (n + 1)).Monic

Tactic:
rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
    one_mul, one_mul, h, one_pow]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
⊢ (descPochhammer R (n + 1)).Monic

Tactic:
have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1

Result:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
h : (X - 1).leadingCoeff = 1
⊢ (descPochhammer R (n + 1)).Monic

Proof state:
R : Type u
inst✝² : Ring R
n : ℕ
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
⊢ (descPochhammer R n).Monic

Tactic:
induction' n with n hn

Result:
case zero
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
⊢ (descPochhammer R 0).Monic

case succ
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
n : ℕ
hn : (descPochhammer R n).Monic
⊢ (descPochhammer R (n + 1)).Monic

Proof state:
case zero
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
⊢ (descPochhammer R 0).Monic

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₁_eq_zero (h : ¬ c₁.Rel i₁ (c₁.next i₁)) :
    K.d₁ c₁₂ i₁ i₂ i₁₂ = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
dsimp [d₁]

Result:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ =
    0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ =
    0

Tactic:
rw [K.shape_f _ _ h, zero_comp, smul_zero]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem terminates_map_iff {f : α → β} {s : Seq α}  :
    (map f s).Terminates ↔ s.Terminates

Proof state:
α : Type u
β : Type v
f : α → β
s : Seq α
⊢ (map f s).Terminates ↔ s.Terminates

Tactic:
simp [Terminates]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma map_cotangentComplex (f : Hom P P') (x) :
    CotangentSpace.map f (P.cotangentComplex x) = P'.cotangentComplex (.map f x)

Proof state:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : P.Cotangent
⊢ (CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Cotangent.map f) x)

Tactic:
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x

Result:
case intro
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
⊢ (CotangentSpace.map f) (P.cotangentComplex (Cotangent.mk x)) =
    P'.cotangentComplex ((Cotangent.map f) (Cotangent.mk x))

Proof state:
case intro
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : ↥P.ker
⊢ (CotangentSpace.map f) (P.cotangentComplex (Cotangent.mk x)) =
    P'.cotangentComplex ((Cotangent.map f) (Cotangent.mk x))

Tactic:
rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_flatten (l : Vector (Vector β m) n) (i : Nat) (hi : i < n * m) :
    l.flatten[i] =
      haveI : i / m < n

Proof state:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
⊢ a.toList[i] = (a :: l)[i / m][i % m]

Tactic:
have h₁ : i / m = 0 := Nat.div_eq_of_lt h

Result:
case pos
β : Type u_1
m : Nat
a : Vector β m
l : List (Vector β m)
ih :
  ∀ (i : Nat) (hi : i < { toList := l }.size * m),
    (List.map Array.toList (List.map toArray l)).flatten[i] = l[i / m][i % m]
i : Nat
hi : i < { toList := a :: l }.size * m
h : i < m
h₁ : i / m = 0
⊢ a.toList[i] = (a :: l)[i / m][i % m]
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem nat_le_order (φ : R⟦X⟧) (n : ℕ) (h : ∀ i < n, coeff R i φ = 0) : ↑n ≤ order φ

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
⊢ ↑n ≤ φ.order

Tactic:
by_contra H

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
H : ¬↑n ≤ φ.order
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
H : ¬↑n ≤ φ.order
⊢ False

Tactic:
rw [not_le] at H

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
H : φ.order < ↑n
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
H : φ.order < ↑n
lt_top : φ.order < ⊤
⊢ False

Tactic:
replace H : (order φ).lift lt_top < n := by simpa

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
lt_top : φ.order < ⊤
H : φ.order.lift lt_top < n
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
lt_top : φ.order < ⊤
H : φ.order.lift lt_top < n
⊢ False

Tactic:
exact coeff_order lt_top (h _ H)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
H : φ.order < ↑n
⊢ False

Tactic:
have lt_top : order φ < ⊤ := lt_top_of_lt H

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
H : φ.order < ↑n
lt_top : φ.order < ⊤
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff R i) φ = 0
H : φ.order < ↑n
lt_top : φ.order < ⊤
⊢ φ.order.lift lt_top < n

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_eq_getValueCastD [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α}
    {fallback : β} : getValueD a l fallback = getValueCastD a l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((_ : α) × β)
a : α
fallback : β
⊢ getValueD a l fallback = getValueCastD a l fallback

Tactic:
simp only [getValueD_eq_getValue?, getValueCastD_eq_getValueCast?, getValue?_eq_getValueCast?]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_add_one_sq_lt_ack_add_three : ∀ m n, (ack m n + 1) ^ 2 ≤ ack (m + 3) n
  | 0, n => by simpa using sq_le_two_pow_add_one_minus_three (n + 2)
  | m + 1, 0 => by
    rw [ack_succ_zero, ack_succ_zero]
    apply ack_add_one_sq_lt_ack_add_three
  | m + 1, n + 1 => by
    rw [ack_succ_succ, ack_succ_succ]
    apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)
    omega

Proof state:
m n : ℕ
⊢ (ack (m + 1) (n + 1) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Result:
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)

Proof state:
m : ℕ
⊢ (ack (m + 1) 0 + 1) ^ 2 ≤ ack (m + 1 + 3) 0

Tactic:
rw [ack_succ_zero, ack_succ_zero]

Result:
m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1

Proof state:
n : ℕ
⊢ (ack 0 n + 1) ^ 2 ≤ ack (0 + 3) n

Tactic:
simpa using sq_le_two_pow_add_one_minus_three (n + 2)

Result:
no goals

Proof state:
m n : ℕ
⊢ m + 1 ≤ m + 3 + 1

Tactic:
omega

Result:
no goals

Proof state:
m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1

Tactic:
apply ack_add_one_sq_lt_ack_add_three

Result:
no goals

Proof state:
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)

Tactic:
apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)

Result:
m n : ℕ
⊢ m + 1 ≤ m + 3 + 1
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_pos {a b : Ordinal} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b

Proof state:
a b : Ordinal.{u_4}
h₁ : 0 < a
h₂ : 0 < b
⊢ 0 < a * b

Tactic:
simpa only [mul_zero] using mul_lt_mul_of_pos_left h₂ h₁

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem finrank_sup_add_finrank_inf_eq (s t : Submodule K V) [FiniteDimensional K s]
    [FiniteDimensional K t] :
    finrank K ↑(s ⊔ t) + finrank K ↑(s ⊓ t) = finrank K ↑s + finrank K ↑t

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + ↑(finrank K ↥t)
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
norm_cast at key

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
repeat rw [← finrank_eq_rank] at key

Result:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + ↑(finrank K ↥t)
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
rw [← finrank_eq_rank] at key

Result:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + ↑(finrank K ↥t)
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
have key : Module.rank K ↑(s ⊔ t) + Module.rank K ↑(s ⊓ t) = Module.rank K s + Module.rank K t :=
  rank_sup_add_rank_inf_eq s t

Result:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem rank_eq_one_iff [Module.Free K V] :
    Module.rank K V = 1 ↔ ∃ v₀ : V, v₀ ≠ 0 ∧ ∀ v, ∃ r : K, r • v₀ = v

Proof state:
case refine_1.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hv : ∀ (v : V), ∃ r, r • v₀ = v
hzero : v₀ = 0
⊢ False

Tactic:
simp_rw [hzero, smul_zero, exists_const] at hv

Result:
case refine_1.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_flatMap (xs : Array α) (f : α → Array β) (p : β → Bool) :
    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p)

Proof state:
α : Type u_1
β : Type u_2
xs : Array α
f : α → Array β
p : β → Bool
⊢ find? p (flatMap f xs) = findSome? (fun x => find? p (f x)) xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
p : β → Bool
toList✝ : List α
⊢ find? p (flatMap f { toList := toList✝ }) = findSome? (fun x => find? p (f x)) { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
p : β → Bool
toList✝ : List α
⊢ find? p (flatMap f { toList := toList✝ }) = findSome? (fun x => find? p (f x)) { toList := toList✝ }

Tactic:
simp [List.find?_flatMap, Array.flatMap_toArray]

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem StrictConvexOn.secant_strict_mono_aux1 (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s)
    (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (z - x) * f y < (z - y) * f x + (y - x) * f z

Proof state:
case calc_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z = ((z - y) * f x + (y - x) * f z) / (z - x)

Tactic:
field_simp

Result:
no goals

Proof state:
case calc_1.e_a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ y = (z - y) / (z - x) * x + (y - x) / (z - x) * z

Tactic:
field_simp

Result:
case calc_1.e_a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ y * (z - x) = (z - y) * x + (y - x) * z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem sub_eq_add_neg (l₁ l₂ : LinearCombo) : l₁ - l₂ = l₁ + -l₂

Proof state:
l₁ l₂ : LinearCombo
⊢ l₁ - l₂ = l₁ + -l₂

Tactic:
rcases l₁ with ⟨a₁, c₁⟩

Result:
case mk
l₂ : LinearCombo
a₁ : Int
c₁ : Coeffs
⊢ { const := a₁, coeffs := c₁ } - l₂ = { const := a₁, coeffs := c₁ } + -l₂

Proof state:
case mk
l₂ : LinearCombo
a₁ : Int
c₁ : Coeffs
⊢ { const := a₁, coeffs := c₁ } - l₂ = { const := a₁, coeffs := c₁ } + -l₂

Tactic:
rcases l₂ with ⟨a₂, c₂⟩

Result:
case mk.mk
a₁ : Int
c₁ : Coeffs
a₂ : Int
c₂ : Coeffs
⊢ { const := a₁, coeffs := c₁ } - { const := a₂, coeffs := c₂ } =
    { const := a₁, coeffs := c₁ } + -{ const := a₂, coeffs := c₂ }

Proof state:
case mk.mk.w₁
a₁ : Int
c₁ : Coeffs
a₂ : Int
c₂ : Coeffs
⊢ ({ const := a₁, coeffs := c₁ } - { const := a₂, coeffs := c₂ }).const =
    ({ const := a₁, coeffs := c₁ } + -{ const := a₂, coeffs := c₂ }).const

Tactic:
simp [Int.sub_eq_add_neg]

Result:
no goals

Proof state:
case mk.mk
a₁ : Int
c₁ : Coeffs
a₂ : Int
c₂ : Coeffs
⊢ { const := a₁, coeffs := c₁ } - { const := a₂, coeffs := c₂ } =
    { const := a₁, coeffs := c₁ } + -{ const := a₂, coeffs := c₂ }

Tactic:
apply ext

Result:
case mk.mk.w₁
a₁ : Int
c₁ : Coeffs
a₂ : Int
c₂ : Coeffs
⊢ ({ const := a₁, coeffs := c₁ } - { const := a₂, coeffs := c₂ }).const =
    ({ const := a₁, coeffs := c₁ } + -{ const := a₂, coeffs := c₂ }).const

case mk.mk.w₂
a₁ : Int
c₁ : Coeffs
a₂ : Int
c₂ : Coeffs
⊢ ({ const := a₁, coeffs := c₁ } - { const := a₂, coeffs := c₂ }).coeffs =
    ({ const := a₁, coeffs := c₁ } + -{ const := a₂, coeffs := c₂ }).coeffs

Proof state:
case mk.mk.w₂
a₁ : Int
c₁ : Coeffs
a₂ : Int
c₂ : Coeffs
⊢ ({ const := a₁, coeffs := c₁ } - { const := a₂, coeffs := c₂ }).coeffs =
    ({ const := a₁, coeffs := c₁ } + -{ const := a₂, coeffs := c₂ }).coeffs

Tactic:
simp [Coeffs.sub_eq_add_neg]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma completedSinZeta_neg (a : UnitAddCircle) (s : ℂ) :
    completedSinZeta (-a) s = -completedSinZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedSinZeta (-a) s = -completedSinZeta a s

Tactic:
simp [completedSinZeta, StrongFEPair.Λ, mellin, StrongFEPair.symm, WeakFEPair.symm,
  hurwitzOddFEPair, sinKernel_neg, integral_neg, neg_div]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem circulant_injective [AddGroup n] : Injective (circulant : (n → α) → Matrix n n α)

Proof state:
case h
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k

Tactic:
rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
⊢ Injective circulant

Tactic:
intro v w h

Result:
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
⊢ v = w

Proof state:
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
⊢ v = w

Tactic:
ext k

Result:
case h
α : Type u_1
n : Type u_3
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k
-- Mathlib/Data/ENNReal/Real.lean
theorem le_ofReal_iff_toReal_le {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ∞) (hb : 0 ≤ b) :
    a ≤ ENNReal.ofReal b ↔ ENNReal.toReal a ≤ b

Proof state:
a : ℝ≥0∞
b : ℝ
ha : a ≠ ⊤
hb : 0 ≤ b
⊢ a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
b : ℝ
hb : 0 ≤ b
a : ℝ≥0
⊢ ↑a ≤ ENNReal.ofReal b ↔ (↑a).toReal ≤ b

Proof state:
case intro
b : ℝ
hb : 0 ≤ b
a : ℝ≥0
⊢ ↑a ≤ ENNReal.ofReal b ↔ (↑a).toReal ≤ b

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.le_toNNReal_iff_coe_le hb

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Yoneda.lean
lemma Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy [Mon_Class X] :
    Mon_ClassOfRepresentableBy X _ (yonedaMonObjRepresentableBy X) = ‹_›

Proof state:
case one
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ toUnit (𝟙_ C) ≫ η = η

Tactic:
rw [toUnit_unique (toUnit _) (𝟙 _), Category.id_comp]

Result:
no goals

Proof state:
case one
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ η = η

Tactic:
show toUnit _ ≫ η = η

Result:
case one
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ toUnit (𝟙_ C) ≫ η = η

Proof state:
case mul
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ lift (fst X X) (snd X X) ≫ μ = μ

Tactic:
rw [lift_fst_snd, Category.id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ Mon_ClassOfRepresentableBy X (yonedaMonObj X) (yonedaMonObjRepresentableBy X) = inst✝

Tactic:
ext

Result:
case one
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ η = η

case mul
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ μ = μ

Proof state:
case mul
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ μ = μ

Tactic:
show lift (fst X X) (snd X X) ≫ μ = μ

Result:
case mul
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
X : C
inst✝ : Mon_Class X
⊢ lift (fst X X) (snd X X) ≫ μ = μ