harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem Rel.trans (r : α → α → Prop) [IsTrans α r] {s t u : Multiset α} (r1 : Rel r s t)
    (r2 : Rel r t u) : Rel r s u

Proof state:
case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r s u

Tactic:
rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
⊢ Rel r s u

Tactic:
induction' t using Multiset.induction_on with x t ih generalizing s u

Result:
case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r s u

case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u

Proof state:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u

Tactic:
obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1

Result:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u

Proof state:
case cons.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u

Tactic:
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2

Result:
case cons.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
b : α
bs : Multiset α
hb1 : r x b
hb2 : Rel r t bs
r2 : Rel r (x ::ₘ t) (b ::ₘ bs)
⊢ Rel r (a ::ₘ as) (b ::ₘ bs)

Proof state:
case cons.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
b : α
bs : Multiset α
hb1 : r x b
hb2 : Rel r t bs
r2 : Rel r (x ::ₘ t) (b ::ₘ bs)
⊢ Rel r (a ::ₘ as) (b ::ₘ bs)

Tactic:
exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem nonpos_of_neg_nonneg {a : Int} (h : 0 ≤ -a) : a ≤ 0 :=
  Int.le_of_neg_le_neg <| by rwa [Int.neg_zero]

Proof state:
a : Int
h : 0 ≤ -a
⊢ -0 ≤ -a

Tactic:
rwa [Int.neg_zero]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
/-- This inequality is particularly useful when `c = 1` and `‖a‖ = ‖b‖ = 1` as it then shows that
chord length is a metric on the unit complex numbers. -/
lemma norm_sub_mul_le (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ :=
  calc
    _ ≤ ‖c - a‖ + ‖a * (1 - b)‖

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + ‖a‖ * ‖1 - b‖ ≤ ‖c - a‖ + 1 * ‖1 - b‖

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + ‖a * (1 - b)‖ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖

Tactic:
gcongr

Result:
case bc
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - a‖ + ‖a * (1 - b)‖

Tactic:
simpa [mul_one_sub] using norm_sub_le_norm_sub_add_norm_sub c a (a * b)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + 1 * ‖1 - b‖ = ‖c - a‖ + ‖1 - b‖

Tactic:
simp

Result:
no goals

Proof state:
case bc
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖

Tactic:
exact norm_mul_le ..

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_antiperiodic : Function.Antiperiodic sin (π : Angle)

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).sin = -(↑x✝).sin

Tactic:
exact Real.sin_antiperiodic _

Result:
no goals

Proof state:
⊢ Function.Antiperiodic sin ↑π

Tactic:
intro θ

Result:
θ : Angle
⊢ (θ + ↑π).sin = -θ.sin

Proof state:
θ : Angle
⊢ (θ + ↑π).sin = -θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).sin = -(↑x✝).sin
-- Mathlib/Algebra/BigOperators/Pi.lean
theorem Finset.univ_prod_mulSingle [Fintype I] (f : ∀ i, Z i) :
    (∏ i, Pi.mulSingle i (f i)) = f

Proof state:
I : Type u_4
inst✝² : DecidableEq I
Z : I → Type u_5
inst✝¹ : (i : I) → CommMonoid (Z i)
inst✝ : Fintype I
f : (i : I) → Z i
⊢ ∏ i : I, Pi.mulSingle i (f i) = f

Tactic:
ext a

Result:
case h
I : Type u_4
inst✝² : DecidableEq I
Z : I → Type u_5
inst✝¹ : (i : I) → CommMonoid (Z i)
inst✝ : Fintype I
f : (i : I) → Z i
a : I
⊢ (∏ i : I, Pi.mulSingle i (f i)) a = f a

Proof state:
case h
I : Type u_4
inst✝² : DecidableEq I
Z : I → Type u_5
inst✝¹ : (i : I) → CommMonoid (Z i)
inst✝ : Fintype I
f : (i : I) → Z i
a : I
⊢ (∏ i : I, Pi.mulSingle i (f i)) a = f a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_pow : ∀ {a : ℝ≥0∞} {n : ℕ}, (a ^ n)⁻¹ = a⁻¹ ^ n
  | _, 0 => by simp only [pow_zero, inv_one]
  | ⊤, n + 1 => by simp [top_pow]
  | (a : ℝ≥0), n + 1 => by
    rcases eq_or_ne a 0 with (rfl | ha)
    · simp [top_pow]
    · have := pow_ne_zero (n + 1) ha
      norm_cast
      rw [inv_pow]

Proof state:
case inl
n : ℕ
⊢ (↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)

Tactic:
simp [top_pow]

Result:
no goals

Proof state:
case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)

Tactic:
have := pow_ne_zero (n + 1) ha

Result:
case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)

Proof state:
a : ℝ≥0
n : ℕ
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
n : ℕ
⊢ (↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)

case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)

Proof state:
x✝ : ℝ≥0∞
⊢ (x✝ ^ 0)⁻¹ = x✝⁻¹ ^ 0

Tactic:
simp only [pow_zero, inv_one]

Result:
no goals

Proof state:
case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)

Tactic:
rw [inv_pow]

Result:
no goals

Proof state:
n : ℕ
⊢ (⊤ ^ (n + 1))⁻¹ = ⊤⁻¹ ^ (n + 1)

Tactic:
simp [top_pow]

Result:
no goals

Proof state:
case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)

Tactic:
norm_cast

Result:
case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem of_P : ∀ q n : ℕ, HigherFacesVanish q ((P q).f (n + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌)
  | 0 => fun n j hj₁ => by omega
  | q + 1 => fun n => by
    simp only [P_succ]
    exact (of_P q n).induction

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) ((P q ≫ (𝟙 K[X] + Hσ q)).f (n + 1))

Tactic:
exact (of_P q n).induction

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + 0
⊢ (P 0).f (n + 1) ≫ X.δ j.succ = 0

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) ((P (q + 1)).f (n + 1))

Tactic:
simp only [P_succ]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) ((P q ≫ (𝟙 K[X] + Hσ q)).f (n + 1))
-- Mathlib/Data/Finmap.lean
theorem liftOn₂_toFinmap {γ} (s₁ s₂ : AList β) (f : AList β → AList β → γ) (H) :
    liftOn₂ ⟦s₁⟧ ⟦s₂⟧ f H = f s₁ s₂

Proof state:
case mk
α : Type u
β : α → Type v
γ : Type u_1
s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧.liftOn₂ ⟦s₂⟧ f H =
    f { entries := entries✝, nodupKeys := nodupKeys✝ } s₂

Tactic:
cases s₂

Result:
case mk.mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : entries✝¹.NodupKeys
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧.liftOn₂ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H =
    f { entries := entries✝¹, nodupKeys := nodupKeys✝¹ } { entries := entries✝, nodupKeys := nodupKeys✝ }

Proof state:
case mk.mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : entries✝¹.NodupKeys
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧.liftOn₂ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H =
    f { entries := entries✝¹, nodupKeys := nodupKeys✝¹ } { entries := entries✝, nodupKeys := nodupKeys✝ }

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type u_1
s₁ s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
⊢ ⟦s₁⟧.liftOn₂ ⟦s₂⟧ f H = f s₁ s₂

Tactic:
cases s₁

Result:
case mk
α : Type u
β : α → Type v
γ : Type u_1
s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧.liftOn₂ ⟦s₂⟧ f H =
    f { entries := entries✝, nodupKeys := nodupKeys✝ } s₂
-- Mathlib/MeasureTheory/Measure/AddContent.lean
/-- For an `m : addContent C` on a `SetSemiring C`, if `I` is a `Finset` of pairwise disjoint
  sets in `C` and `⋃₀ I ⊆ t` for `t ∈ C`, then `∑ s ∈ I, m s ≤ m t`. -/
lemma sum_addContent_le_of_subset (hC : IsSetSemiring C)
    (h_ss : ↑I ⊆ C) (h_dis : PairwiseDisjoint (I : Set (Set α)) id)
    (ht : t ∈ C) (hJt : ∀ s ∈ I, s ⊆ t) :
    ∑ u ∈ I, m u ≤ m t

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
⊢ ∑ u ∈ I, m u ≤ ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion ht h_ss, m i

Tactic:
exact le_add_right le_rfl

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
⊢ ∑ u ∈ I, m u ≤ m t

Tactic:
classical
rw [addContent_eq_add_disjointOfDiffUnion_of_subset hC ht h_ss hJt h_dis]
exact le_add_right le_rfl

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
⊢ ∑ u ∈ I, m u ≤ m t

Tactic:
rw [addContent_eq_add_disjointOfDiffUnion_of_subset hC ht h_ss hJt h_dis]

Result:
α : Type u_1
C : Set (Set α)
t : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
ht : t ∈ C
hJt : ∀ s ∈ I, s ⊆ t
⊢ ∑ u ∈ I, m u ≤ ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion ht h_ss, m i
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_mul_Gamma_add_half (s : ℂ) :
    Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * (2 : ℂ) ^ (1 - 2 * s) * ↑(√π)

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (Gamma ↑t)⁻¹ * (Gamma (↑t + 1 / 2))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑√π

Tactic:
rw [← mul_inv, Gamma_ofReal, (by norm_num : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
  ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
  mul_inv, mul_inv, (by norm_num : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
  ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
  ofReal_one, neg_sub, ← div_eq_mul_inv]

Result:
no goals

Proof state:
case ha
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun y => (Gamma (2 * y))⁻¹

Tactic:
exact differentiable_one_div_Gamma.comp (differentiable_id'.const_mul _)

Result:
no goals

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ ↑t + 1 / 2 = ↑(t + 1 / 2)

Tactic:
norm_num

Result:
no goals

Proof state:
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π

Tactic:
convert congr_arg Inv.inv (congr_fun this s) using 1

Result:
case h.e'_2
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹

case h.e'_3
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = ((Gamma (2 * s))⁻¹ * 2 ^ (2 * s - 1) / ↑√π)⁻¹

Proof state:
case hb
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun y => 2 ^ (2 * y - 1)

Tactic:
refine fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)

Result:
case hb
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
t : ℂ
⊢ DifferentiableAt ℂ (fun y => 2 * y - 1) t

Proof state:
s : ℂ
⊢ DifferentiableOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Tactic:
refine (differentiable_one_div_Gamma.mul ?_).differentiableOn

Result:
s : ℂ
⊢ Differentiable ℂ fun z => (Gamma (z + 1 / 2))⁻¹

Proof state:
s : ℂ
⊢ Differentiable ℂ fun z => (Gamma (z + 1 / 2))⁻¹

Tactic:
exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableAt_iff_source_of_mem_source
    [IsManifold I 1 M] {x' : M} (hx' : x' ∈ (chartAt H x).source) :
    MDifferentiableAt I I' f x' ↔
      MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (extChartAt I x).symm) (range I)
        (extChartAt I x x')

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
x : M
inst✝ : IsManifold I 1 M
x' : M
hx' : x' ∈ (chartAt H x).source
⊢ MDifferentiableAt I I' f x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')

Tactic:
simp_rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_source_of_mem_source hx',
  preimage_univ, univ_inter]

Result:
no goals
-- Mathlib/Data/Nat/Cast/NeZero.lean
theorem one_le {n : ℕ} [NeZero n] : 1 ≤ n

Proof state:
n : ℕ
inst✝ : NeZero n
this : n ≠ 0
⊢ 1 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ 1 ≤ n

Tactic:
have := NeZero.ne n

Result:
n : ℕ
inst✝ : NeZero n
this : n ≠ 0
⊢ 1 ≤ n
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_single_neg {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : ¬p i) :
    (single i x).filter p = 0

Proof state:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ filter p (single i x) = 0

Tactic:
rw [filter_single, if_neg h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[simp]
lemma Spec.map_inv {R S : CommRingCat} (f : R ⟶ S) [IsIso f] :
    Spec.map (inv f) = inv (Spec.map f)

Proof state:
R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ map (inv f) = inv (map f)

Tactic:
show Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)

Result:
R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)

Proof state:
R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)

Tactic:
rw [op_inv, ← Scheme.Spec.map_inv]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂)
    (a : α) :
    (Option.map f₁ a).map g₁ = (Option.map f₂ a).map g₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))

Tactic:
rw [map_map, h, ← map_map]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph X Y) :
    (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈
      (f.symm.trans f').restr (f.target ∩ f.symm ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ f.symm.trans ((s.partialHomeomorphSubtypeCoe hs).symm.trans (s.partialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s) openness₂)

Tactic:
refine EqOnSource.trans' (eqOnSource_refl _) ?_

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ (s.partialHomeomorphSubtypeCoe hs).symm.trans (s.partialHomeomorphSubtypeCoe hs) ≈ ofSet (↑s) openness₂
-- Mathlib/LinearAlgebra/Dual.lean
theorem LinearMap.dualMap_id : (LinearMap.id : M₁ →ₗ[R] M₁).dualMap = LinearMap.id

Proof state:
case h.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ (id.dualMap x✝¹) x✝ = (id x✝¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
⊢ id.dualMap = id

Tactic:
ext

Result:
case h.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ (id.dualMap x✝¹) x✝ = (id x✝¹) x✝
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem mem_fixedPoints_iff_apply_mem_of_mem_centralizer {g p : Perm α}
    (hp : p ∈ Subgroup.centralizer {g}) {x : α} :
    x ∈ Function.fixedPoints g ↔ p x ∈ Function.fixedPoints g :=  by
  simp only [Subgroup.mem_centralizer_singleton_iff] at hp
  simp only [Function.mem_fixedPoints_iff]
  rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]

Proof state:
α : Type u
g p : Perm α
hp : p ∈ Subgroup.centralizer {g}
x : α
⊢ x ∈ fixedPoints ⇑g ↔ p x ∈ fixedPoints ⇑g

Tactic:
simp only [Subgroup.mem_centralizer_singleton_iff] at hp

Result:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ x ∈ fixedPoints ⇑g ↔ p x ∈ fixedPoints ⇑g

Proof state:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ x ∈ fixedPoints ⇑g ↔ p x ∈ fixedPoints ⇑g

Tactic:
simp only [Function.mem_fixedPoints_iff]

Result:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ g x = x ↔ g (p x) = p x

Proof state:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ g x = x ↔ g (p x) = p x

Tactic:
rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Pullback.lean
lemma pullbackShiftFunctorZero'_hom_app :
    (shiftFunctorZero _ A).hom.app X = (pullbackShiftIso C φ 0 (φ 0) rfl).hom.app X ≫
      (shiftFunctorZero' C (φ 0) (by rw [map_zero])).hom.app X

Proof state:
C : Type u_1
inst✝³ : Category.{?u.18735, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ φ 0 = 0

Tactic:
rw [map_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero (PullbackShift C φ) A).hom.app X =
    (pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app X ≫ (shiftFunctorZero' C (φ 0) ⋯).hom.app X

Tactic:
rw [← cancel_epi ((shiftFunctorZero _ A).inv.app X), Iso.inv_hom_id_app,
  pullbackShiftFunctorZero'_inv_app, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_inter [Fintype (s ∩ t : Set _)] : (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

Proof state:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
a✝ : α
⊢ a✝ ∈ (s ∩ t).toFinset ↔ a✝ ∈ s.toFinset ∩ t.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
⊢ (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
a✝ : α
⊢ a✝ ∈ (s ∩ t).toFinset ↔ a✝ ∈ s.toFinset ∩ t.toFinset
-- Mathlib/Data/List/Basic.lean
theorem reverse_concat' (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse

Proof state:
α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
l : List α
a : α
⊢ (l ++ [a]).reverse = a :: l.reverse

Tactic:
rw [reverse_append]

Result:
α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_cons_of_false [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} (h : (k == a) = false) : getValueCast? a (⟨k, v⟩ :: l) = getValueCast? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = false
⊢ getValueCast? a (⟨k, v⟩ :: l) = getValueCast? a l

Tactic:
simp [getValueCast?, h]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_inter (t s₁ s₂ s : Set α) : t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

Proof state:
α : Type u
t s₁ s₂ s : Set α
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

Tactic:
rw [ite_inter_inter, ite_same]

Result:
no goals