harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem isLeast_opNNNorm : IsLeast {C : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsLeast {C | ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊

Tactic:
simpa only [← opNNNorm_le_iff] using isLeast_Ici

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_zero_iff_subsingleton' :
    Monic (0 : R[X]) ↔ (∀ f g : R[X], f = g) ∧ ∀ a b : R, a = b :=
  Polynomial.monic_zero_iff_subsingleton.trans
    ⟨by
      intro
      simp [eq_iff_true_of_subsingleton], fun h => subsingleton_iff.mpr h.2⟩

Proof state:
R : Type u
inst✝ : Semiring R
a✝ : Subsingleton R
⊢ (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b

Tactic:
intro

Result:
R : Type u
inst✝ : Semiring R
a✝ : Subsingleton R
⊢ (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
-- Mathlib/Order/PartialSups.lean
lemma partialSups_eq_biUnion_range (s : ℕ → Set α) (n : ℕ) :
    partialSups s n = ⋃ i ∈ Finset.range (n + 1), s i

Proof state:
α : Type u_1
s : ℕ → Set α
n : ℕ
⊢ (partialSups s) n = ⋃ i ∈ range (n + 1), s i

Tactic:
ext

Result:
case h
α : Type u_1
s : ℕ → Set α
n : ℕ
x✝ : α
⊢ x✝ ∈ (partialSups s) n ↔ x✝ ∈ ⋃ i ∈ range (n + 1), s i

Proof state:
case h
α : Type u_1
s : ℕ → Set α
n : ℕ
x✝ : α
⊢ x✝ ∈ (partialSups s) n ↔ x✝ ∈ ⋃ i ∈ range (n + 1), s i

Tactic:
simp [partialSups_eq_biSup, Nat.lt_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
    (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂)

Proof state:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ &&& x₂ ++ y₂).getLsbD i = if i < v then (y₁ &&& y₂).getLsbD i else (x₁ &&& x₂).getLsbD (i - v)

Tactic:
split <;> simp [getLsbD_append, *]

Result:
no goals

Proof state:
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
⊢ x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)

Tactic:
ext i

Result:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ &&& x₂ ++ y₂).getLsbD i = ((x₁ &&& x₂) ++ (y₁ &&& y₂)).getLsbD i

Proof state:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ &&& x₂ ++ y₂).getLsbD i = ((x₁ &&& x₂) ++ (y₁ &&& y₂)).getLsbD i

Tactic:
simp only [getLsbD_append, cond_eq_if]

Result:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ &&& x₂ ++ y₂).getLsbD i = if i < v then (y₁ &&& y₂).getLsbD i else (x₁ &&& x₂).getLsbD (i - v)
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem zero_divInt (n) : 0 /. n = 0

Proof state:
n : Int
⊢ 0 /. n = 0

Tactic:
cases n <;> simp [divInt]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma posPart_zero : (0 : A)⁺ = 0

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
⊢ 0⁺ = 0

Tactic:
simp [posPart_def]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem algebraicIndependent_of_finite' (s : Set A)
    (hinj : Injective (algebraMap R A))
    (H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R ((↑) : t → A) →
      ∀ a ∈ s, a ∉ t → Transcendental (adjoin R t) a) :
    AlgebraicIndependent R ((↑) : s → A) :=
  algebraicIndependent_of_finite_type' hinj fun t hfin h i hi ↦ H _
    (by rintro _ ⟨x, _, rfl⟩; exact x.2) (hfin.image _) h.image _ i.2
    (mt Subtype.val_injective.mem_set_image.mp hi)

Proof state:
case intro.intro
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
hinj : Injective ⇑(algebraMap R A)
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val → ∀ a ∈ s, a ∉ t → Transcendental (↥(adjoin R t)) a
t : Set { x // x ∈ s }
hfin : t.Finite
h : AlgebraicIndependent R fun i => ↑↑i
i : { x // x ∈ s }
hi : i ∉ t
x : { x // x ∈ s }
left✝ : x ∈ t
⊢ ↑x ∈ s

Tactic:
exact x.2

Result:
no goals

Proof state:
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
hinj : Injective ⇑(algebraMap R A)
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val → ∀ a ∈ s, a ∉ t → Transcendental (↥(adjoin R t)) a
t : Set { x // x ∈ s }
hfin : t.Finite
h : AlgebraicIndependent R fun i => ↑↑i
i : { x // x ∈ s }
hi : i ∉ t
⊢ Subtype.val '' t ⊆ s

Tactic:
rintro _ ⟨x, _, rfl⟩

Result:
case intro.intro
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
hinj : Injective ⇑(algebraMap R A)
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val → ∀ a ∈ s, a ∉ t → Transcendental (↥(adjoin R t)) a
t : Set { x // x ∈ s }
hfin : t.Finite
h : AlgebraicIndependent R fun i => ↑↑i
i : { x // x ∈ s }
hi : i ∉ t
x : { x // x ∈ s }
left✝ : x ∈ t
⊢ ↑x ∈ s
-- Mathlib/Data/Fin/Basic.lean
lemma lt_succAbove_iff_lt_castSucc (p : Fin (n + 1)) (i : Fin n) :
    p < p.succAbove i ↔ p < succ i

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p < i.succ

Tactic:
rw [lt_succAbove_iff_le_castSucc, le_castSucc_iff]

Result:
no goals
-- Mathlib/Logic/ExistsUnique.lean
theorem ExistsUnique.unique₂ {p : α → Sort*} [∀ x, Subsingleton (p x)]
    {q : ∀ (x : α) (_ : p x), Prop} (h : ∃! x, ∃! hx : p x, q x hx) {y₁ y₂ : α}
    (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) : y₁ = y₂

Proof state:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x, ∃ hx, q x hx
⊢ y₁ = y₂

Tactic:
exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩

Result:
no goals

Proof state:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
h : ∃! x, ∃! hx, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂

Tactic:
simp only [existsUnique_iff_exists] at h

Result:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x, ∃ hx, q x hx
⊢ y₁ = y₂
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem Option.get_congr {o o' : Option α} {ho : o.isSome} (h : o = o') :
    o.get ho = o'.get (h ▸ ho)

Proof state:
α : Type u
o o' : Option α
ho : o.isSome = true
h : o = o'
⊢ o.get ho = o'.get ⋯

Tactic:
cases h

Result:
case refl
α : Type u
o : Option α
ho : o.isSome = true
⊢ o.get ho = o.get ⋯

Proof state:
case refl
α : Type u
o : Option α
ho : o.isSome = true
⊢ o.get ho = o.get ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_strictMono [Nontrivial R] (b : Basis (Fin n) R M) : StrictMono b.flag :=
  Fin.strictMono_iff_lt_succ.2 fun _ ↦ by simp [flag_succ]

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
n : ℕ
inst✝ : Nontrivial R
b : Basis (Fin n) R M
x✝ : Fin n
⊢ b.flag x✝.castSucc < b.flag x✝.succ

Tactic:
simp [flag_succ]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive (attr := simp)]
lemma smul_inv_smul (g : G) (a : α) : g • g⁻¹ • a = a

Proof state:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ g • g⁻¹ • a = a

Tactic:
rw [smul_smul, mul_inv_cancel, one_smul]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem geom_le {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ k < n, c * u k ≤ u (k + 1)) :
    c ^ n * u 0 ≤ u n

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ n * u 0 ≤ u n

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h <;>
  simp [_root_.pow_succ', mul_assoc, le_refl]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.add_zsmul_eq [AddGroup α] [AddGroup β] (h : Antiperiodic f c) (n : ℤ) :
    f (x + n • c) = (n.negOnePow : ℤ) • f x

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k) • c) = ↑(2 * k).negOnePow • f x

Tactic:
rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℤ
⊢ f (x + n • c) = ↑n.negOnePow • f x

Tactic:
rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩

Result:
case intro.inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k) • c) = ↑(2 * k).negOnePow • f x

case intro.inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k + 1) • c) = ↑(2 * k + 1).negOnePow • f x

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k + 1) • c) = ↑(2 * k + 1).negOnePow • f x

Tactic:
rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
  Units.val_one, neg_zsmul, one_zsmul]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_eq_iff_eq_add_of_le (hb : AddLECancellable b) (h : b ≤ a) :
    a - b = c ↔ a = c + b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b = c ↔ a = c + b

Tactic:
rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_comm]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem sr_mul_self (i : ZMod n) : sr i * sr i = 1

Proof state:
n : ℕ
i : ZMod n
⊢ sr i * sr i = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_foldr {f : α → List β} {g : α → σ} {h : α → β × σ → σ} (hf : Primrec f)
    (hg : Primrec g) (hh : Primrec₂ h) :
    Primrec fun a => (f a).foldr (fun b s => h a (b, s)) (g a) :=
  (list_foldl (list_reverse.comp hf) hg <| to₂ <| hh.comp fst <| (pair snd fst).comp snd).of_eq
    fun a => by simp [List.foldl_reverse]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ List.foldl (fun s b => h (a, s, b).1 ((a, s, b).2.2, (a, s, b).2.1)) (g a) (f a).reverse =
    List.foldr (fun b s => h a (b, s)) (g a) (f a)

Tactic:
simp [List.foldl_reverse]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem mem_perpBisector_iff_dist_eq : c ∈ perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
  vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
  neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma two_le_iff_one_lt {c : Cardinal} : 2 ≤ c ↔ 1 < c

Proof state:
case h.e'_1.h.e'_3
c : Cardinal.{u_1}
⊢ 2 = ↑1 + 1

Tactic:
norm_cast

Result:
no goals

Proof state:
c : Cardinal.{u_1}
⊢ 2 ≤ c ↔ 1 < c

Tactic:
convert natCast_add_one_le_iff

Result:
case h.e'_1.h.e'_3
c : Cardinal.{u_1}
⊢ 2 = ↑1 + 1
-- Mathlib/Order/UpperLower/Basic.lean
theorem codisjoint_prod :
    Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂

Tactic:
simp_rw [codisjoint_iff, prod_sup_prod, prod_eq_top]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- Two measures at vanishing Lévy-Prokhorov distance from each other assign the same values to all
closed sets. -/
lemma measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed {μ ν : Measure Ω}
    (hLP : levyProkhorovEDist μ ν = 0) {s : Set Ω} (s_closed : IsClosed s)
    (hμs : ∃ δ > 0, μ (thickening δ s) ≠ ∞) (hνs : ∃ δ > 0, ν (thickening δ s) ≠ ∞) :
    μ s = ν s

Proof state:
case a
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ⊤
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ ν s ≤ μ s

Tactic:
exact measure_le_measure_closure_of_levyProkhorovEDist_eq_zero
  (levyProkhorovEDist_comm μ ν ▸ hLP) s_closed.measurableSet hμs |>.trans <|
  le_of_eq (congr_arg _ s_closed.closure_eq)

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ⊤
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ μ s = ν s

Tactic:
apply le_antisymm

Result:
case a
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ⊤
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ μ s ≤ ν s

case a
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ⊤
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ ν s ≤ μ s

Proof state:
case a
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ⊤
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ μ s ≤ ν s

Tactic:
exact measure_le_measure_closure_of_levyProkhorovEDist_eq_zero
  hLP s_closed.measurableSet hνs |>.trans <|
  le_of_eq (congr_arg _ s_closed.closure_eq)

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 :=
  Eq.trans (by rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm])
    (cosh_sq_sub_sinh_sq (x * I))

Proof state:
x : ℂ
⊢ sin x ^ 2 + cos x ^ 2 = cosh (x * I) ^ 2 - sinh (x * I) ^ 2

Tactic:
rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_filter {l : List α} {p q : α → Bool} :
    (filter p l).all q = l.all fun a => p a → q a

Proof state:
case nil
α : Type u_1
p q : α → Bool
⊢ (filter p []).all q = [].all fun a => decide (p a = true → q a = true)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
h : α
t : List α
ih : (filter p t).all q = t.all fun a => decide (p a = true → q a = true)
⊢ (if p h = true then h :: filter p t else filter p t).all q = (h :: t).all fun a => decide (p a = true → q a = true)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
p q : α → Bool
⊢ (filter p l).all q = l.all fun a => decide (p a = true → q a = true)

Tactic:
induction l with
| nil => rfl
| cons h t ih =>
  simp only [filter_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
h : α
t : List α
ih : (filter p t).all q = t.all fun a => decide (p a = true → q a = true)
⊢ (filter p (h :: t)).all q = (h :: t).all fun a => decide (p a = true → q a = true)

Tactic:
simp only [filter_cons]

Result:
case cons
α : Type u_1
p q : α → Bool
h : α
t : List α
ih : (filter p t).all q = t.all fun a => decide (p a = true → q a = true)
⊢ (if p h = true then h :: filter p t else filter p t).all q = (h :: t).all fun a => decide (p a = true → q a = true)
-- Mathlib/Tactic/Ring/Basic.lean
theorem toProd_pf (p : (a : R) = a') :
    a = a' ^ (nat_lit 1).rawCast * (nat_lit 1).rawCast

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a a' : R
p : a = a'
⊢ a = a' ^ Nat.rawCast 1 * Nat.rawCast 1

Tactic:
simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem not_mem_range_self {n : Nat} : n ∉ range n

Proof state:
n : Nat
⊢ ¬n ∈ range n

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@[simp] lemma card_triangles [NoAccidental t] : #((graph t).cliqueFinset 3) = #t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ #((graph t).cliqueFinset 3) = #t

Tactic:
rw [cliqueFinset_eq_map, card_map]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_smul_rotation_pi_div_two_left (x : V) (r : ℝ) :
    ⟪r • o.rotation (π / 2 : ℝ) x, x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ inner (r • (o.rotation ↑(π / 2)) x) x = 0

Tactic:
rw [inner_smul_left, inner_rotation_pi_div_two_left, mul_zero]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.prime_of_isPrime {P : Ideal A} (hP : P ≠ ⊥) (h : IsPrime P) : Prime P

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
⊢ Prime P

Tactic:
refine ⟨hP, mt Ideal.isUnit_iff.mp h.ne_top, fun I J hIJ => ?_⟩

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
I J : Ideal A
hIJ : P ∣ I * J
⊢ P ∣ I ∨ P ∣ J

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
h : P.IsPrime
I J : Ideal A
hIJ : P ∣ I * J
⊢ P ∣ I ∨ P ∣ J

Tactic:
simpa only [Ideal.dvd_iff_le] using h.mul_le.mp (Ideal.le_of_dvd hIJ)

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem lift_index_left_left {f : PadicSeq p} (hf : ¬f ≈ 0) (v2 v3 : ℕ) :
    padicNorm p (f (stationaryPoint hf)) =
    padicNorm p (f (max (stationaryPoint hf) (max v2 v3)))

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (stationaryPoint hf ⊔ (v2 ⊔ v3)))

Tactic:
apply stationaryPoint_spec hf

Result:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf ⊔ (v2 ⊔ v3)

case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf ⊔ (v2 ⊔ v3)

Tactic:
apply le_max_left

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_X_pow_char_sub_C {y : R} :
    (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Tactic:
have H := roots_X_pow_char_pow_sub_C (p := p) (n := 1) (y := y)

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p ^ 1 - C y).roots = p ^ 1 • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p ^ 1 - C y).roots = p ^ 1 • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Tactic:
rwa [pow_one, iterateFrobeniusEquiv_one] at H

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_zero_left (y : M) : polar Q 0 y = 0

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
y : M
⊢ polar (⇑Q) 0 y = 0

Tactic:
simp only [polar, zero_add, QuadraticMap.map_zero, sub_zero, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_erase_self [LawfulBEq α] (h : m.1.WF) {k : α} [Inhabited (β k)] :
    (m.erase k).get! k = default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
k : α
inst✝ : Inhabited (β k)
⊢ (m.erase k).get! k = default

Tactic:
simp_to_model [erase] using List.getValueCast!_eraseKey_self

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
@[simp]
lemma piecewise_eq_of_mem {i : ι} (hi : i ∈ s) : s.piecewise f g i = f i

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
hi : i ∈ s
⊢ s.piecewise f g i = f i

Tactic:
simp [piecewise, hi]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
lemma Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact
    {K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) :
    ∃ x ∈ K, AccPt x (cofinite ⊓ 𝓟 s) :=
  (@hK _ hs.cofinite_inf_principal_neBot (inf_le_right.trans <| principal_mono.2 hsub)).imp
    fun x hx ↦ by rwa [acc_iff_cluster, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
rwa [acc_iff_cluster, inf_comm, inf_right_comm,
(finite_singleton _).cofinite_inf_principal_compl]

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem card_powersetCard (n : ℕ) (s : Multiset α) :
    card (powersetCard n s) = Nat.choose (card s) n :=
  Quotient.inductionOn s <| by simp [powersetCard_coe]

Proof state:
α : Type u_1
n : ℕ
s : Multiset α
⊢ ∀ (a : List α), (powersetCard n ⟦a⟧).card = (card ⟦a⟧).choose n

Tactic:
simp [powersetCard_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_insertEntry_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k a : α} {v : β k} (h : k == a) : containsKey a (insertEntry k v l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ containsKey a (insertEntry k v l) = true

Tactic:
simp [h]

Result:
no goals