harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem iSup_pow {o : Ordinal} (ho : 0 < o) : ⨆ n : ℕ, o ^ n = o ^ ω

Proof state:
case inr
ho : 0 < 1
⊢ 1 ≤ ⨆ n, 1 ^ ↑n

Tactic:
exact_mod_cast Ordinal.le_iSup _ 0

Result:
no goals

Proof state:
case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ ↑n = 1

Tactic:
refine le_antisymm (Ordinal.iSup_le fun n => by rw [one_opow]) ?_

Result:
case inr
ho : 0 < 1
⊢ 1 ≤ ⨆ n, 1 ^ ↑n

Proof state:
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ ⨆ n, o ^ ↑n = o ^ ω

Tactic:
exact (isNormal_opow ho₁).apply_omega0

Result:
no goals

Proof state:
o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ n, o ^ ↑n = o ^ ω

Tactic:
rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl

Result:
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ ⨆ n, o ^ ↑n = o ^ ω

case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ ↑n = 1 ^ ω

Proof state:
o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ n, o ^ n = o ^ ω

Tactic:
simp_rw [← opow_natCast]

Result:
o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ n, o ^ ↑n = o ^ ω

Proof state:
case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ ↑n = 1 ^ ω

Tactic:
rw [one_opow]

Result:
case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ ↑n = 1

Proof state:
ho : 0 < 1
n : ℕ
⊢ 1 ^ ↑n ≤ 1

Tactic:
rw [one_opow]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_lipschitz (μ : FiniteMeasure Ω) :
    LipschitzWith μ.mass fun f : Ω →ᵇ ℝ≥0 ↦ μ.testAgainstNN f

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -(↑μ.mass * dist f₁ f₂) ≤ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ∧
    ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂

Tactic:
constructor

Result:
case left
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -(↑μ.mass * dist f₁ f₂) ≤ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂)

case right
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_one_add_mul_comm (A : Matrix m n α) (B : Matrix n m α) :
    det (1 + A * B) = det (1 + B * A) :=
  calc
    det (1 + A * B) = det (fromBlocks 1 (-A) B 1)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det

Tactic:
rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 + A * B).det = (fromBlocks 1 (-A) B 1).det

Tactic:
rw [det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem card_eq_card_of_rel {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) :
    card s = card t

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ s.card = t.card

Tactic:
induction h <;> simp [*]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lift_card_sInf_compl_le (s : Set Ordinal.{u}) :
    Cardinal.lift.{u + 1} (sInf sᶜ).card ≤ #s

Proof state:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ ¬x ∉ s

Tactic:
exact not_mem_of_lt_csInf' hx

Result:
no goals

Proof state:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ x ∈ s

Tactic:
rw [← not_not_mem]

Result:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ ¬x ∉ s

Proof state:
s : Set Ordinal.{u}
⊢ Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ #↑s

Tactic:
rw [← mk_Iio_ordinal]

Result:
s : Set Ordinal.{u}
⊢ #↑(Iio (sInf sᶜ)) ≤ #↑s

Proof state:
s : Set Ordinal.{u}
⊢ #↑(Iio (sInf sᶜ)) ≤ #↑s

Tactic:
refine mk_le_mk_of_subset fun x (hx : x < _) ↦ ?_

Result:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ x ∈ s
-- Mathlib/Data/Bool/Basic.lean
theorem and_elim_left : ∀ {a b : Bool}, a && b → a

Proof state:
⊢ ∀ {a b : Bool}, (a && b) = true → a = true

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem comp_open_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs

Result:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : Set (α × α)
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen u
hu₃ : SymmetricRel u
⊢ ∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s

Tactic:
exact ⟨u, hu₁, hu₂, hu₃, (compRel_mono hu₄ hu₄).trans ht₂⟩

Result:
no goals

Proof state:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁

Result:
case intro.intro.intro.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : Set (α × α)
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen u
hu₃ : SymmetricRel u
⊢ ∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
-- Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
theorem mem_nhds_zero {s : Set R} : s ∈ 𝓝 (0 : R) ↔ ∃ γ : Γ₀ˣ, { x | v x < (γ : Γ₀) } ⊆ s

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | v x < ↑γ} ⊆ s

Tactic:
simp only [mem_nhds, sub_zero]

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
theorem div2_bits_eq_tail (n : ℕ) : n.div2.bits = n.bits.tail

Proof state:
n : ℕ
⊢ n.div2.bits = n.bits.tail

Tactic:
induction n using Nat.binaryRec' with
| z => simp
| f _ _ h _ => simp [div2_bit, bits_append_bit _ _ h]

Result:
no goals

Proof state:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : n✝.div2.bits = n✝.bits.tail
⊢ (bit b✝ n✝).div2.bits = (bit b✝ n✝).bits.tail

Tactic:
simp [div2_bit, bits_append_bit _ _ h]

Result:
no goals

Proof state:
case z

⊢ (div2 0).bits = (bits 0).tail

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem transpose_map {f : α → β} {M : Matrix m n α} : Mᵀ.map f = (M.map f)ᵀ

Proof state:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
f : α → β
M : Matrix m n α
⊢ Mᵀ.map f = (M.map f)ᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
f : α → β
M : Matrix m n α
i✝ : n
j✝ : m
⊢ Mᵀ.map f i✝ j✝ = (M.map f)ᵀ i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
f : α → β
M : Matrix m n α
i✝ : n
j✝ : m
⊢ Mᵀ.map f i✝ j✝ = (M.map f)ᵀ i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Extensive.lean
theorem FinitaryExtensive.isVanKampen_finiteCoproducts_Fin [FinitaryExtensive C] {n : ℕ}
    {F : Discrete (Fin n) ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsVanKampenColimit c

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ IsVanKampenColimit c

Tactic:
have : F = Discrete.functor f :=
  Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ IsVanKampenColimit c

Proof state:
case hc
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsColimit (Cofan.mk (∐ fun i => f i.succ) (Sigma.ι fun i => f i.succ))

Tactic:
exact coproductIsCoproduct _

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
let f : Fin n → C := F.obj ∘ Discrete.mk

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ IsVanKampenColimit c
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getKey!_eq_getKey! [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
    m.getKey! a = List.getKey! a (toListModel m.1.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
⊢ m.getKey! a = List.getKey! a (toListModel m.val.buckets)

Tactic:
rw [getKey!_eq_getKey!ₘ, getKey!ₘ_eq_getKey! hm]

Result:
no goals
-- Mathlib/Order/BooleanGenerators.lean
lemma atomistic (hS : BooleanGenerators S) (a : α) (ha : a ≤ sSup S) : ∃ T ⊆ S, a = sSup T

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : a ≤ sSup S
⊢ ∃ T ⊆ S, a = sSup T

Tactic:
obtain ⟨C, hC, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq a

Result:
case intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
⊢ ∃ T ⊆ S, sSup C = sSup T

Proof state:
case h.right.a.a.h.a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
hc : c ∈ C
⊢ T c ⋯ ⋯ ∈ {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}

Tactic:
use c, hc, hC _ hc, (le_sSup hc).trans ha

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
⊢ ‖a‖ ≤ ‖b‖

Tactic:
have h₂ : cfc (id : ℝ → ℝ) a ≤ cfc (fun _ => ‖b‖) a := by
  calc _ = a := by rw [cfc_id ℝ a]
    _ ≤ cfc id b := (cfc_id ℝ b) ▸ hab
    _ ≤ cfc (fun _ => ‖b‖) b := by
        refine cfc_mono fun x hx => ?_
        calc x = ‖x‖ := (Real.norm_of_nonneg (spectrum_nonneg_of_nonneg hb hx)).symm
          _ ≤ ‖b‖ := spectrum.norm_le_norm_of_mem hx
    _ = _ := by rw [cfc_const _ _, cfc_const _ _]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ b✝ : A
ha✝ : autoParam (0 ≤ a✝) _auto✝
hab✝ : a✝ ≤ b✝
a b : Unitization ℂ A
ha : 0 ≤ a
hab : a ≤ b
hb : 0 ≤ b
this✝ : IsSelfAdjoint a
this : IsSelfAdjoint b
h₂ : cfc id a ≤ cfc (fun x => ‖b‖) a
⊢ ‖a‖ ≤ ‖b‖
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma genWeightSpace_chainBotCoeff_sub_one_zsmul_sub :
    genWeightSpace M ((-chainBotCoeff α β - 1 : ℤ) • α + β : L → R) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M ((-↑(chainBotCoeff α β) - 1) • α + ⇑β) = ⊥

Tactic:
rw [sub_eq_add_neg, ← neg_add, neg_smul, ← smul_neg, chainBotCoeff,
  genWeightSpace_chainTopCoeff_add_one_zsmul_add _ _ (by simpa using hα)]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ -α ≠ 0

Tactic:
simpa using hα

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem mem_coclosedCompact_iff :
    s ∈ coclosedCompact X ↔ IsCompact (closure sᶜ)

Proof state:
case refine_1.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : tᶜ ⊆ s
htcl : IsClosed t
htco : IsCompact t
⊢ IsCompact (closure sᶜ)

Tactic:
exact htco.of_isClosed_subset isClosed_closure <|
  closure_minimal (compl_subset_comm.2 hst) htcl

Result:
no goals

Proof state:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsCompact (closure sᶜ)
⊢ ∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ s

Tactic:
exact ⟨closure sᶜ, ⟨isClosed_closure, h⟩, compl_subset_comm.2 subset_closure⟩

Result:
no goals

Proof state:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure sᶜ)

Tactic:
rintro ⟨t, ⟨htcl, htco⟩, hst⟩

Result:
case refine_1.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : tᶜ ⊆ s
htcl : IsClosed t
htco : IsCompact t
⊢ IsCompact (closure sᶜ)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure sᶜ)

Tactic:
refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure sᶜ)

case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsCompact (closure sᶜ)
⊢ ∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ s
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem coordChange_coordChange (e₁ e₂ e₃ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet)
    (h₂ : b ∈ e₂.baseSet) (x : F) :
    e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x

Tactic:
rw [coordChange, e₁.mk_coordChange _ h₁ h₂, ← e₂.coe_coe, e₂.left_inv, coordChange]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑e₁.symm (b, x) ∈ e₂.source
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem restrict_singleton (μ : Measure α) (a : α) : μ.restrict {a} = μ {a} • dirac a

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
by_cases ha : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
have : s ∩ {a} = {a} := by simpa

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
⊢ μ.restrict {a} = μ {a} • dirac a

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
this : s ∩ {a} = ∅
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
simp [*]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
this : s ∩ {a} = {a}
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
simp [*]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Tactic:
have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∉ s
this : s ∩ {a} = ∅
⊢ (μ.restrict {a}) s = (μ {a} • dirac a) s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
a : α
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem map_lift_equalizerComparison [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : C}
    {h : Z ⟶ X} (w : h ≫ f = h ≫ g) :
    G.map (equalizer.lift h w) ≫ equalizerComparison f g G =
      equalizer.lift (G.map h) (by simp only [← G.map_comp, w])

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ (G.map (equalizer.lift h w) ≫ equalizerComparison f g G) ≫ equalizer.ι (G.map f) (G.map g) =
    equalizer.lift (G.map h) ⋯ ≫ equalizer.ι (G.map f) (G.map g)

Tactic:
simp [← G.map_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map (equalizer.lift h w) ≫ equalizerComparison f g G = equalizer.lift (G.map h) ⋯

Tactic:
apply equalizer.hom_ext

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ (G.map (equalizer.lift h w) ≫ equalizerComparison f g G) ≫ equalizer.ι (G.map f) (G.map g) =
    equalizer.lift (G.map h) ⋯ ≫ equalizer.ι (G.map f) (G.map g)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g

Tactic:
simp only [← G.map_comp, w]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.intTrace_eq_of_isLocalization
    (x : B) :
    algebraMap A Aₘ (Algebra.intTrace A B x) = Algebra.intTrace Aₘ Bₘ (algebraMap B Bₘ x)

Proof state:
case neg.a
A : Type u_1
B : Type u_4
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_5
Bₘ : Type u_6
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : NoZeroSMulDivisors A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_4 := FractionRing B
this✝¹¹ : IsIntegralClosure B A L
this✝¹⁰ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝⁹ : Algebra Aₘ K := f.toAlgebra
this✝⁸ : IsScalarTower A Aₘ K
this✝⁷ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝⁶ : Algebra Bₘ L := g.toAlgebra
this✝⁵ : IsScalarTower B Bₘ L
this✝⁴ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra
this✝³ : IsScalarTower Aₘ K L
this✝² : IsScalarTower Aₘ Bₘ L
this✝¹ : IsFractionRing Bₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L
this✝ : FiniteDimensional K L
this : IsIntegralClosure Bₘ Aₘ L
⊢ (algebraMap Aₘ K) ((algebraMap A Aₘ) ((intTrace A B) x)) = (algebraMap Aₘ K) ((intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x))

Tactic:
rw [← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intTrace_fractionRing,
  Algebra.algebraMap_intTrace (L := L), ← IsScalarTower.algebraMap_apply]

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem toZMod_spec : x - (ZMod.cast (toZMod x) : ℤ_[p]) ∈ maximalIdeal ℤ_[p]

Proof state:
case h.e'_5.h.e'_6.intro
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ (↑x.zmodRepr).val = x.zmodRepr

Tactic:
apply mod_eq_of_lt

Result:
case h.e'_5.h.e'_6.intro.h
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ x.zmodRepr < (0 + p').succ

Proof state:
case h.e'_5.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x.zmodRepr).cast = ↑x.zmodRepr

Tactic:
rcases Nat.exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩

Result:
case h.e'_5.h.e'_6.intro
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ (↑x.zmodRepr).cast = ↑x.zmodRepr

Proof state:
case h.e'_5.h.e'_6.intro
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ (↑x.zmodRepr).cast = ↑x.zmodRepr

Tactic:
change ↑((_ : ZMod (0 + p' + 1)).val) = (_ : ℤ_[0 + p' + 1])

Result:
case h.e'_5.h.e'_6.intro
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑(↑x.zmodRepr).val = ↑x.zmodRepr

Proof state:
case h.e'_5.h.e'_6.intro.h
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ x.zmodRepr < (0 + p').succ

Tactic:
simpa only [zero_add] using zmodRepr_lt_p x

Result:
no goals

Proof state:
case h.e'_5.h.e'_6.intro
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑(↑x.zmodRepr).val = ↑x.zmodRepr

Tactic:
rw [Nat.cast_inj]

Result:
case h.e'_5.h.e'_6.intro
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ (↑x.zmodRepr).val = x.zmodRepr

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x - (toZMod x).cast ∈ maximalIdeal ℤ_[p]

Tactic:
convert sub_zmodRepr_mem x using 2

Result:
case h.e'_5.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (toZMod x).cast = ↑x.zmodRepr

Proof state:
case h.e'_5.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (toZMod x).cast = ↑x.zmodRepr

Tactic:
dsimp [toZMod, toZModHom]

Result:
case h.e'_5.h.e'_6
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x.zmodRepr).cast = ↑x.zmodRepr