harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Defs.lean
theorem npowRec'_two_mul {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
    npowRec' (2 * k) m = npowRec' k (m * m)

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 0 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * 0) m = npowRec' 0 (m * m)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec' (2 * k) m = npowRec' k (m * m)

Tactic:
induction k using Nat.strongRecOn with
| ind k' ih =>
  match k' with
  | 0 => rfl
  | 1 => simp [npowRec']
  | k + 2 => simp [npowRec', ← mul_assoc, Nat.mul_add, ← ih]

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 1 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * 1) m = npowRec' 1 (m * m)

Tactic:
simp [npowRec']

Result:
no goals

Proof state:
case ind
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k' → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * k') m = npowRec' k' (m * m)

Tactic:
match k' with
| 0 => rfl
| 1 => simp [npowRec']
| k + 2 => simp [npowRec', ← mul_assoc, Nat.mul_add, ← ih]

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 2 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * (k + 2)) m = npowRec' (k + 2) (m * m)

Tactic:
simp [npowRec', ← mul_assoc, Nat.mul_add, ← ih]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_powerset_neg_one_pow_card {α : Type*} [DecidableEq α] {x : Finset α} :
    (∑ m ∈ x.powerset, (-1 : ℤ) ^ #m) = if x = ∅ then 1 else 0

Proof state:
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ range (#x + 1), (#x).choose m • (-1) ^ m = if x = ∅ then 1 else 0

Tactic:
simp only [nsmul_eq_mul', ← card_eq_zero, Int.alternating_sum_range_choose]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = if x = ∅ then 1 else 0

Tactic:
rw [sum_powerset_apply_card]

Result:
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ range (#x + 1), (#x).choose m • (-1) ^ m = if x = ∅ then 1 else 0
-- Mathlib/Topology/Compactness/Compact.lean
theorem inCompact.isBounded_iff : @IsBounded _ (inCompact X) s ↔ ∃ t, IsCompact t ∧ s ⊆ t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
change sᶜ ∈ Filter.cocompact X ↔ _

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ cocompact X ↔ ∃ t, IsCompact t ∧ s ⊆ t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ cocompact X ↔ ∃ t, IsCompact t ∧ s ⊆ t

Tactic:
rw [Filter.mem_cocompact]

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_eq_zero : f.reverse = 0 ↔ f = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse = 0 ↔ f = 0

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h : a ∈ l) :
    f a (H a h) ∈ pmap f l H

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ ∃ a_1 h_1, f a_1 ⋯ = f a ⋯

Tactic:
exact ⟨a, h, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ f a ⋯ ∈ pmap f l H

Tactic:
rw [mem_pmap]

Result:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ ∃ a_1 h_1, f a_1 ⋯ = f a ⋯
-- Mathlib/Topology/Basic.lean
theorem isClosed_iff_nhds :
    IsClosed s ↔ ∀ x, (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s

Tactic:
simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable {a : E} (ha : IsSeparable F a)
    (q : ℕ) [ExpChar F q] (n : ℕ) : F⟮a⟯ = F⟮a ^ q ^ n⟯

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
a : E
ha : IsSeparable F a
q : ℕ
inst✝ : ExpChar F q
n : ℕ
this : Algebra.IsSeparable F ↥F⟮a⟯
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Tactic:
simpa using adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E {a} q n

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
a : E
ha : IsSeparable F a
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).mpr ha

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
a : E
ha : IsSeparable F a
q : ℕ
inst✝ : ExpChar F q
n : ℕ
this : Algebra.IsSeparable F ↥F⟮a⟯
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_lt_self (h : 1 < n) : sqrt n < n :=
  sqrt_lt.2 <| by have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h); rwa [Nat.mul_one] at this

Proof state:
n : ℕ
h : 1 < n
⊢ n < n * n

Tactic:
have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h)

Result:
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n

Proof state:
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n

Tactic:
rwa [Nat.mul_one] at this

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivAt_comp_add_left (a : E) :
    HasFDerivAt (fun x ↦ f (a + x)) f' x ↔ HasFDerivAt f f' (a + x)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x a : E
⊢ HasFDerivAt (fun x => f (a + x)) f' x ↔ HasFDerivAt f f' (a + x)

Tactic:
simpa [add_comm a] using hasFDerivAt_comp_add_right a

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_comp_sub_const {a b : 𝕜} :
    DifferentiableAt 𝕜 (fun x ↦ f (x - b)) a ↔ DifferentiableAt 𝕜 f (a - b)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 (fun x => f (x - b)) a ↔ DifferentiableAt 𝕜 f (a - b)

Tactic:
simp [sub_eq_add_neg, differentiableAt_comp_add_const]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem smul_right {R : Type*} [Semiring R] [DistribMulAction R N] [ContinuousConstSMul R N]
    (r : R) (h : v ⟂ᵥ w) : v ⟂ᵥ r • w :=
  let ⟨s, hmeas, hs₁, hs₂⟩ := h
  ⟨s, hmeas, hs₁, fun t ht => by simp only [coe_smul, Pi.smul_apply, hs₂ t ht, smul_zero]⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
R : Type u_6
inst✝² : Semiring R
inst✝¹ : DistribMulAction R N
inst✝ : ContinuousConstSMul R N
r : R
h : v ⟂ᵥ w
s : Set α
hmeas : MeasurableSet s
hs₁ : ∀ t ⊆ s, ↑v t = 0
hs₂ : ∀ t ⊆ sᶜ, ↑w t = 0
t : Set α
ht : t ⊆ sᶜ
⊢ ↑(r • w) t = 0

Tactic:
simp only [coe_smul, Pi.smul_apply, hs₂ t ht, smul_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma slope_of_Y_ne_eq_eval {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
    W.slope x₁ x₂ y₁ y₂ = -W.polynomialX.evalEval x₁ y₁ / W.polynomialY.evalEval x₁ y₁

Proof state:
case e_a
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) = 2 * y₁ + W.a₁ * x₁ + W.a₃

Tactic:
ring1

Result:
no goals

Proof state:
case e_a
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY

Tactic:
rw [negY, evalEval_polynomialY]

Result:
case e_a
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) = 2 * y₁ + W.a₁ * x₁ + W.a₃

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY

Tactic:
congr 1

Result:
case e_a
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY

Tactic:
rw [slope_of_Y_ne hx hy, evalEval_polynomialX, neg_sub]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) =
    (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY
-- Mathlib/Topology/Constructions.lean
lemma Topology.IsClosedEmbedding.uliftDown [TopologicalSpace X] :
    IsClosedEmbedding (ULift.down : ULift.{v, u} X → X) :=
  ⟨.uliftDown, by simp only [ULift.down_surjective.range_eq, isClosed_univ]⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ IsClosed (range ULift.down)

Tactic:
simp only [ULift.down_surjective.range_eq, isClosed_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_true_iff_exists_mem [BEq α] {l : List ((a : α) × β a)} {a : α} :
    containsKey a l = true ↔ ∃ p ∈ l, p.1 == a

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = true ↔ ∃ p, p ∈ l ∧ (p.fst == a) = true

Tactic:
induction l using assoc_induction <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma smul_set_stabilizer_subset (ha : a ∈ s) : a • (stabilizer G s : Set G) ⊆ s

Proof state:
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
ha : a ∈ s
⊢ a • ↑(stabilizer G s) ⊆ s

Tactic:
simpa using op_smul_set_stabilizer_subset ha

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem nhds_le_of_le {f} (h : x ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 x ≤ f

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
f : Filter X
h : x ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ 𝓝 x ≤ f

Tactic:
rw [nhds_def]

Result:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
f : Filter X
h : x ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 s ≤ f

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
f : Filter X
h : x ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 s ≤ f

Tactic:
exact iInf₂_le_of_le s ⟨h, o⟩ sf

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma expect_le_expect (hfg : ∀ i ∈ s, f i ≤ g i) : 𝔼 i ∈ s, f i ≤ 𝔼 i ∈ s, g i :=
  smul_le_smul_of_nonneg_left (sum_le_sum hfg) <| by positivity

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f g : ι → α
inst✝ : PosSMulMono ℚ≥0 α
hfg : ∀ i ∈ s, f i ≤ g i
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_eq_size {l : Vector α n} : count a l = l.size ↔ ∀ b ∈ l, a = b

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ count a { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }.size ↔
    ∀ (b : α), b ∈ { toArray := l, size_toArray := ⋯ } → a = b

Tactic:
simp [Array.count_eq_size]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
l : Vector α n
⊢ count a l = l.size ↔ ∀ (b : α), b ∈ l → a = b

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ count a { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }.size ↔
    ∀ (b : α), b ∈ { toArray := l, size_toArray := ⋯ } → a = b
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsuppLid_apply_apply (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) :
    finsuppTensorFinsuppLid R N ι κ (f ⊗ₜ[R] g) (a, b) = f a • g b

Proof state:
R : Type u_1
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ι →₀ R
g : κ →₀ N
a : ι
b : κ
⊢ ((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b

Tactic:
simp [finsuppTensorFinsuppLid]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.isoColimitCocone_ι_inv {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
    t.cocone.ι.app j ≫ (colimit.isoColimitCocone t).inv = colimit.ι F j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ t.cocone.ι.app j ≫ t.isColimit.desc (cocone F) = ι F j

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ t.cocone.ι.app j ≫ (isoColimitCocone t).inv = ι F j

Tactic:
dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
t : ColimitCocone F
j : J
⊢ t.cocone.ι.app j ≫ t.isColimit.desc (cocone F) = ι F j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_eq_mkVector_iff {l : Vector α n} {f : Nat → α → β} {b : β} :
    mapIdx f l = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] = b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : Array α
⊢ mapIdx f { toArray := l, size_toArray := ⋯ } = mkVector l.size b ↔
    ∀ (i : Nat) (h : i < l.size), f i { toArray := l, size_toArray := ⋯ }[i] = b

Tactic:
simp [Array.mapIdx_eq_mkArray_iff]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : Nat → α → β
b : β
⊢ mapIdx f l = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] = b

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : Array α
⊢ mapIdx f { toArray := l, size_toArray := ⋯ } = mkVector l.size b ↔
    ∀ (i : Nat) (h : i < l.size), f i { toArray := l, size_toArray := ⋯ }[i] = b
-- Mathlib/Order/Minimal.lean
theorem maximal_true_subtype {x : Subtype P} : Maximal (fun _ ↦ True) x ↔ Maximal P x

Proof state:
case mk
α : Type u_1
P : α → Prop
inst✝ : LE α
x : α
hx : P x
⊢ Maximal (fun x => True) ⟨x, hx⟩ ↔ Maximal P ↑⟨x, hx⟩

Tactic:
simp [Maximal, hx]

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
inst✝ : LE α
x : Subtype P
⊢ Maximal (fun x => True) x ↔ Maximal P ↑x

Tactic:
obtain ⟨x, hx⟩ := x

Result:
case mk
α : Type u_1
P : α → Prop
inst✝ : LE α
x : α
hx : P x
⊢ Maximal (fun x => True) ⟨x, hx⟩ ↔ Maximal P ↑⟨x, hx⟩
-- Mathlib/LinearAlgebra/Dimension/Localization.lean
lemma nonempty_oreSet_of_strongRankCondition [StrongRankCondition R] :
    Nonempty (OreLocalization.OreSet R⁰)

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
⊢ Nonempty (OreLocalization.OreSet R⁰)

Tactic:
by_contra h

Result:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : ¬Nonempty (OreLocalization.OreSet R⁰)
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : ¬Nonempty (OreLocalization.OreSet R⁰)
⊢ False

Tactic:
have := aleph0_le_rank_of_isEmpty_oreSet (not_nonempty_iff.mp h)

Result:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : ¬Nonempty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ Module.rank R R
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : ¬Nonempty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ Module.rank R R
⊢ False

Tactic:
rw [rank_self] at this

Result:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : ¬Nonempty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ 1
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : ¬Nonempty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ 1
⊢ False

Tactic:
exact this.not_lt one_lt_aleph0

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem setIntegral_piecewise (a : α) (g : β → E) (t : Set β) :
    ∫ b in t, g b ∂piecewise hs κ η a =
      if a ∈ s then ∫ b in t, g b ∂κ a else ∫ b in t, g b ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → E
t : Set β
⊢ ∫ (b : β) in t, g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a

Tactic:
simp_rw [piecewise_apply]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → E
t : Set β
⊢ (∫ (b : β) in t, g b ∂if a ∈ s then κ a else η a) =
    if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → E
t : Set β
⊢ (∫ (b : β) in t, g b ∂if a ∈ s then κ a else η a) =
    if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_tail (f : α → β) (l : List α) :
    map f l.tail = (map f l).tail

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l.tail = (map f l).tail

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_sub_of_le {a b c : Ordinal} (h : b ≤ a) : c ≤ a - b ↔ b + c ≤ a

Proof state:
a b c : Ordinal.{u_4}
h : b ≤ a
⊢ c ≤ a - b ↔ b + c ≤ a

Tactic:
rw [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem idxOf?_toList [BEq α] {a : α} {l : Array α} :
    l.toList.idxOf? a = l.idxOf? a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ List.idxOf? a l.toList = l.idxOf? a

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ List.idxOf? a { toList := l }.toList = { toList := l }.idxOf? a

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ List.idxOf? a { toList := l }.toList = { toList := l }.idxOf? a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem div_div_self (a : G₀) : a / (a / a) = a

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a / a) = a

Tactic:
rw [div_div_eq_mul_div]

Result:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Tactic:
exact mul_self_div_self a

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.takeUntil {u v w : V} {p : G.Walk v w} (hc : p.IsPath)
    (h : u ∈ p.support) : (p.takeUntil u h).IsPath :=
  IsPath.of_append_left (q := p.dropUntil u h) (by rwa [← take_spec _ h] at hc)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsPath
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath

Tactic:
rwa [← take_spec _ h] at hc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem xor_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    lhs' ^^^ rhs' = lhs ^^^ rhs

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' ^^^ rhs' = lhs ^^^ rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_eq_univ : (s : Set α) = univ ↔ s = ⊥

Proof state:
α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = univ ↔ s = ⊥

Tactic:
simp [SetLike.ext'_iff]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.spectrum_zero_eq [Nontrivial A] :
    spectrum R (0 : A) = {0}

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
⊢ spectrum R 0 = {0}

Tactic:
have : (0 : A) = algebraMap R A 0 := Eq.symm (RingHom.map_zero (algebraMap R A))

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
this : 0 = (algebraMap R A) 0
⊢ spectrum R 0 = {0}

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
this : 0 = (algebraMap R A) 0
⊢ spectrum R 0 = {0}

Tactic:
rw [this, spectrum_algebraMap_eq]

Result:
no goals