harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sign.lean
theorem sign_eq_neg_one_iff : sign a = -1 ↔ a < 0

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
⊢ a < 0

Tactic:
split_ifs at h

Result:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h✝¹ : ¬0 < a
h✝ : a < 0
h : -1 = -1
⊢ a < 0

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : sign a = -1
⊢ a < 0

Tactic:
rw [sign_apply] at h

Result:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
⊢ a < 0

Proof state:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h✝¹ : ¬0 < a
h✝ : a < 0
h : -1 = -1
⊢ a < 0

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
⊢ sign a = -1 ↔ a < 0

Tactic:
refine ⟨fun h => ?_, fun h => sign_neg h⟩

Result:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
h : sign a = -1
⊢ a < 0
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticWithinAt.differentiableWithinAt (h : AnalyticWithinAt 𝕜 f s x) :
    DifferentiableWithinAt 𝕜 f (insert x s) x

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
exact hp.differentiableWithinAt

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : AnalyticWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
obtain ⟨p, hp⟩ := h

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x
-- Mathlib/Data/Seq/Computation.lean
theorem terminates_def (s : Computation α) : Terminates s ↔ ∃ n, (s.1 n).isSome :=
  ⟨fun ⟨⟨a, n, h⟩⟩ =>
    ⟨n, by
      dsimp [Stream'.get] at h
      rw [← h]
      exact rfl⟩,
    fun ⟨n, h⟩ => ⟨⟨Option.get _ h, n, (Option.eq_some_of_isSome h).symm⟩⟩⟩

Proof state:
α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = ↑s n
⊢ (some a).isSome = true

Tactic:
exact rfl

Result:
no goals

Proof state:
α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = ↑s n
⊢ (↑s n).isSome = true

Tactic:
rw [← h]

Result:
α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = ↑s n
⊢ (some a).isSome = true

Proof state:
α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : (fun b => some a = b) ((↑s).get n)
⊢ (↑s n).isSome = true

Tactic:
dsimp [Stream'.get] at h

Result:
α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = ↑s n
⊢ (↑s n).isSome = true
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi {θ ψ : Angle}
    (h : (2 : ℕ) • θ + (2 : ℕ) • ψ = π) : |cos θ| = |sin ψ|

Proof state:
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
rw [← eq_sub_iff_add_eq, ← two_nsmul_coe_div_two, ← nsmul_sub, two_nsmul_eq_iff] at h

Result:
θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ |θ.cos| = |ψ.sin|

Proof state:
θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
rcases h with (rfl | rfl) <;> simp [cos_pi_div_two_sub]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_eq_rotate' (l : List α) (n : ℕ) : l.rotate n = l.rotate' n :=
  if h : l.length = 0 then by simp_all [length_eq_zero]
  else by
    rw [← rotate'_mod,
        rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
    simp [rotate]

Proof state:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
simp [rotate]

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
rw [← rotate'_mod,
    rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]

Result:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Proof state:
α : Type u
l : List α
n : ℕ
h : l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
simp_all [length_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mem_top_objs (c : C) : c ∈ (⊤ : Subgroupoid C).objs

Proof state:
C : Type u
inst✝ : Groupoid C
c : C
⊢ univ.Nonempty

Tactic:
simp only [univ_nonempty]

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
c : C
⊢ c ∈ ⊤.objs

Tactic:
dsimp [Top.top, objs]

Result:
C : Type u
inst✝ : Groupoid C
c : C
⊢ univ.Nonempty
-- Mathlib/Data/Multiset/Lattice.lean
theorem nodup_sup_iff {α : Type*} [DecidableEq α] {m : Multiset (Multiset α)} :
    m.sup.Nodup ↔ ∀ a : Multiset α, a ∈ m → a.Nodup

Proof state:
α : Type u_2
inst✝ : DecidableEq α
m : Multiset (Multiset α)
⊢ m.sup.Nodup ↔ ∀ a ∈ m, a.Nodup

Tactic:
induction m using Multiset.induction_on with
| empty => simp
| cons _ _ h => simp [h]

Result:
no goals

Proof state:
case cons
α : Type u_2
inst✝ : DecidableEq α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
h : s✝.sup.Nodup ↔ ∀ a ∈ s✝, a.Nodup
⊢ (a✝ ::ₘ s✝).sup.Nodup ↔ ∀ a ∈ a✝ ::ₘ s✝, a.Nodup

Tactic:
simp [h]

Result:
no goals

Proof state:
case empty
α : Type u_2
inst✝ : DecidableEq α
⊢ (sup 0).Nodup ↔ ∀ a ∈ 0, a.Nodup

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mulEquivOfQuotient_mk (x y) : mulEquivOfQuotient f (mk x y) = f.mk' x y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) (mk x y) = f.mk' x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) ((monoidOf S).mk' x y) = f.mk' x y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f) ((monoidOf S).mk' x y) = f.mk' x y

Tactic:
exact mulEquivOfQuotient_mk' _ _

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tsum_geometric_inv_two_ge (n : ℕ) :
    (∑' i, ite (n ≤ i) ((2 : ℝ)⁻¹ ^ i) 0) = 2 * 2⁻¹ ^ n

Proof state:
n : ℕ
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n

Tactic:
have A : Summable fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0 := by
  simpa only [← piecewise_eq_indicator, one_div]
    using summable_geometric_two.indicator {i | n ≤ i}

Result:
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n

Proof state:
n : ℕ
⊢ Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0

Tactic:
simpa only [← piecewise_eq_indicator, one_div]
  using summable_geometric_two.indicator {i | n ≤ i}

Result:
no goals

Proof state:
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
B : (∑ i ∈ Finset.range n, if n ≤ i then 2⁻¹ ^ i else 0) = 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n

Tactic:
simp only [← _root_.sum_add_tsum_nat_add n A, B, if_true, zero_add, zero_le',
  le_add_iff_nonneg_left, pow_add, _root_.tsum_mul_right, tsum_geometric_inv_two]

Result:
no goals

Proof state:
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n

Tactic:
have B : ((Finset.range n).sum fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0) = 0 :=
  Finset.sum_eq_zero fun i hi ↦
    ite_eq_right_iff.2 fun h ↦ (lt_irrefl _ ((Finset.mem_range.1 hi).trans_le h)).elim

Result:
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
B : (∑ i ∈ Finset.range n, if n ≤ i then 2⁻¹ ^ i else 0) = 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_diff_add_mk {S T : Set α} (h : T ⊆ S) : #(S \ T : Set α) + #T = #S

Proof state:
α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T) + #↑T = #↑S

Tactic:
refine (mk_union_of_disjoint <| ?_).symm.trans <| by rw [diff_union_of_subset h]

Result:
α : Type u
S T : Set α
h : T ⊆ S
⊢ Disjoint (S \ T) T

Proof state:
α : Type u
S T : Set α
h : T ⊆ S
⊢ Disjoint (S \ T) T

Tactic:
exact disjoint_sdiff_self_left

Result:
no goals

Proof state:
α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T ∪ T) = #↑S

Tactic:
rw [diff_union_of_subset h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
lemma isIso_π_of_isLimit {c : Cone F} (hc : IsLimit c) :
    IsIso (c.π.app i₀)

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (hc.conePointUniqueUpToIso h.isLimitCone).hom

Tactic:
infer_instance

Result:
no goals

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (c.π.app i₀)

Tactic:
simp only [← IsLimit.conePointUniqueUpToIso_hom_comp hc h.isLimitCone i₀,
  cone_π_app, coneπApp_eq_id, cone_pt, comp_id]

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (hc.conePointUniqueUpToIso h.isLimitCone).hom
-- Mathlib/CategoryTheory/NatIso.lean
theorem cancel_natIso_hom_left {X : C} {Z : D} (g g' : G.obj X ⟶ Z) :
    α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
X : C
Z : D
g g' : G.obj X ⟶ Z
⊢ α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi, refl]

Result:
no goals
-- Mathlib/Data/Real/Pi/Wallis.lean
theorem W_eq_integral_sin_pow_div_integral_sin_pow (k : ℕ) : (π / 2)⁻¹ * W k =
    (∫ x : ℝ in (0)..π, sin x ^ (2 * k + 1)) / ∫ x : ℝ in (0)..π, sin x ^ (2 * k)

Proof state:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))

Tactic:
rfl

Result:
no goals

Proof state:
k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Tactic:
rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]

Result:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))

Proof state:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))

Tactic:
simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]

Result:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem modify_eq_modifyₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
    (f : β a → β a) : m.modify a f = m.modifyₘ a f

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : β a → β a
⊢ m.modify a f = m.modifyₘ a f

Tactic:
rw [modify_eq_alter, alter_eq_alterₘ, modifyₘ]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_zero (x : α 0) (p : ∀ j : Fin n, α (succAbove 0 j)) :
    insertNth 0 x p =
      cons x fun j ↦ _root_.cast (congr_arg α (congr_fun succAbove_zero j)) (p j)

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ x = cons x (fun j => cast ⋯ (p j)) 0

Tactic:
simp

Result:
no goals

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
j : Fin n
⊢ p j = removeNth 0 (cons x fun j => cast ⋯ (p j)) j

Tactic:
convert (cons_succ x p j).symm

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ p = removeNth 0 (cons x fun j => cast ⋯ (p j))

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
j : Fin n
⊢ p j = removeNth 0 (cons x fun j => cast ⋯ (p j)) j

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ insertNth 0 x p = cons x fun j => cast ⋯ (p j)

Tactic:
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩

Result:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ p = removeNth 0 (cons x fun j => cast ⋯ (p j))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
    m.contains a = false → get! m a = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ m.contains a = false → get! m a = default

Tactic:
simp_to_model using List.getValue!_eq_default

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0 (n + s)
  | 0, _ => rfl
  | s + 1, n => by rw [← Nat.add_assoc, Nat.add_right_comm n s 1]; exact range_loop_range' s (n + 1)

Proof state:
s n : Nat
⊢ range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + 1 + s)

Tactic:
exact range_loop_range' s (n + 1)

Result:
no goals

Proof state:
s n : Nat
⊢ range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + (s + 1))

Tactic:
rw [← Nat.add_assoc, Nat.add_right_comm n s 1]

Result:
s n : Nat
⊢ range.loop (s + 1) (range' (s + 1) n) = range' 0 (n + 1 + s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
    Bool.atLeastTwo lhsBit rhsBit carry
      =
    (((lhsBit ^^ rhsBit) && carry) || (lhsBit && rhsBit))

Proof state:
⊢ ∀ (lhsBit rhsBit carry : Bool), lhsBit.atLeastTwo rhsBit carry = ((lhsBit ^^ rhsBit) && carry || lhsBit && rhsBit)

Tactic:
decide

Result:
no goals

Proof state:
lhsBit rhsBit carry : Bool
⊢ lhsBit.atLeastTwo rhsBit carry = ((lhsBit ^^ rhsBit) && carry || lhsBit && rhsBit)

Tactic:
revert lhsBit rhsBit carry

Result:
⊢ ∀ (lhsBit rhsBit carry : Bool), lhsBit.atLeastTwo rhsBit carry = ((lhsBit ^^ rhsBit) && carry || lhsBit && rhsBit)
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
@[simp]
lemma awayMap_mk {d : ι} (n : ℕ) (hf : f ∈ 𝒜 d) (a : A) (ha : a ∈ 𝒜 (n • d)) :
    awayMap 𝒜 hg hx (Away.mk 𝒜 hf n a ha) = Away.mk 𝒜 (hx ▸ mul_mem_graded hf hg) n
      (a * g ^ n) (by rw [smul_add]; exact mul_mem_graded ha (pow_mem_graded n hg))

Proof state:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ val ((awayMap 𝒜 hg hx) (Away.mk 𝒜 hf n a ha)) = val (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯)

Tactic:
exact val_awayMap_mk ..

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x✝ : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • d + n • e)

Tactic:
exact mul_mem_graded ha (pow_mem_graded n hg)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ (awayMap 𝒜 hg hx) (Away.mk 𝒜 hf n a ha) = Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯

Tactic:
ext

Result:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ val ((awayMap 𝒜 hg hx) (Away.mk 𝒜 hf n a ha)) = val (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x✝ : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • (d + e))

Tactic:
rw [smul_add]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x✝ : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • d + n • e)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_hom_app_right : (spanExt iX iY iZ wf wg).hom.app WalkingSpan.right = iZ.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).hom.app WalkingSpan.right = iZ.hom

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem totallyBounded_iff_ultrafilter {s : Set α} :
    TotallyBounded s ↔ ∀ f : Ultrafilter α, ↑f ≤ 𝓟 s → Cauchy (f : Filter α)

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f
⊢ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c

Tactic:
intro f hf hfs

Result:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f
f : Filter α
hf : f.NeBot
hfs : f ≤ 𝓟 s
⊢ ∃ c ≤ f, Cauchy c

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f
f : Filter α
hf : f.NeBot
hfs : f ≤ 𝓟 s
⊢ ∃ c ≤ f, Cauchy c

Tactic:
exact ⟨Ultrafilter.of f, Ultrafilter.of_le f, H _ ((Ultrafilter.of_le f).trans hfs)⟩

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f

Tactic:
refine ⟨fun hs f => f.cauchy_of_totallyBounded hs, fun H => totallyBounded_iff_filter.2 ?_⟩

Result:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f
⊢ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
-- Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean
theorem antipode_C (a : A) :
    HopfAlgebra.antipode (R := R) (C a) = C (HopfAlgebra.antipode (R := R) a)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ AddMonoidAlgebra.single (-0) (antipode a) = C (antipode a)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ antipode (C a) = C (antipode a)

Tactic:
rw [← single_eq_C, AddMonoidAlgebra.antipode_single]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ AddMonoidAlgebra.single (-0) (antipode a) = C (antipode a)
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_iff_isCompact_univ : IsCompact s ↔ IsCompact (univ : Set s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact univ

Tactic:
rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tanh_neg : tanh (-x) = -tanh x

Proof state:
x : ℂ
⊢ tanh (-x) = -tanh x

Tactic:
simp [tanh, neg_div]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma le_log_of_rpow_le (hx : 0 < x) (h : x ^ z ≤ y) : z * log x ≤ log y :=
  log_rpow hx _ ▸ log_le_log (by positivity) h

Proof state:
x y z : ℝ
hx : 0 < x
h : x ^ z ≤ y
⊢ 0 < x ^ z

Tactic:
positivity

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem pow_right (a : ℤ) (b e : ℕ) : J(a | b ^ e) = J(a | b) ^ e

Proof state:
case succ
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
rcases eq_zero_or_neZero b with hb | _

Result:
case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Proof state:
case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]

Result:
no goals

Proof state:
case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]

Result:
no goals

Proof state:
case zero
a : ℤ
b : ℕ
⊢ J(a | b ^ 0) = J(a | b) ^ 0

Tactic:
rw [Nat.pow_zero, _root_.pow_zero, one_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n} :
    xs.allM p = (! ·) <$> xs.anyM ((! ·) <$> p ·)

Proof state:
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
xs : Vector α n
⊢ allM p xs = (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) xs

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
xs : Array α
⊢ allM p { toArray := xs, size_toArray := ⋯ } =
    (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) { toArray := xs, size_toArray := ⋯ }

Proof state:
case mk
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
xs : Array α
⊢ allM p { toArray := xs, size_toArray := ⋯ } =
    (fun x => !x) <$> anyM (fun x => (fun x => !x) <$> p x) { toArray := xs, size_toArray := ⋯ }

Tactic:
simp [Array.allM_eq_not_anyM_not]

Result:
no goals