harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_add (x₁ x₂ : R) (y₁ y₂ : M) :
    mk' S (x₁ * y₂ + x₂ * y₁) (y₁ * y₂) = mk' S x₁ y₁ + mk' S x₂ y₂ :=
  mk'_eq_iff_eq_mul.2 <|
    Eq.symm
      (by
        rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
          mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul,
          mk'_add_eq_iff_add_mul_eq_mul]
        simp only [map_add, Submonoid.coe_mul, map_mul]
        ring)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) ↑y₁ * ((algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂) * (algebraMap R S) x₂ +
      (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂ * (algebraMap R S) x₁ * (algebraMap R S) ↑y₂ =
    ((algebraMap R S) x₁ * (algebraMap R S) ↑y₂ + (algebraMap R S) x₂ * (algebraMap R S) ↑y₁) * (algebraMap R S) ↑y₁ *
      (algebraMap R S) ↑y₂

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑y₁ * ↑(y₁ * y₂) * x₂) + (algebraMap R S) (↑(y₁ * y₂) * x₁) * (algebraMap R S) ↑y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂

Tactic:
simp only [map_add, Submonoid.coe_mul, map_mul]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) ↑y₁ * ((algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂) * (algebraMap R S) x₂ +
      (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂ * (algebraMap R S) x₁ * (algebraMap R S) ↑y₂ =
    ((algebraMap R S) x₁ * (algebraMap R S) ↑y₂ + (algebraMap R S) x₂ * (algebraMap R S) ↑y₁) * (algebraMap R S) ↑y₁ *
      (algebraMap R S) ↑y₂

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (mk' S x₁ y₁ + mk' S x₂ y₂) * (algebraMap R S) ↑(y₁ * y₂) = (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁)

Tactic:
rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
  mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul,
  mk'_add_eq_iff_add_mul_eq_mul]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑y₁ * ↑(y₁ * y₂) * x₂) + (algebraMap R S) (↑(y₁ * y₂) * x₁) * (algebraMap R S) ↑y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem fieldRange_le : (algebraMap K L).fieldRange ≤ S.toSubfield := fun x hx =>
  S.toSubalgebra.range_subset (by rwa [Set.mem_range, ← RingHom.mem_fieldRange])

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ (algebraMap K L).fieldRange
⊢ x ∈ Set.range ⇑(algebraMap K L)

Tactic:
rwa [Set.mem_range, ← RingHom.mem_fieldRange]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_matrix' (m n : Type v) [Finite m] [Finite n] :
    Module.rank R (Matrix m n R) = Cardinal.lift.{u} (#m * #n)

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)

Tactic:
rw [rank_matrix, lift_mul, lift_umax.{v, u}]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atTop_of_pos (hr : 0 < r) :
    Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atTop :=
  ⟨fun h => h.atTop_of_const_mul₀ hr, fun h =>
    Tendsto.atTop_of_const_mul₀ (inv_pos.2 hr) <| by simpa only [inv_mul_cancel_left₀ hr.ne'] ⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
hr : 0 < r
h : Tendsto f l atTop
⊢ Tendsto (fun x => r⁻¹ * (r * f x)) l atTop

Tactic:
simpa only [inv_mul_cancel_left₀ hr.ne']

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem ofInt'_eq : ∀ n : ℤ, ZNum.ofInt' n = n
  | (n : ℕ) => rfl
  | -[n+1] => by
    show Num.toZNumNeg (n + 1 : ℕ) = -(n + 1 : ℕ)
    rw [← neg_inj, neg_neg, Nat.cast_succ, Num.add_one, Num.zneg_toZNumNeg, Num.toZNum_succ,
      Nat.cast_succ, ZNum.add_one]
    rfl

Proof state:
n : ℕ
⊢ ofInt' -[n+1] = ↑-[n+1]

Tactic:
show Num.toZNumNeg (n + 1 : ℕ) = -(n + 1 : ℕ)

Result:
n : ℕ
⊢ (↑(n + 1)).toZNumNeg = -↑(n + 1)

Proof state:
n : ℕ
⊢ (↑n).toZNum.succ = (↑n).succ

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ (↑(n + 1)).toZNumNeg = -↑(n + 1)

Tactic:
rw [← neg_inj, neg_neg, Nat.cast_succ, Num.add_one, Num.zneg_toZNumNeg, Num.toZNum_succ,
  Nat.cast_succ, ZNum.add_one]

Result:
n : ℕ
⊢ (↑n).toZNum.succ = (↑n).succ
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Cone.ofTrident_π {F : WalkingParallelFamily J ⥤ C} (t : Trident fun j => F.map (line j))
    (j) : (Cone.ofTrident t).π.app j = t.π.app j ≫ eqToHom (by cases j <;> aesop_cat) :=
  rfl

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j => F.map (line j)
j : WalkingParallelFamily J
⊢ (parallelFamily fun j => F.map (line j)).obj j = F.obj j

Tactic:
cases j <;> aesop_cat

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrixAlgEquiv_comp (f g : M₁ →ₗ[R] M₁) :
    LinearMap.toMatrixAlgEquiv v₁ (f.comp g) =
      LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁) (f ∘ₗ g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g

Tactic:
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
theorem map_neg : X (-f) = -X f

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ X (-f) = -X f

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_lt_lift_iff {a : Cardinal.{u}} :
    (1 : Cardinal) < lift.{v} a ↔ 1 < a

Proof state:
a : Cardinal.{u}
⊢ 1 < lift.{v, u} a ↔ 1 < a

Tactic:
simpa using nat_lt_lift_iff (n := 1)

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_get : ∀ l : List α, (ofFn (get l)) = l
  | [] => by rw [ofFn_zero]
  | a :: l => by
    rw [ofFn_succ]
    congr
    exact ofFn_get l

Proof state:
α : Type u
a : α
l : List α
⊢ ((a :: l).get 0 :: ofFn fun i => (a :: l).get i.succ) = a :: l

Tactic:
congr

Result:
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => (a :: l).get i.succ) = l

Proof state:
α : Type u
a : α
l : List α
⊢ ofFn (a :: l).get = a :: l

Tactic:
rw [ofFn_succ]

Result:
α : Type u
a : α
l : List α
⊢ ((a :: l).get 0 :: ofFn fun i => (a :: l).get i.succ) = a :: l

Proof state:
α : Type u
⊢ ofFn [].get = []

Tactic:
rw [ofFn_zero]

Result:
no goals

Proof state:
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => (a :: l).get i.succ) = l

Tactic:
exact ofFn_get l

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
@[simp] lemma exterior_subset_iff_isOpen : exterior s ⊆ s ↔ IsOpen s

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ exterior s ⊆ s ↔ IsOpen s

Tactic:
simp only [exterior_eq_iff_isOpen.symm, Subset.antisymm_iff, subset_exterior, and_true]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NF.zero_of_zero {e n a} (h : NF (ONote.oadd e n a)) (e0 : e = 0) : a = 0

Proof state:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ a = 0

Tactic:
simpa [e0, NFBelow_zero] using h.snd'

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem finrank_eq_card_finset_basis {ι : Type w} {b : Finset ι} (h : Basis b R M) :
    finrank R M = Finset.card b

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Finset ι
h : Basis { x // x ∈ b } R M
⊢ finrank R M = b.card

Tactic:
rw [finrank_eq_card_basis h, Fintype.card_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem umod_zero {x : BitVec n} : x % 0#n = x

Proof state:
n : Nat
x : BitVec n
⊢ x % 0#n = x

Tactic:
simp [umod_def]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem right_nonuniformWitnesses_card (h : ¬G.IsUniform ε s t) :
    #t * ε ≤ #(G.nonuniformWitnesses ε s t).2

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#t) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).2)

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#t) * ε ≤ ↑(#(⋯.choose, ⋯.choose).2)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#t) * ε ≤ ↑(#(⋯.choose, ⋯.choose).2)

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.1

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_smul (m : ℝ≥0∞ → ℝ≥0∞) {c : ℝ≥0∞} (hc : c ≠ ∞) (hc' : c ≠ 0) :
    (mkMetric (c • m) : OuterMeasure X) = c • mkMetric m

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
hc' : c ≠ 0
⊢ mkMetric (c • m) = c • mkMetric m

Tactic:
simp only [mkMetric, mkMetric', mkMetric'.pre, inducedOuterMeasure, ENNReal.smul_iSup]

Result:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
hc' : c ≠ 0
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => (c • m) (diam s)) =
    c • ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => m (diam s))

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
hc' : c ≠ 0
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => (c • m) (diam s)) =
    c • ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => m (diam s))

Tactic:
simp_rw [smul_iSup, smul_boundedBy hc, smul_extend _ hc', Pi.smul_apply]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma AnalyticWithinAt.restrictScalars (hf : AnalyticWithinAt 𝕜' f s x) :
    AnalyticWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
s : Set E
hf : AnalyticWithinAt 𝕜' f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rcases hf with ⟨p, hp⟩

Result:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f s x

Proof state:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem ne_zero_iff_odd {n : ℕ} : (n : ZMod 2) ≠ 0 ↔ Odd n

Proof state:
case mpr
n : ℕ
⊢ Odd n → ↑n ≠ 0

Tactic:
contrapose

Result:
case mpr
n : ℕ
⊢ ¬↑n ≠ 0 → ¬Odd n

Proof state:
case mpr
n : ℕ
⊢ ¬↑n ≠ 0 → ¬Odd n

Tactic:
simp [eq_zero_iff_even]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.isEmpty = false ↔ ∃ a, a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.isEmpty = false ↔ ∃ a, a ∈ m

Tactic:
simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true h

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma sUnion_disjiUnion {f : α → Finset (Set β)} (I : Finset α)
    (hf : (I : Set α).PairwiseDisjoint f) :
    ⋃₀ (I.disjiUnion f hf : Set (Set β)) = ⋃ a ∈ I, ⋃₀ ↑(f a)

Proof state:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
⊢ ⋃₀ ↑(I.disjiUnion f hf) = ⋃ a ∈ I, ⋃₀ ↑(f a)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
x✝ : β
⊢ x✝ ∈ ⋃₀ ↑(I.disjiUnion f hf) ↔ x✝ ∈ ⋃ a ∈ I, ⋃₀ ↑(f a)

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
x✝ : β
⊢ (∃ t, (∃ i ∈ I, t ∈ f i) ∧ x✝ ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x✝ ∈ t

Tactic:
tauto

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
x✝ : β
⊢ x✝ ∈ ⋃₀ ↑(I.disjiUnion f hf) ↔ x✝ ∈ ⋃ a ∈ I, ⋃₀ ↑(f a)

Tactic:
simp only [coe_disjiUnion, Set.mem_sUnion, Set.mem_iUnion, mem_coe, exists_prop]

Result:
case h
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
x✝ : β
⊢ (∃ t, (∃ i ∈ I, t ∈ f i) ∧ x✝ ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x✝ ∈ t
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_nonempty (hs : ¬ BddAbove s) (o : Ordinal) :
    (s ∩ { b | ∀ c, c < o → enumOrd s c < b }).Nonempty

Proof state:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
obtain ⟨a, ha⟩ := bddAbove_of_small (enumOrd s '' Iio o)

Result:
case intro
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Proof state:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
rw [not_bddAbove_iff] at hs

Result:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Proof state:
case intro.intro.intro
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
b : Ordinal.{u}
hb : b ∈ s
hba : a < b
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
exact ⟨b, hb, fun c hc ↦ (ha (mem_image_of_mem _ hc)).trans_lt hba⟩

Result:
no goals

Proof state:
case intro
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
obtain ⟨b, hb, hba⟩ := hs a

Result:
case intro.intro.intro
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
b : Ordinal.{u}
hb : b ∈ s
hba : a < b
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty
-- Mathlib/Data/Nat/PartENat.lean
theorem ofENat_lt {x y : ℕ∞} : ofENat x < ofENat y ↔ x < y

Proof state:
x y : ℕ∞
⊢ ↑x < ↑y ↔ x < y

Tactic:
rw [← toWithTop_lt, toWithTop_ofENat, toWithTop_ofENat]

Result:
no goals

Proof state:
x y : ℕ∞
⊢ ↑x < ↑y ↔ x < y

Tactic:
classical
rw [← toWithTop_lt, toWithTop_ofENat, toWithTop_ofENat]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem linfty_opNorm_row (v : n → α) : ‖row ι v‖ = ∑ i, ‖v i‖ :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_row v).trans <| by simp [NNReal.coe_sum]

Proof state:
n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ↑(∑ i : n, ‖v i‖₊) = ∑ i : n, ‖v i‖

Tactic:
simp [NNReal.coe_sum]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma antivaryOn_iff_forall_mul_nonpos :
    AntivaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
s : Set ι
⊢ AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0

Tactic:
simp only [smul_eq_mul, antivaryOn_iff_forall_smul_nonpos]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
/-- The RHS is a noncomputable version of `Nat.floorRoot` with better order theoretical
properties. -/
lemma floorRoot_def :
    floorRoot n a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod (· ^ ·)

Proof state:
a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ (k / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2

Tactic:
split_ifs with h <;> simp [Finsupp.floorDiv_def, prod_mapRange_index pow_zero]

Result:
no goals

Proof state:
a n : ℕ
⊢ n.floorRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2

Tactic:
unfold floorRoot

Result:
a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ (k / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOn.tendstoLocallyUniformlyOn (h : TendstoUniformlyOn F f p s) :
    TendstoLocallyUniformlyOn F f p s := fun u hu _ _ =>
  ⟨s, self_mem_nhdsWithin, by simpa using h u hu⟩

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoUniformlyOn F f p s
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝¹ : α
x✝ : x✝¹ ∈ s
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u

Tactic:
simpa using h u hu

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem?_eq_none [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ↔ ¬dom c i

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
⊢ getElem? c i = none ↔ ¬dom c i

Tactic:
simp only [getElem?_def]

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
⊢ (if h : dom c i then some (getElem c i h) else none) = none ↔ ¬dom c i

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
⊢ (if h : dom c i then some (getElem c i h) else none) = none ↔ ¬dom c i

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Unitization.lean
theorem norm_eq_sup (x : Unitization 𝕜 A) :
    ‖x‖ = ‖x.fst‖ ⊔ ‖algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd‖

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖x‖ = ‖x.fst‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd‖

Tactic:
rw [norm_def, splitMul_apply, Prod.norm_def]

Result:
no goals
-- Mathlib/Logic/Function/CompTypeclasses.lean
lemma comp_apply {M N P : Type*}
    {φ : M → N} {ψ : N → P} {χ : M → P} (h : CompTriple φ ψ χ) (x : M) :
    ψ (φ x) = χ x

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
⊢ ψ (φ x) = χ x

Tactic:
rw [← h.comp_eq, Function.comp_apply]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem Polynomial.exists_dvd_map_of_isAlgebraic [CommRing R] [CommRing S] [NoZeroDivisors S]
    [Algebra R S] [Algebra.IsAlgebraic R S] (f : S[X]) (hf : f ≠ 0) :
    ∃ g : R[X], g ≠ 0 ∧ f ∣ g.map (algebraMap R S) :=
  have ⟨g, ne, eq⟩ := (id ⟨f, hf, by simp⟩ : IsAlgebraic S (AdjoinRoot.root f)).restrictScalars R
  ⟨g, ne, by rwa [aeval_def, IsScalarTower.algebraMap_eq R S, ← eval₂_map, ← aeval_def,
    AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero] at eq⟩

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic R S
f : S[X]
hf : f ≠ 0
⊢ (aeval (AdjoinRoot.root f)) f = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic R S
f : S[X]
hf : f ≠ 0
g : R[X]
ne : g ≠ 0
eq : (aeval (AdjoinRoot.root f)) g = 0
⊢ f ∣ map (algebraMap R S) g

Tactic:
rwa [aeval_def, IsScalarTower.algebraMap_eq R S, ← eval₂_map, ← aeval_def,
AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero] at eq

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
@[reassoc]
lemma pushout.map_comp {X Y Z X' Y' Z' X'' Y'' Z'' : C}
    {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'} {f'' : X'' ⟶ Y''} {g'' : X'' ⟶ Z''}
    (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y') (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'')
    [HasPushout f g] [HasPushout f' g'] [HasPushout f'' g'']
    (e₁ e₂ e₃ e₄) :
    pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ =
      pushout.map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁)
        (by rw [reassoc_of% e₁, e₃, Category.assoc])
        (by rw [reassoc_of% e₂, e₄, Category.assoc])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''

Tactic:
rw [reassoc_of% e₂, e₄, Category.assoc]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ map f g f' g' i₂ i₃ i₁ e₁ e₂ ≫ map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄ = map f g f'' g'' (i₂ ≫ j₂) (i₃ ≫ j₃) (i₁ ≫ j₁) ⋯ ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ f ≫ i₂ ≫ j₂ = (i₁ ≫ j₁) ≫ f''

Tactic:
rw [reassoc_of% e₁, e₃, Category.assoc]

Result:
no goals