harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean
theorem exists_opensMeasurableSpace_of_countablySeparated (α : Type*)
    [m : MeasurableSpace α] [CountablySeparated α] :
    ∃ _ : TopologicalSpace α, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Proof state:
α : Type u_5
m : MeasurableSpace α
inst✝ : CountablySeparated α
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩

Result:
case intro.intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝¹ : CountablyGenerated α
left✝ : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝³ : CountablyGenerated α
left✝² : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
τm' : BorelSpace α
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
exact ⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝¹ : CountablyGenerated α
left✝ : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
rcases exists_borelSpace_of_countablyGenerated_of_separatesPoints (m := m') with ⟨τ, _, _, τm'⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_5
m : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝³ : CountablyGenerated α
left✝² : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
τ : TopologicalSpace α
left✝¹ : SecondCountableTopology α
left✝ : T4Space α
τm' : BorelSpace α
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
-- Mathlib/GroupTheory/Abelianization.lean
theorem commutator_centralizer_commutator_le_center :
    ⁅centralizer (commutator G : Set G), centralizer (commutator G)⁆ ≤ Subgroup.center G

Proof state:
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥

Tactic:
refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this

Result:
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), ⊤⁆, centralizer ↑(commutator G)⁆ = ⊥

Proof state:
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅centralizer ↑(commutator G), ⊤⁆, centralizer ↑(commutator G)⁆ = ⊥

Tactic:
rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥

Tactic:
rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]

Result:
G : Type u
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆

Proof state:
G : Type u
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ Subgroup.center G

Tactic:
rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
  Subgroup.commutator_eq_bot_iff_le_centralizer]

Result:
G : Type u
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥

Proof state:
G : Type u
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆

Tactic:
exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥

Tactic:
suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
  refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
  rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]

Result:
G : Type u
inst✝ : Group G
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
    m.contains a = false → getD m a fallback = fallback

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

Tactic:
simp_to_model using List.getValueD_eq_fallback

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem smul_closedBall_one : x • closedBall (1 : E) δ = closedBall x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • closedBall 1 δ = closedBall x δ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_flatMap (l : Vector α n) (f : α → Vector β m) (i : Nat) :
    (l.flatMap f)[i]? =
      if hi : i < n * m then
        haveI : i / m < n

Proof state:
α : Type ?u.322599
n : Nat
β : Type ?u.322604
m : Nat
l : Vector α n
f : α → Vector β m
i : Nat
hi : i < n * m
⊢ i / m < n

Tactic:
rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
m : Nat
l : Vector α n
f : α → Vector β m
i : Nat
⊢ (l.flatMap f)[i]? = if hi : i < n * m then some (f l[i / m])[i % m] else none

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m

Proof state:
n m k : Nat
⊢ n * m * k = n * k * m

Tactic:
rw [Nat.mul_assoc, Nat.mul_comm m, ← Nat.mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_coe_center_sq (z w : ℍ) (r : ℝ) : dist (z : ℂ) (w.center r) ^ 2 =
    2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Proof state:
z w : ℍ
r : ℝ
⊢ 2 * z.im * w.im ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Tactic:
have H : 2 * z.im * w.im ≠ 0 := by positivity

Result:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Proof state:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ (z.re - w.re) ^ 2 + (z.im ^ 2 - 2 * z.im * (w.im * Real.cosh r) + w.im ^ 2 * (Real.sinh r ^ 2 + 1)) =
    (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2 - 2 * z.im * w.im * Real.cosh r + w.im ^ 2 * Real.sinh r ^ 2

Tactic:
ring

Result:
no goals

Proof state:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Tactic:
simp only [Complex.dist_eq, Complex.sq_norm, normSq_apply, coe_re, coe_im, center_re, center_im,
  cosh_dist', mul_div_cancel₀ _ H, sub_sq z.im, mul_pow, Real.cosh_sq, sub_re, sub_im, mul_sub, ←
  sq]

Result:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ (z.re - w.re) ^ 2 + (z.im ^ 2 - 2 * z.im * (w.im * Real.cosh r) + w.im ^ 2 * (Real.sinh r ^ 2 + 1)) =
    (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2 - 2 * z.im * w.im * Real.cosh r + w.im ^ 2 * Real.sinh r ^ 2
-- Mathlib/FieldTheory/Normal/Defs.lean
theorem AlgEquiv.restrictNormalHom_comp_apply (K₁ K₂ : Type*) {F K₃ : Type*}
    [Field F] [Field K₁] [Field K₂] [Field K₃]
    [Algebra F K₁] [Algebra F K₂] [Algebra F K₃] [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃]
    [IsScalarTower F K₁ K₃] [IsScalarTower F K₁ K₂] [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃]
    [Normal F K₁] [Normal F K₂] (f : K₃ ≃ₐ[F] K₃) :
    AlgEquiv.restrictNormalHom K₁ f =
    (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂ f)

Proof state:
K₁ : Type u_6
K₂ : Type u_7
F : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : K₃ ≃ₐ[F] K₃
⊢ (AlgEquiv.restrictNormalHom K₁) f = (AlgEquiv.restrictNormalHom K₁) ((AlgEquiv.restrictNormalHom K₂) f)

Tactic:
rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem or_as_aig : ∀ (a b : Bool), (!(!a && !b)) = (a || b)

Proof state:
⊢ ∀ (a b : Bool), (!(!a && !b)) = (a || b)

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem normalize_lcm (s : Multiset α) : normalize s.lcm = s.lcm :=
  Multiset.induction_on s (by simp) fun a s _ ↦ by simp

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ normalize (lcm 0) = lcm 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : normalize s.lcm = s.lcm
⊢ normalize (a ::ₘ s).lcm = (a ::ₘ s).lcm

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem quotient_norm_add_le (S : AddSubgroup M) (x y : M ⧸ S) : ‖x + y‖ ≤ ‖x‖ + ‖y‖

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
⊢ ‖↑x + ↑y‖ ≤ ‖↑x‖ + ‖↑y‖

Tactic:
simp only [← mk'_apply, ← map_add, quotient_norm_mk_eq, sInf_image']

Result:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
⊢ ⨅ a, ‖x + y + ↑a‖ ≤ (⨅ a, ‖x + ↑a‖) + ⨅ a, ‖y + ↑a‖

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ‖x + y + ↑(a + b)‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖

Tactic:
exact (congr_arg norm (add_add_add_comm _ _ _ _)).trans_le (norm_add_le _ _)

Result:
no goals

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
⊢ ⨅ a, ‖x + y + ↑a‖ ≤ (⨅ a, ‖x + ↑a‖) + ⨅ a, ‖y + ↑a‖

Tactic:
refine le_ciInf_add_ciInf fun a b ↦ ?_

Result:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ⨅ a, ‖x + y + ↑a‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ⨅ a, ‖x + y + ↑a‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖

Tactic:
refine ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ norm_nonneg _⟩ (a + b) ?_

Result:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ‖x + y + ↑(a + b)‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
rcases And.intro (mk_surjective x) (mk_surjective y) with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩

Result:
case intro.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M
⊢ ‖↑x + ↑y‖ ≤ ‖↑x‖ + ‖↑y‖
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap_comap_eq_relfinrank_inf (f : L →ₐ[F] E) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A (B ⊓ f.fieldRange)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))

Result:
no goals
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem comp_gen : (((𝓤 α).lift' gen).lift' fun s => compRel s s) ≤ (𝓤 α).lift' gen :=
  calc
    (((𝓤 α).lift' gen).lift' fun s => compRel s s) =
        (𝓤 α).lift' fun s => compRel (gen s) (gen s)

Proof state:
case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s => s ○ s

Tactic:
exact monotone_id.compRel monotone_id

Result:
no goals

Proof state:
case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

Tactic:
exact monotone_gen

Result:
no goals

Proof state:
case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

Tactic:
exact monotone_gen

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s => gen (s ○ s)) = ((𝓤 α).lift' fun s => s ○ s).lift' gen

Tactic:
rw [lift'_lift'_assoc]

Result:
case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s => s ○ s

case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ (((𝓤 α).lift' gen).lift' fun s => s ○ s) = (𝓤 α).lift' fun s => gen s ○ gen s

Tactic:
rw [lift'_lift'_assoc]

Result:
case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s => s ○ s

Proof state:
case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s => s ○ s

Tactic:
exact monotone_id.compRel monotone_id

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp) natAbs_nsmul_eq_zero]
lemma pow_natAbs_eq_one : a ^ n.natAbs = 1 ↔ a ^ n = 1

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ n.natAbs = 1 ↔ a ^ n = 1

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Algebra/Star/CentroidHom.lean
theorem star_centerToCentroidCenter (z : NonUnitalStarSubsemiring.center α) :
    star (centerToCentroidCenter z) =
      (centerToCentroidCenter (star z : NonUnitalStarSubsemiring.center α))

Proof state:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
⊢ star (centerToCentroidCenter z) = centerToCentroidCenter (star z)

Tactic:
ext a

Result:
case a.h
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ ↑(star (centerToCentroidCenter z)) a = ↑(centerToCentroidCenter (star z)) a

Proof state:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ a * ↑(star z) = ↑(star z) * a

Tactic:
rw [(star z).property.comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (↑z * star a) = star (star a) * ↑(star z)

Tactic:
simp only [star_mul, star_star, StarMemClass.coe_star]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (star a) * ↑(star z) = a * ↑(star z)

Tactic:
rw [star_star]

Result:
no goals

Proof state:
case a.h
α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ ↑(star (centerToCentroidCenter z)) a = ↑(centerToCentroidCenter (star z)) a

Tactic:
calc
    (star (centerToCentroidCenter z)) a = star (z * star a) := rfl
    _ = star (star a) * star z := by simp only [star_mul, star_star, StarMemClass.coe_star]
    _ = a * star z := by rw [star_star]
    _ = (star z) * a := by rw [(star z).property.comm]
    _ = (centerToCentroidCenter ((star z) : NonUnitalStarSubsemiring.center α)) a := rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Folds.lean
theorem iunfoldr_getLsbD {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
  getLsbD (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
i : Fin w
ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)
⊢ (iunfoldr f (state 0)).snd.getLsbD ↑i = (f i (state ↑i)).snd

Tactic:
exact (iunfoldr_getLsbD' state ind).1 i

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem univ_sigma_preimage_mk (s : Set (Σ i, α i)) :
    (univ : Set ι).sigma (fun i ↦ Sigma.mk i ⁻¹' s) = s :=
  ext <| by simp

Proof state:
ι : Type u_1
α : ι → Type u_3
s : Set ((i : ι) × α i)
⊢ ∀ (x : (i : ι) × α i), (x ∈ univ.sigma fun i => Sigma.mk i ⁻¹' s) ↔ x ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem to_map_eq_zero_iff {x : R} (hM : M ≤ nonZeroDivisors R) : algebraMap R S x = 0 ↔ x = 0

Proof state:
case mpr
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ (algebraMap R S) x = (algebraMap R S) 0

Tactic:
rw [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ (algebraMap R S) x = 0 ↔ x = 0

Tactic:
rw [← (algebraMap R S).map_zero]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ (algebraMap R S) x = (algebraMap R S) 0 ↔ x = 0

Proof state:
case mp.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : (algebraMap R S) x = (algebraMap R S) 0
c : ↥M
hc : ↑c * x = ↑c * 0
⊢ x = 0

Tactic:
rw [mul_zero, mul_comm] at hc

Result:
case mp.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : (algebraMap R S) x = (algebraMap R S) 0
c : ↥M
hc : x * ↑c = 0
⊢ x = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ (algebraMap R S) x = (algebraMap R S) 0 ↔ x = 0

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : (algebraMap R S) x = (algebraMap R S) 0
⊢ x = 0

case mpr
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ (algebraMap R S) x = (algebraMap R S) 0

Proof state:
case mp.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : (algebraMap R S) x = (algebraMap R S) 0
c : ↥M
hc : x * ↑c = 0
⊢ x = 0

Tactic:
exact hM c.2 x hc

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : (algebraMap R S) x = (algebraMap R S) 0
⊢ x = 0

Tactic:
obtain ⟨c, hc⟩ := (eq_iff_exists M S).mp h

Result:
case mp.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : (algebraMap R S) x = (algebraMap R S) 0
c : ↥M
hc : ↑c * x = ↑c * 0
⊢ x = 0
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem IsConjRoot.exists_algEquiv [Normal K L] {x y: L} (h : IsConjRoot K x y) :
    ∃ σ : L ≃ₐ[K] L, σ y = x

Proof state:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
h : IsConjRoot K x y
⊢ ∃ σ, σ y = x

Tactic:
obtain ⟨σ, hσ⟩ :=
  exists_algHom_of_splits_of_aeval (normal_iff.mp inferInstance) (h ▸ minpoly.aeval K x)

Result:
case intro
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
h : IsConjRoot K x y
σ : L →ₐ[K] L
hσ : σ y = x
⊢ ∃ σ, σ y = x

Proof state:
case intro
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
h : IsConjRoot K x y
σ : L →ₐ[K] L
hσ : σ y = x
⊢ ∃ σ, σ y = x

Tactic:
exact ⟨AlgEquiv.ofBijective σ (σ.normal_bijective _ _ _), hσ⟩

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem ascPochhammer_smeval_eq_eval [Semiring R] (r : R) (n : ℕ) :
    (ascPochhammer ℕ n).smeval r = (ascPochhammer R n).eval r

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (ascPochhammer ℕ n).smeval r = eval r (ascPochhammer R n)

Tactic:
rw [eval_eq_smeval, ascPochhammer_smeval_cast R]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic.dvd_X_pow_sub_one (n : ℕ) (R : Type*) [Ring R] :
    cyclotomic n R ∣ X ^ n - 1

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n R ∣ X ^ n - 1

Tactic:
suffices cyclotomic n ℤ ∣ X ^ n - 1 by
  simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
    Polynomial.map_X] using map_dvd (Int.castRingHom R) this

Result:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n ℤ ∣ X ^ n - 1

Proof state:
case inl
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 ℤ ∣ X ^ 0 - 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n ℤ ∣ X ^ n - 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 ℤ ∣ X ^ 0 - 1

case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ X ^ n - 1

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
this : cyclotomic n ℤ ∣ X ^ n - 1
⊢ cyclotomic n R ∣ X ^ n - 1

Tactic:
simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
  Polynomial.map_X] using map_dvd (Int.castRingHom R) this

Result:
no goals

Proof state:
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ X ^ n - 1

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one hn]

Result:
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ ∏ i ∈ n.divisors, cyclotomic i ℤ

Proof state:
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ ∏ i ∈ n.divisors, cyclotomic i ℤ

Tactic:
exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
@[simp]
lemma extClass_comp_assoc {Y : C} {n : ℕ} (γ : Ext S.X₂ Y n) {n' : ℕ} {h : 1 + n = n'} :
    hS.extClass.comp ((Ext.mk₀ S.f).comp γ (zero_add n)) h = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + 0 + n = n'

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + n = n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + 0 = 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ hS.extClass.comp ((Ext.mk₀ S.f).comp γ ⋯) h = 0

Tactic:
rw [← Ext.comp_assoc (a₁₂ := 1) _ _ _ (by omega) (by omega) (by omega),
  extClass_comp, Ext.zero_comp]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem toNNReal_add {r₁ r₂ : ℝ≥0∞} (h₁ : r₁ ≠ ∞) (h₂ : r₂ ≠ ∞) :
    (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal

Proof state:
r₁ r₂ : ℝ≥0∞
h₁ : r₁ ≠ ⊤
h₂ : r₂ ≠ ⊤
⊢ (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal

Tactic:
lift r₁ to ℝ≥0 using h₁

Result:
case intro
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ⊤
r₁ : ℝ≥0
⊢ (↑r₁ + r₂).toNNReal = (↑r₁).toNNReal + r₂.toNNReal

Proof state:
case intro.intro
r₁ r₂ : ℝ≥0
⊢ (↑r₁ + ↑r₂).toNNReal = (↑r₁).toNNReal + (↑r₂).toNNReal

Tactic:
rfl

Result:
no goals

Proof state:
case intro
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ⊤
r₁ : ℝ≥0
⊢ (↑r₁ + r₂).toNNReal = (↑r₁).toNNReal + r₂.toNNReal

Tactic:
lift r₂ to ℝ≥0 using h₂

Result:
case intro.intro
r₁ r₂ : ℝ≥0
⊢ (↑r₁ + ↑r₂).toNNReal = (↑r₁).toNNReal + (↑r₂).toNNReal