harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/SuccPred.lean
theorem covBy_iff_sub_one_eq [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] :
    x ⋖ y ↔ y - 1 = x

Proof state:
α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
⊢ x ⋖ y ↔ y - 1 = x

Tactic:
rw [← pred_eq_sub_one]

Result:
α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
⊢ x ⋖ y ↔ pred y = x

Proof state:
α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
⊢ x ⋖ y ↔ pred y = x

Tactic:
exact pred_eq_iff_covBy.symm

Result:
no goals
-- Mathlib/Order/RelSeries.lean
@[simp]
lemma head_take (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.take i).head = p.head

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.take i).head = p.head

Tactic:
simp [take, head]

Result:
no goals
-- Mathlib/FieldTheory/KrullTopology.lean
theorem IntermediateField.fixingSubgroup.antimono {K L : Type*} [Field K] [Field L] [Algebra K L]
    {E1 E2 : IntermediateField K L} (h12 : E1 ≤ E2) : E2.fixingSubgroup ≤ E1.fixingSubgroup

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h12 : E1 ≤ E2
⊢ E2.fixingSubgroup ≤ E1.fixingSubgroup

Tactic:
rintro σ hσ ⟨x, hx⟩

Result:
case mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h12 : E1 ≤ E2
σ : L ≃ₐ[K] L
hσ : σ ∈ E2.fixingSubgroup
x : L
hx : x ∈ ↑E1
⊢ σ • ↑⟨x, hx⟩ = ↑⟨x, hx⟩

Proof state:
case mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h12 : E1 ≤ E2
σ : L ≃ₐ[K] L
hσ : σ ∈ E2.fixingSubgroup
x : L
hx : x ∈ ↑E1
⊢ σ • ↑⟨x, hx⟩ = ↑⟨x, hx⟩

Tactic:
exact hσ ⟨x, h12 hx⟩

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma pred_one_add (n : ℕ) : pred (1 + n) = n

Proof state:
n : ℕ
⊢ (1 + n).pred = n

Tactic:
rw [Nat.add_comm, add_one, Nat.pred_succ]

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem ofRingEquiv_dpow_apply (hI : DividedPowers I) {n : ℕ} {a : A} :
    (ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a)

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
⊢ (ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem mem_iUnion : x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
⊢ x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J

Tactic:
convert Set.mem_iUnion₂

Result:
case h.e'_2.h.e'_2.h.a
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π.toPrepartition), x ∈ ↑x✝

Proof state:
case h.e'_2.h.e'_2.h.a
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π.toPrepartition), x ∈ ↑x✝

Tactic:
rw [Box.mem_coe, mem_toPrepartition, exists_prop]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivativeFun_coe (f : R[X]) : (f : R⟦X⟧).derivativeFun = derivative f

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
⊢ (coeff R n✝) (↑f).derivativeFun = (coeff R n✝) ↑(derivative f)

Tactic:
rw [coeff_derivativeFun, coeff_coe, coeff_coe, coeff_derivative]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ (↑f).derivativeFun = ↑(derivative f)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n✝ : ℕ
⊢ (coeff R n✝) (↑f).derivativeFun = (coeff R n✝) ↑(derivative f)
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem edgeFinset_sup_edge [Fintype (edgeSet (G ⊔ edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) :
    (G ⊔ edge s t).edgeFinset = G.edgeFinset.cons s(s, t) (by simp_all)

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ (G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯

Tactic:
rw [edgeFinset_sup, cons_eq_insert, insert_eq, union_comm]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ (edge s t).edgeFinset ∪ G.edgeFinset = {s(s, t)} ∪ G.edgeFinset

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ {s(s, t)}.toFinset ∪ G.edgeSet.toFinset = {s(s, t)} ∪ G.edgeSet.toFinset

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ (edge s t).edgeFinset ∪ G.edgeFinset = {s(s, t)} ∪ G.edgeFinset

Tactic:
simp_rw [edgeFinset, edge_edgeSet_of_ne h]

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ {s(s, t)}.toFinset ∪ G.edgeSet.toFinset = {s(s, t)} ∪ G.edgeSet.toFinset

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ (G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯

Tactic:
letI := Classical.decEq V

Result:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
this : DecidableEq V := Classical.decEq V
⊢ (G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ s(s, t) ∉ G.edgeFinset

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_inv_self : a / b = b⁻¹ ↔ a = 1

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = b⁻¹ ↔ a = 1

Tactic:
rw [div_eq_mul_inv, mul_left_eq_self]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpL1_mono {E} [NormedLatticeAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E]
    [OrderedSMul ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
    condExpL1 hm μ f ≤ᵐ[μ] condExpL1 hm μ g

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ condExpL1 hm μ f ≤ condExpL1 hm μ g

Tactic:
have h_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x : E, 0 ≤ x → 0 ≤ condExpInd E hm μ s x :=
  fun s hs hμs x hx => condExpInd_nonneg hs hμs.ne x hx

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), 0 ≤ x → 0 ≤ (condExpInd E hm μ s) x
⊢ condExpL1 hm μ f ≤ condExpL1 hm μ g

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ ↑↑(condExpL1 hm μ f) ≤ᶠ[ae μ] ↑↑(condExpL1 hm μ g)

Tactic:
rw [coeFn_le]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ condExpL1 hm μ f ≤ condExpL1 hm μ g

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝⁴ : SigmaFinite (μ.trim hm)
E : Type u_7
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), 0 ≤ x → 0 ≤ (condExpInd E hm μ s) x
⊢ condExpL1 hm μ f ≤ condExpL1 hm μ g

Tactic:
exact setToFun_mono (dominatedFinMeasAdditive_condExpInd E hm μ) h_nonneg hf hg hfg

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
/-- Auxiliary lemma. Use `limit_of_surjections_surjective` instead. -/
lemma surjective_π_app_zero_of_surjective_map_aux :
    Function.Surjective ((limitCone F).π.app ⟨0⟩)

Proof state:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)
⊢ F.map (Opposite.op { down := { down := ⋯ } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p.succ)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)

Tactic:
rw [← ih]

Result:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)
⊢ F.map (Opposite.op { down := { down := ⋯ } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p.succ)) =
    F.map (Opposite.op { down := { down := h } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op p))

Proof state:
case refl
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)
a : F.obj (Opposite.op 0)
n m : ℕ
⊢ F.map (Opposite.op { down := { down := ⋯ } })
      ((fun x =>
          match x with
          | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
        (Opposite.op m)) =
    (fun x =>
        match x with
        | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n)
      (Opposite.op m)

Tactic:
erw [CategoryTheory.Functor.map_id, types_id_apply]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_zero : degrees (0 : MvPolynomial σ R) = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).degrees = 0

Tactic:
exact degrees_C 0

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ degrees 0 = 0

Tactic:
rw [← C_0]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).degrees = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α} {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
    getKey? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (insertManyIfNewUnit empty l).val.getKey? k' = some k

Tactic:
exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
  contains_empty distinct mem

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem lt_neg_comm {a b : EReal} : a < -b ↔ b < -a

Proof state:
a b : EReal
⊢ a < -b ↔ b < -a

Tactic:
rw [← neg_lt_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y

Proof state:
case mpr
w : Nat
x y : BitVec w
h : x ≠ -y
h' : -x = y
⊢ False

Tactic:
subst h'

Result:
case mpr
w : Nat
x : BitVec w
h : x ≠ - -x
⊢ False

Proof state:
w : Nat
x y : BitVec w
⊢ -x ≠ y ↔ x ≠ -y

Tactic:
constructor

Result:
case mp
w : Nat
x y : BitVec w
⊢ -x ≠ y → x ≠ -y

case mpr
w : Nat
x y : BitVec w
⊢ x ≠ -y → -x ≠ y

Proof state:
case mp
w : Nat
x y : BitVec w
⊢ -x ≠ y → x ≠ -y

case mpr
w : Nat
x y : BitVec w
⊢ x ≠ -y → -x ≠ y

Tactic:
all_goals
  intro h h'
  subst h'
  simp at h

Result:
no goals

Proof state:
case mpr
w : Nat
x y : BitVec w
⊢ x ≠ -y → -x ≠ y

Tactic:
intro h h'

Result:
case mpr
w : Nat
x y : BitVec w
h : x ≠ -y
h' : -x = y
⊢ False

Proof state:
case mpr
w : Nat
x : BitVec w
h : x ≠ - -x
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem const_mul_cancel (f g₁ g₂ : R) (U hu₁ hu₂) :
    const R f g₁ U hu₁ * const R g₁ g₂ U hu₂ = const R f g₂ U hu₂

Proof state:
case h
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl
⊢ f * g₁ * g₂ = f * (g₁ * g₂)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl
⊢ const R f g₁ U hu₁ * const R g₁ g₂ U hu₂ = const R f g₂ U hu₂

Tactic:
rw [const_mul, const_ext]

Result:
case h
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl
⊢ f * g₁ * g₂ = f * (g₁ * g₂)
-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem prod_pow_factorization_centralBinom (n : ℕ) :
    (∏ p ∈ Finset.range (2 * n + 1), p ^ (centralBinom n).factorization p) = centralBinom n

Proof state:
case hkn
n : ℕ
⊢ n ≤ 2 * n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
⊢ ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p = n.centralBinom

Tactic:
apply prod_pow_factorization_choose

Result:
case hkn
n : ℕ
⊢ n ≤ 2 * n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_flatten (xs : Array (Array α)) (p : α → Bool) :
    xs.flatten.find? p = xs.findSome? (·.find? p)

Proof state:
α : Type u_1
xs : Array (Array α)
p : α → Bool
⊢ find? p xs.flatten = findSome? (fun x => find? p x) xs

Tactic:
cases xs using array₂_induction

Result:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ find? p (List.map List.toArray xss✝).toArray.flatten =
    findSome? (fun x => find? p x) (List.map List.toArray xss✝).toArray

Proof state:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ find? p (List.map List.toArray xss✝).toArray.flatten =
    findSome? (fun x => find? p x) (List.map List.toArray xss✝).toArray

Tactic:
simp [List.findSome?_map, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive zsmul_neg]
lemma inv_zpow (a : α) : ∀ n : ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
  | (n : ℕ)    => by rw [zpow_natCast, zpow_natCast, inv_pow]
  | .negSucc n => by rw [zpow_negSucc, zpow_negSucc, inv_pow]

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ ↑n = (a ^ ↑n)⁻¹

Tactic:
rw [zpow_natCast, zpow_natCast, inv_pow]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹

Tactic:
rw [zpow_negSucc, zpow_negSucc, inv_pow]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
theorem associator_hom_snd_fst (X Y Z : C) :
    (α_ X Y Z).hom ≫ prod.snd ≫ prod.fst = prod.fst ≫ prod.snd

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ prod.snd ≫ prod.fst = prod.fst ≫ prod.snd

Tactic:
simp [associator_hom]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma equation_iff (x y : R) : W'.Equation x y ↔
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ↔ y ^ 2 + W'.a₁ * x * y + W'.a₃ * y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆

Tactic:
rw [equation_iff', sub_eq_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp, norm_cast]
lemma rpow_intCast (x : ℝ≥0) (n : ℤ) : x ^ (n : ℝ) = x ^ n

Proof state:
x : ℝ≥0
n : ℤ
⊢ x ^ ↑n = x ^ n

Tactic:
cases n <;> simp only [Int.ofNat_eq_coe, Int.cast_natCast, rpow_natCast, zpow_natCast,
  Int.cast_negSucc, rpow_neg, zpow_negSucc]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_iff_exists_le {x y : PGame} :
    x ⧏ y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y

Proof state:
x y : PGame
⊢ ((¬∀ (i : y.LeftMoves), y.moveLeft i ⧏ x) ∨ ¬∀ (j : x.RightMoves), y ⧏ x.moveRight j) ↔
    (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y

Tactic:
simp

Result:
no goals

Proof state:
x y : PGame
⊢ x ⧏ y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y

Tactic:
rw [LF, le_iff_forall_lf, not_and_or]

Result:
x y : PGame
⊢ ((¬∀ (i : y.LeftMoves), y.moveLeft i ⧏ x) ∨ ¬∀ (j : x.RightMoves), y ⧏ x.moveRight j) ↔
    (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y
-- Mathlib/SetTheory/Cardinal/Subfield.lean
private lemma rangeOfWType_eq_top : rangeOfWType s = ⊤ := top_le_iff.mp fun a _ ↦ by
  rw [← SetLike.mem_coe, ← Subtype.val_injective.mem_set_image]
  change ↑a ∈ map (closure s).subtype _
  refine closure_le.mpr (fun a ha ↦ ?_) a.prop
  exact ⟨⟨a, subset_closure ha⟩, ⟨WType.mk (.inr ⟨a, ha⟩) Empty.rec, rfl⟩, rfl⟩

Proof state:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ a ∈ Subfield.rangeOfWType s

Tactic:
rw [← SetLike.mem_coe, ← Subtype.val_injective.mem_set_image]

Result:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ Subtype.val '' ↑(Subfield.rangeOfWType s)

Proof state:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ Subtype.val '' ↑(Subfield.rangeOfWType s)

Tactic:
change ↑a ∈ map (closure s).subtype _

Result:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ map (closure s).subtype (Subfield.rangeOfWType s)

Proof state:
α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ map (closure s).subtype (Subfield.rangeOfWType s)

Tactic:
refine closure_le.mpr (fun a ha ↦ ?_) a.prop

Result:
α : Type u
s : Set α
inst✝ : DivisionRing α
a✝ : ↥(closure s)
x✝ : a✝ ∈ ⊤
a : α
ha : a ∈ s
⊢ a ∈ ↑(map (closure s).subtype (Subfield.rangeOfWType s))

Proof state:
α : Type u
s : Set α
inst✝ : DivisionRing α
a✝ : ↥(closure s)
x✝ : a✝ ∈ ⊤
a : α
ha : a ∈ s
⊢ a ∈ ↑(map (closure s).subtype (Subfield.rangeOfWType s))

Tactic:
exact ⟨⟨a, subset_closure ha⟩, ⟨WType.mk (.inr ⟨a, ha⟩) Empty.rec, rfl⟩, rfl⟩

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_smul_ball (p : Seminorm 𝕜 E) {r₁ : ℝ} (hr₁ : r₁ ≠ 0) (r₂ : ℝ) :
    Metric.closedBall (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), p b < r₂ → ‖a‖ * p b < r₁ * r₂

Tactic:
refine fun a ha b hb ↦ mul_lt_mul' ha hb (apply_nonneg _ _) ?_

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b < r₂
⊢ 0 < r₁

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b < r₂
⊢ 0 < r₁

Tactic:
exact hr₁.lt_or_lt.resolve_left <| ((norm_nonneg a).trans ha).not_lt

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ Metric.closedBall 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), p b < r₂ → ‖a‖ * p b < r₁ * r₂
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_sub_mk' {M M' : Type*} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M']
    (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : S) :
    mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)

Tactic:
rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Real.Ioo_eq_ball (x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2)

Proof state:
x y : ℝ
⊢ Ioo x y = ball ((x + y) / 2) ((y - x) / 2)

Tactic:
rw [Real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
  ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowingε₀_two : fastGrowingε₀ 2 = 2048

Proof state:
⊢ fastGrowingε₀ 2 = 2048

Tactic:
norm_num [fastGrowingε₀, show oadd 0 1 0 = 1 from rfl, @fastGrowing_limit (oadd 1 1 0) _ rfl,
  show oadd 0 (2 : Nat).succPNat 0 = 3 from rfl, @fastGrowing_succ 3 2 rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_eq_bind {x : Option α} : x.map f = x.bind (some ∘ f)

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → α✝
x : Option α
⊢ Option.map f x = x.bind (some ∘ f)

Tactic:
cases x <;> simp [Option.bind]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem lcm_image [DecidableEq β] {g : γ → β} (s : Finset γ) :
    (s.image g).lcm f = s.lcm (f ∘ g)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).lcm f = s.lcm (f ∘ g)

Tactic:
induction s using Finset.induction <;> simp [*]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).lcm f = s.lcm (f ∘ g)

Tactic:
classical induction s using Finset.induction <;> simp [*]

Result:
no goals