harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem cooper_resolution_left
    {a b p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) :
    (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔
    (∃ k : Int, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p)

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p

Tactic:
have h := cooper_resolution_dvd_left
  a_pos b_pos Int.zero_lt_one (c := 1) (s := 0) (p := p) (q := q)

Result:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(a.lcm (a * 1 / ↑((a * 1).gcd 1))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * 1 ∣ 1 * k + 1 * p + a * 0
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h :
  (∃ x, p ≤ a * x ∧ b * x ≤ q ∧ 1 ∣ 1 * x + 0) ↔
    ∃ k,
      0 ≤ k ∧
        k < ↑(a.lcm (a * 1 / ↑((a * 1).gcd 1))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * 1 ∣ 1 * k + 1 * p + a * 0
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p

Tactic:
simp only [Int.mul_one, Int.one_mul, Int.mul_zero, Int.add_zero, gcd_one, Int.ofNat_one,
  Int.ediv_one, lcm_self, Int.natAbs_of_nonneg (Int.le_of_lt a_pos), Int.one_dvd, and_true,
  and_self] at h

Result:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h : (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p

Proof state:
a b p q : Int
a_pos : 0 < a
b_pos : 0 < b
h : (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p
⊢ (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔ ∃ k, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p

Tactic:
exact h

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- A slight generalisation of the **Marica-Schönheim Inequality**. -/
lemma Finset.le_card_diffs_mul_card_diffs (s t : Finset α) :
    #s * #t ≤ #(s \\ t) * #(t \\ s)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ #s * #t ≤ #(s \\ t) * #(t \\ s)

Tactic:
have : ∀ s t : Finset α, (s \\ t).map ⟨_, liftLatticeHom_injective⟩ =
    s.map ⟨_, liftLatticeHom_injective⟩ \\ t.map ⟨_, liftLatticeHom_injective⟩ := by
  rintro s t
  simp_rw [map_eq_image]
  exact image_image₂_distrib fun a b ↦ rfl

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s t : Finset α
this :
  ∀ (s t : Finset α),
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
      map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t
⊢ #s * #t ≤ #(s \\ t) * #(t \\ s)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ ∀ (s t : Finset α),
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
      map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t

Tactic:
rintro s t

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s t : Finset α
this :
  ∀ (s t : Finset α),
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
      map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t
⊢ #s * #t ≤ #(s \\ t) * #(t \\ s)

Tactic:
simpa [← card_compls (_ ⊻ _), ← map_sup, ← map_inf, ← this] using
  (s.map ⟨_, liftLatticeHom_injective⟩).le_card_infs_mul_card_sups
    (t.map ⟨_, liftLatticeHom_injective⟩)ᶜˢ

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t

Tactic:
simp_rw [map_eq_image]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) (s \\ t) =
    image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) s \\ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) t

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) (s \\ t) =
    image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) s \\ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) t

Tactic:
exact image_image₂_distrib fun a b ↦ rfl

Result:
no goals
-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` preserves localizations, then `Locally P` is stable under composition if `P` is. -/
lemma locally_stableUnderComposition (hPi : RespectsIso P) (hPl : LocalizationPreserves P)
    (hPc : StableUnderComposition P) :
    StableUnderComposition (Locally P)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : { x // x ∈ sf }
b : { x // x ∈ sg }
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
⊢ (algebraMap T (Localization.Away a')).comp (g.comp f) =
    (Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)

Tactic:
ext x

Result:
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : { x // x ∈ sf }
b : { x // x ∈ sg }
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
x : R
⊢ ((algebraMap T (Localization.Away a')).comp (g.comp f)) x =
    ((Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)) x
-- Mathlib/Algebra/FreeAlgebra.lean
theorem adjoin_range_ι : Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X)) = ⊤

Proof state:
case h_grade1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : X
⊢ ι R x ∈ S

Tactic:
exact Algebra.subset_adjoin (Set.mem_range_self _)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
⊢ S = ⊤

Tactic:
refine top_unique fun x hx => ?_

Result:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : FreeAlgebra R X
hx : x ∈ ⊤
⊢ x ∈ S

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : FreeAlgebra R X
⊢ x ∈ S

Tactic:
induction x with
| h_grade0 => exact S.algebraMap_mem _
| h_add x y hx hy => exact S.add_mem hx hy
| h_mul x y hx hy => exact S.mul_mem hx hy
| h_grade1 x => exact Algebra.subset_adjoin (Set.mem_range_self _)

Result:
no goals

Proof state:
case h_grade0
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
r✝ : R
⊢ (algebraMap R (FreeAlgebra R X)) r✝ ∈ S

Tactic:
exact S.algebraMap_mem _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : FreeAlgebra R X
hx : x ∈ ⊤
⊢ x ∈ S

Tactic:
clear hx

Result:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : FreeAlgebra R X
⊢ x ∈ S

Proof state:
case h_mul
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x * y ∈ S

Tactic:
exact S.mul_mem hx hy

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x + y ∈ S

Tactic:
exact S.add_mem hx hy

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ Algebra.adjoin R (Set.range (ι R)) = ⊤

Tactic:
set S := Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X))

Result:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
⊢ S = ⊤
-- Mathlib/Data/Seq/WSeq.lean
theorem head_terminates_of_head_tail_terminates (s : WSeq α) [T : Terminates (head (tail s))] :
    Terminates (head s) :=
  (head_terminates_iff _).2 <| by
    rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩
    simp? [tail] at h says simp only [tail, destruct_flatten, bind_map_left] at h
    rcases exists_of_mem_bind h with ⟨s', h1, _⟩
    exact terminates_of_mem h1

Proof state:
case mk.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ s.destruct.Terminates

Tactic:
simp? [tail] at h says simp only [tail, destruct_flatten, bind_map_left] at h

Result:
case mk.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  a ∈ do
    let a ← s.destruct
    (Option.rec nil Prod.snd a).destruct
⊢ s.destruct.Terminates

Proof state:
case mk.intro.intro.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  a ∈ do
    let a ← s.destruct
    (Option.rec nil Prod.snd a).destruct
s' : Option (α × WSeq α)
h1 : s' ∈ s.destruct
right✝ : a ∈ (Option.rec nil Prod.snd s').destruct
⊢ s.destruct.Terminates

Tactic:
exact terminates_of_mem h1

Result:
no goals

Proof state:
case mk.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ s.destruct.Terminates

Tactic:
simp only [tail, destruct_flatten, bind_map_left] at h

Result:
case mk.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  a ∈ do
    let a ← s.destruct
    (Option.rec nil Prod.snd a).destruct
⊢ s.destruct.Terminates

Proof state:
case mk.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  a ∈ do
    let a ← s.destruct
    (Option.rec nil Prod.snd a).destruct
⊢ s.destruct.Terminates

Tactic:
rcases exists_of_mem_bind h with ⟨s', h1, _⟩

Result:
case mk.intro.intro.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  a ∈ do
    let a ← s.destruct
    (Option.rec nil Prod.snd a).destruct
s' : Option (α × WSeq α)
h1 : s' ∈ s.destruct
right✝ : a ∈ (Option.rec nil Prod.snd s').destruct
⊢ s.destruct.Terminates

Proof state:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
⊢ s.destruct.Terminates

Tactic:
rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩

Result:
case mk.intro
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ s.destruct.Terminates
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
    (l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f

Proof state:
α : Type u_1
f : α → α
l : List α
n : Nat
h : 0 < n
⊢ (modifyHead f l).eraseIdx n = modifyHead f (l.eraseIdx n)

Tactic:
cases l <;> cases n <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_algHom {f : R[X]} (h : Splits (algebraMap R K) f) (e : K →ₐ[R] L) :
    Splits (algebraMap R L) f

Proof state:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
f : R[X]
h : Splits (algebraMap R K) f
e : K →ₐ[R] L
⊢ Splits (algebraMap R L) f

Tactic:
rw [← e.comp_algebraMap_of_tower R]

Result:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
f : R[X]
h : Splits (algebraMap R K) f
e : K →ₐ[R] L
⊢ Splits ((↑e).comp (algebraMap R K)) f

Proof state:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
f : R[X]
h : Splits (algebraMap R K) f
e : K →ₐ[R] L
⊢ Splits ((↑e).comp (algebraMap R K)) f

Tactic:
exact splits_comp_of_splits _ _ h

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
theorem fermatLastTheoremThree_case_1 {a b c : ℤ} (hdvd : ¬ 3 ∣ a * b * c) :
    a ^ 3 + b ^ 3 ≠ c ^ 3

Proof state:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ ¬↑(a ^ 3 + b ^ 3) = ↑(c ^ 3)

Tactic:
simp_rw [Int.cast_add, Int.cast_pow]

Result:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Proof state:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3

Tactic:
apply mt (congrArg (Int.cast : ℤ → ZMod 9))

Result:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ ¬↑(a ^ 3 + b ^ 3) = ↑(c ^ 3)

Proof state:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rcases cube_of_not_dvd hdvd.1.1 with ha | ha <;>
rcases cube_of_not_dvd hdvd.1.2 with hb | hb <;>
rcases cube_of_not_dvd hdvd.2 with hc | hc <;>
rw [ha, hb, hc] <;> decide

Result:
no goals

Proof state:
a b c : ℤ
hdvd : ¬3 ∣ a * b * c
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3

Tactic:
simp_rw [Int.prime_three.dvd_mul, not_or] at hdvd

Result:
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f : ℝ → ℝ` is strictly convex on `S` and right-differentiable at `x ∈ S`, then the slope of
any secant line with left endpoint at `x` is strictly greater than the right derivative of `f` at
`x`. -/
lemma lt_slope_of_hasDerivWithinAt_Ioi (hfc : StrictConvexOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Ioi x) x) :
    f' < slope f x y

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
⊢ f' < slope f x y

Tactic:
have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ f' < slope f x y

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x u < slope f x y
⊢ f' < slope f x y

Tactic:
exact (hfc.convexOn.le_slope_of_hasDerivWithinAt_Ioi hx hu hxu hf').trans_lt this

Result:
no goals

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
⊢ f' < slope f x y

Tactic:
have := hfc.secant_strict_mono hx hu hy hxu.ne' hxy.ne' huy

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f u - f x) / (u - x) < (f y - f x) / (y - x)
⊢ f' < slope f x y

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ f' < slope f x y

Tactic:
obtain ⟨u, hxu, huy⟩ := exists_between hxy

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
⊢ f' < slope f x y

Proof state:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f u - f x) / (u - x) < (f y - f x) / (y - x)
⊢ f' < slope f x y

Tactic:
simp only [← slope_def_field] at this

Result:
case intro.intro
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x u < slope f x y
⊢ f' < slope f x y
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma setIntegral_tilted [SFinite μ] (f : α → ℝ) (g : α → E) (s : Set α) :
    ∫ x in s, g x ∂(μ.tilted f) = ∫ x in s, (exp (f x) / ∫ x, exp (f x) ∂μ) • (g x) ∂μ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x => rexp (f x)) μ
⊢ 0 = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
rw [integral_undef hf']

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x => rexp (f x)) μ
⊢ 0 = ∫ (x : α) in s, (rexp (f x) / 0) • g x ∂μ
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma exists_null_set_measure_lt_of_disjoint (h : Disjoint μ ν) {ε : ℝ≥0} (hε : 0 < ε) :
    ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ε

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
refine ⟨⋂ n, t n, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ μ (⋂ n, t n) = 0

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : sInf {m | ∃ t, m = μ t + ν tᶜ} = 0
t : ℕ → Set α
ht₂ : ∀ (n : ℕ), μ (t n) + ν (t n)ᶜ < ↑ε * (1 / 2) ^ n
⊢ ν (⋂ n, t n)ᶜ ≤ 2 * ↑ε
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_multiset_of_isEmpty (α : Type u) [IsEmpty α] : #(Multiset α) = 1 :=
  Multiset.toFinsupp.toEquiv.cardinal_eq.trans (by simp)

Proof state:
α : Type u
inst✝ : IsEmpty α
⊢ #(α →₀ ℕ) = 1

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_abs_ne_one (h : |x| ≠ 1) : orderOf x = 0

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
intro n hn hx

Result:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False

Proof state:
case inr
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h✝ : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : 1 < |x|
⊢ False

Tactic:
exact ((one_lt_pow₀ h hn.ne').ne' hx).elim

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False

Tactic:
replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs hx

Result:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
⊢ False

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
⊢ False

Tactic:
rcases h.lt_or_lt with h | h

Result:
case inl
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h✝ : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : |x| < 1
⊢ False

case inr
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h✝ : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : 1 < |x|
⊢ False

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x = 0

Tactic:
rw [orderOf_eq_zero_iff']

Result:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ |x| ^ n = 1

Tactic:
simpa only [abs_one, abs_pow] using congr_arg abs hx

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝ : LinearOrderedRing G
x : G
h✝ : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : |x| < 1
⊢ False

Tactic:
exact ((pow_lt_one₀ (abs_nonneg x) h hn.ne').ne hx).elim

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_X_mul {p : R[X]} : content (X * p) = content p

Proof state:
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff (a + 1) = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
rw [mul_comm, coeff_mul_X]

Result:
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (fun x => (X * p).coeff x.succ) p.support.val = Multiset.map p.coeff p.support.val

Tactic:
refine congr (congr rfl ?_) rfl

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ (fun x => (X * p).coeff x.succ) = p.coeff