harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
@[to_additive tsum_eq_tsum_primes_of_support_subset_prime_powers]
lemma tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers {f : ℕ → α}
    (hfm : Multipliable f) (hf : Function.mulSupport f ⊆ {n | IsPrimePow n}) :
    ∏' n : ℕ, f n = ∏' (p : Nat.Primes) (k : ℕ), f (p ^ (k + 1))

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))

Tactic:
have hfm' : Multipliable fun pk : Nat.Primes × ℕ ↦ f (pk.fst ^ (pk.snd + 1)) :=
  prodNatEquiv.symm.multipliable_iff.mp <| by
    simpa only [← coe_prodNatEquiv_apply, Prod.eta, Function.comp_def, Equiv.apply_symm_apply]
      using hfm.subtype _

Result:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfm' : Multipliable fun pk => f (↑pk.1 ^ (pk.2 + 1))
⊢ ∏' (n : ℕ), f n = ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ Multipliable ((fun pk => f (↑pk.1 ^ (pk.2 + 1))) ∘ ⇑prodNatEquiv.symm)

Tactic:
simpa only [← coe_prodNatEquiv_apply, Prod.eta, Function.comp_def, Equiv.apply_symm_apply]
  using hfm.subtype _

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfm' : Multipliable fun pk => f (↑pk.1 ^ (pk.2 + 1))
⊢ ∏' (c : Nat.Primes × ℕ), f ↑(prodNatEquiv c) = ∏' (p : Nat.Primes × ℕ), f (↑p.1 ^ (p.2 + 1))

Tactic:
refine tprod_congr fun (p, k) ↦ congrArg f <| coe_prodNatEquiv_apply ..

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfm' : Multipliable fun pk => f (↑pk.1 ^ (pk.2 + 1))
⊢ ∏' (n : ℕ), f n = ∏' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))

Tactic:
simp only [← tprod_subtype_eq_of_mulSupport_subset hf, Set.coe_setOf, ← prodNatEquiv.tprod_eq,
  ← tprod_prod hfm']

Result:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
hfm' : Multipliable fun pk => f (↑pk.1 ^ (pk.2 + 1))
⊢ ∏' (c : Nat.Primes × ℕ), f ↑(prodNatEquiv c) = ∏' (p : Nat.Primes × ℕ), f (↑p.1 ^ (p.2 + 1))
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_mapRange_index {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N}
    (h0 : ∀ a, h a 0 = 1) : (mapRange f hf g).prod h = g.prod fun a b => h a (f b) :=
  Finset.prod_subset support_mapRange fun _ _ H => by rw [not_mem_support_iff.1 H, h0]

Proof state:
α : Type u_1
M : Type u_8
M' : Type u_9
N : Type u_10
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x✝¹ : α
x✝ : x✝¹ ∈ g.support
H : x✝¹ ∉ (mapRange f hf g).support
⊢ h x✝¹ ((mapRange f hf g) x✝¹) = 1

Tactic:
rw [not_mem_support_iff.1 H, h0]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_singleton (a b : α) : count a #v[b] = if b == a then 1 else 0

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
⊢ count a { toArray := #[b], size_toArray := ⋯ } = if (b == a) = true then 1 else 0

Tactic:
simp [count_eq_countP]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem one_lt_rpow {x z : ℝ} (hx : 1 < x) (hz : 0 < z) : 1 < x ^ z

Proof state:
x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 ^ z < x ^ z

Tactic:
exact rpow_lt_rpow zero_le_one hx hz

Result:
no goals

Proof state:
x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z

Tactic:
rw [← one_rpow z]

Result:
x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 ^ z < x ^ z
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblX_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z)
    (hy' : P y * Q z = W'.negY Q * P z) : W'.dblX P = 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (W'.negY P - W'.negY P) -
          W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
        2 * P x * P z * (W'.negY P - W'.negY P) ^ 2) *
      (W'.negY P - W'.negY P) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblX P = 0

Tactic:
apply eq_zero_of_ne_zero_of_mul_right_eq_zero hPz

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblX P * P z = 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblX P * P z = 0

Tactic:
rw [dblX_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (W'.negY P - W'.negY P) -
          W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
        2 * P x * P z * (W'.negY P - W'.negY P) ^ 2) *
      (W'.negY P - W'.negY P) =
    0
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma one_succAbove_succ {n : ℕ} (j : Fin n) :
    (1 : Fin (n + 2)).succAbove j.succ = j.succ.succ

Proof state:
n : ℕ
j : Fin n
this : (succ 0).succAbove j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
rwa [succ_zero_eq_one, zero_succAbove] at this

Result:
no goals

Proof state:
n : ℕ
j : Fin n
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
have := succ_succAbove_succ 0 j

Result:
n : ℕ
j : Fin n
this : (succ 0).succAbove j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive] lemma antivary_inv : Antivary f⁻¹ g⁻¹ ↔ Antivary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
f : ι → α
g : ι → β
⊢ Antivary f⁻¹ g⁻¹ ↔ Antivary f g

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_is_bilimit' {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPushout b.fst b.snd (0 : X ⟶ 0) (0 : Y ⟶ 0)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.fst b.snd 0 0

Tactic:
refine IsPushout.of_left ?_ (by simp) (IsPushout.inl_snd' h)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout (b.inl ≫ b.fst) 0 0 (0 ≫ 0)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout (b.inl ≫ b.fst) 0 0 (0 ≫ 0)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ b.fst ≫ 0 = b.snd ≫ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Distributions/Exponential.lean
lemma hasDerivAt_neg_exp_mul_exp {r x : ℝ} :
    HasDerivAt (fun a ↦ -exp (-(r * a))) (r * exp (-(r * x))) x

Proof state:
r x : ℝ
⊢ HasDerivAt (fun a => -rexp (-(r * a))) (r * rexp (-(r * x))) x

Tactic:
convert (((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1)) using 1

Result:
case h.e'_8
r x : ℝ
⊢ (fun a => -rexp (-(r * a))) = fun y => -1 * rexp (-r * id y)

case h.e'_9
r x : ℝ
⊢ r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))

Proof state:
case h.e'_8
r x : ℝ
⊢ (fun a => -rexp (-(r * a))) = fun y => -1 * rexp (-r * id y)

Tactic:
simp only [one_mul, id_eq, neg_mul]

Result:
no goals

Proof state:
case h.e'_9
r x : ℝ
⊢ r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))

Tactic:
simp only [id_eq, neg_mul, mul_one, mul_neg, one_mul, neg_neg, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem minpoly_sub_algebraMap_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (x - algebraMap K L r)).Splits (algebraMap K L)

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) (minpoly K (x - (algebraMap K L) r))

Tactic:
simpa only [sub_eq_add_neg, map_neg] using minpoly_add_algebraMap_splits (-r) g

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.tdiv b = a / b

Proof state:
case neg
a b : Int
h : b ∣ a
b0 : ¬b = 0
⊢ a.tdiv b = a / b

Tactic:
rw [Int.tdiv_eq_iff_eq_mul_left b0 h, ← Int.ediv_eq_iff_eq_mul_left b0 h]

Result:
no goals

Proof state:
a b : Int
h : b ∣ a
⊢ a.tdiv b = a / b

Tactic:
by_cases b0 : b = 0

Result:
case pos
a b : Int
h : b ∣ a
b0 : b = 0
⊢ a.tdiv b = a / b

case neg
a b : Int
h : b ∣ a
b0 : ¬b = 0
⊢ a.tdiv b = a / b

Proof state:
case pos
a b : Int
h : b ∣ a
b0 : b = 0
⊢ a.tdiv b = a / b

Tactic:
simp [b0]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_erase_le (p : R[X]) (n : ℕ) : degree (p.erase n) ≤ degree p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).degree ≤ p.degree

Tactic:
rcases p with ⟨p⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (erase n { toFinsupp := p }).degree ≤ { toFinsupp := p }.degree

Proof state:
case ofFinsupp.h
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ p.support.erase n ⊆ p.support

Tactic:
apply Finset.erase_subset

Result:
no goals

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (erase n { toFinsupp := p }).degree ≤ { toFinsupp := p }.degree

Tactic:
simp only [erase_def, degree, coeff, support]

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (Finsupp.erase n p).support.max ≤ p.support.max

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (Finsupp.erase n p).support.max ≤ p.support.max

Tactic:
apply sup_mono

Result:
case ofFinsupp.h
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (Finsupp.erase n p).support ⊆ p.support

Proof state:
case ofFinsupp.h
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ (Finsupp.erase n p).support ⊆ p.support

Tactic:
rw [Finsupp.support_erase]

Result:
case ofFinsupp.h
R : Type u
inst✝ : Semiring R
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ p.support.erase n ⊆ p.support
-- Mathlib/Order/Filter/Lift.lean
theorem prod_lift'_lift' {f₁ : Filter α₁} {f₂ : Filter α₂} {g₁ : Set α₁ → Set β₁}
    {g₂ : Set α₂ → Set β₂} (hg₁ : Monotone g₁) (hg₂ : Monotone g₂) :
    f₁.lift' g₁ ×ˢ f₂.lift' g₂ = f₁.lift fun s => f₂.lift' fun t => g₁ s ×ˢ g₂ t :=
  calc
    f₁.lift' g₁ ×ˢ f₂.lift' g₂ = f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t) :=
      prod_lift_lift (monotone_principal.comp hg₁) (monotone_principal.comp hg₂)
    _ = f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s ×ˢ g₂ t)

Proof state:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Set β₁
g₂ : Set α₂ → Set β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s) ×ˢ 𝓟 (g₂ t)) = f₁.lift fun s => f₂.lift fun t => 𝓟 (g₁ s ×ˢ g₂ t)

Tactic:
simp only [prod_principal_principal]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_op {X Y : C} (h : X = Y) : (eqToHom h).op = eqToHom (congr_arg op h.symm)

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (eqToHom ⋯).op = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ (eqToHom h).op = eqToHom ⋯

Tactic:
cases h

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (eqToHom ⋯).op = eqToHom ⋯
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma of_eq {X Y : C} {f : X ⟶ Y} (hf : P f)
    {X' Y' : C} {f' : X' ⟶ Y'}
    (hX : X = X') (hY : Y = Y') (h : f' = eqToHom hX.symm ≫ f ≫ eqToHom hY) :
    P f'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ P f'

Tactic:
rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f' ∈ P.toSet

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f' ∈ P.toSet

Tactic:
rwa [(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
@[simp] lemma mem_sup' (hs) : a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
induction' hs using Nonempty.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
theorem rpow_one_add_le_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) :
    (1 + s) ^ p ≤ 1 + p * s

Proof state:
case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2 : p ≤ 1
hp1 : 0 < p
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
rcases eq_or_lt_of_le hp2 with (rfl | hp2)

Result:
case inr.inl
s : ℝ
hs : -1 ≤ s
hp1✝ : 0 ≤ 1
hp2 : 1 ≤ 1
hp1 : 0 < 1
⊢ (1 + s) ^ 1 ≤ 1 + 1 * s

case inr.inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p ≤ 1 + p * s

Proof state:
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1 : 0 ≤ p
hp2 : p ≤ 1
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
rcases eq_or_lt_of_le hp1 with (rfl | hp1)

Result:
case inl
s : ℝ
hs : -1 ≤ s
hp1 : 0 ≤ 0
hp2 : 0 ≤ 1
⊢ (1 + s) ^ 0 ≤ 1 + 0 * s

case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2 : p ≤ 1
hp1 : 0 < p
⊢ (1 + s) ^ p ≤ 1 + p * s

Proof state:
case inr.inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
by_cases hs' : s = 0

Result:
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : ¬s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

Proof state:
case inr.inl
s : ℝ
hs : -1 ≤ s
hp1✝ : 0 ≤ 1
hp2 : 1 ≤ 1
hp1 : 0 < 1
⊢ (1 + s) ^ 1 ≤ 1 + 1 * s

Tactic:
simp

Result:
no goals

Proof state:
case neg
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : ¬s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
exact (rpow_one_add_lt_one_add_mul_self hs hs' hp1 hp2).le

Result:
no goals

Proof state:
case inl
s : ℝ
hs : -1 ≤ s
hp1 : 0 ≤ 0
hp2 : 0 ≤ 1
⊢ (1 + s) ^ 0 ≤ 1 + 0 * s

Tactic:
simp

Result:
no goals

Proof state:
case pos
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
hs' : s = 0
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
simp [hs']

Result:
no goals
-- Mathlib/Algebra/DualNumber.lean
theorem algHom_ext' ⦃f g : A[ε] →ₐ[R] B⦄
    (hinl : f.comp (inlAlgHom _ _ _) = g.comp (inlAlgHom _ _ _))
    (hinr : f.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R =
        g.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R) :
      f = g :=
  algHom_ext' hinl (by
    ext a
    show f (inr a) = g (inr a)
    simpa only [inr_eq_smul_eps] using DFunLike.congr_fun hinr a)

Proof state:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
⊢ f.toLinearMap ∘ₗ ↑R (inrHom A A) = g.toLinearMap ∘ₗ ↑R (inrHom A A)

Tactic:
ext a

Result:
case h
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
a : A
⊢ (f.toLinearMap ∘ₗ ↑R (inrHom A A)) a = (g.toLinearMap ∘ₗ ↑R (inrHom A A)) a

Proof state:
case h
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
a : A
⊢ (f.toLinearMap ∘ₗ ↑R (inrHom A A)) a = (g.toLinearMap ∘ₗ ↑R (inrHom A A)) a

Tactic:
show f (inr a) = g (inr a)

Result:
case h
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
a : A
⊢ f (inr a) = g (inr a)

Proof state:
case h
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
a : A
⊢ f (inr a) = g (inr a)

Tactic:
simpa only [inr_eq_smul_eps] using DFunLike.congr_fun hinr a

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma exact_of_δlast {n : ℕ} (S : ComposableArrows C (n + 2))
    (h₁ : S.δlast.Exact) (h₂ : (mk₂ (S.map' n (n + 1)) (S.map' (n + 1) (n + 2))).Exact) :
    S.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.Exact

Tactic:
rw [exact_iff_δlast]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
constructor <;> assumption

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_self_of_one_lt (h₁ : 1 < x) (h₂ : y < 1) : x ^ y < x

Proof state:
x y : ℝ
h₁ : 1 < x
h₂ : y < 1
⊢ x ^ y < x

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_lt h₁ h₂

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_lt_eq_Ioi [DecidablePred (a < ·)] : ({x | a < x} : Finset _) = Ioi a

Proof state:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => a < x
a✝ : α
⊢ a✝ ∈ filter (fun x => a < x) univ ↔ a✝ ∈ Ioi a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => a < x
⊢ filter (fun x => a < x) univ = Ioi a

Tactic:
ext

Result:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => a < x
a✝ : α
⊢ a✝ ∈ filter (fun x => a < x) univ ↔ a✝ ∈ Ioi a
-- Mathlib/Data/Finset/Max.lean
theorem map_toDual_min (s : Finset α) : s.min.map toDual = (s.image toDual).max

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).max

Tactic:
rw [max_eq_sup_withBot, sup_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = s.sup (WithBot.some ∘ ⇑toDual)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = s.sup (WithBot.some ∘ ⇑toDual)

Tactic:
exact congr_fun Option.map_id _

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem liftRel_pure_left (R : α → β → Prop) (a : α) (cb : Computation β) :
    LiftRel R (pure a) cb ↔ ∃ b, b ∈ cb ∧ R a b :=
  ⟨fun ⟨l, _⟩ => l (ret_mem _), fun ⟨b, mb, ab⟩ =>
    ⟨fun {a'} ma' => by rw [eq_of_pure_mem ma']; exact ⟨b, mb, ab⟩, fun {b'} mb' =>
      ⟨_, ret_mem _, by rw [mem_unique mb' mb]; exact ab⟩⟩⟩

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ b, b ∈ cb ∧ R a' b

Tactic:
rw [eq_of_pure_mem ma']

Result:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ b, b ∈ cb ∧ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ b, b ∈ cb ∧ R a b

Tactic:
exact ⟨b, mb, ab⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b'

Tactic:
rw [mem_unique mb' mb]

Result:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b

Tactic:
exact ab

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem exists_not_acc_lt_of_not_acc {a : α} {r} (h : ¬Acc r a) : ∃ b, ¬Acc r b ∧ r b a

Proof state:
α : Type u_1
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
hb : ¬Acc r b
⊢ False

Tactic:
exact h b hb hr

Result:
no goals

Proof state:
α : Type u_1
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
⊢ Acc r a

Tactic:
refine ⟨_, fun b hr => ?_⟩

Result:
α : Type u_1
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
⊢ Acc r b

Proof state:
α : Type u_1
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
⊢ Acc r b

Tactic:
by_contra hb

Result:
α : Type u_1
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
hb : ¬Acc r b
⊢ False

Proof state:
α : Type u_1
a : α
r : α → α → Prop
h : ¬Acc r a
⊢ ∃ b, ¬Acc r b ∧ r b a

Tactic:
contrapose! h

Result:
α : Type u_1
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
⊢ Acc r a