harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem containsThenInsertIfNew_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) :
    (m.containsThenInsertIfNew a b).1 = m.containsₘ a

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
      | ⟨i, h⟩ =>
        let bkt := m.1.buckets[i];
        if AssocList.contains a bkt = true then (true, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)
        else
          let size' := m.1.size + 1;
          let buckets' := m.1.buckets.uset i (AssocList.cons a b bkt) h;
          (false, expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)).fst =
    AssocList.contains a
      (match mkIdx m.val.buckets.size ⋯ (hash a) with
      | ⟨i, h⟩ => m.val.buckets[i])

Tactic:
dsimp only [Array.ugetElem_eq_getElem, Array.uset]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (if AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true then
        (true, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)
      else
        (false,
          expandIfNecessary
            ⟨{ size := m.1.size + 1,
                buckets :=
                  m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
                    (AssocList.cons a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
              ⋯⟩)).fst =
    AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat]

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (m.containsThenInsertIfNew a b).fst = m.containsₘ a

Tactic:
rw [containsThenInsertIfNew, containsₘ, bucket]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
      | ⟨i, h⟩ =>
        let bkt := m.1.buckets[i];
        if AssocList.contains a bkt = true then (true, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)
        else
          let size' := m.1.size + 1;
          let buckets' := m.1.buckets.uset i (AssocList.cons a b bkt) h;
          (false, expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)).fst =
    AssocList.contains a
      (match mkIdx m.val.buckets.size ⋯ (hash a) with
      | ⟨i, h⟩ => m.val.buckets[i])

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (if AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true then
        (true, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)
      else
        (false,
          expandIfNecessary
            ⟨{ size := m.1.size + 1,
                buckets :=
                  m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
                    (AssocList.cons a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
              ⋯⟩)).fst =
    AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat]

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_self : finSepDegree F F = 1

Proof state:
F : Type u
inst✝ : Field F
this : Cardinal.mk (Emb F F) = 1
⊢ finSepDegree F F = 1

Tactic:
rw [finSepDegree, Nat.card, this, Cardinal.one_toNat]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
⊢ finSepDegree F F = 1

Tactic:
have : Cardinal.mk (Emb F F) = 1 := le_antisymm
  (Cardinal.le_one_iff_subsingleton.2 AlgHom.subsingleton)
  (Cardinal.one_le_iff_ne_zero.2 <| Cardinal.mk_ne_zero _)

Result:
F : Type u
inst✝ : Field F
this : Cardinal.mk (Emb F F) = 1
⊢ finSepDegree F F = 1
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_zpow (x : ℚ_[p]) : ∀ n : ℤ, (x ^ n).valuation = n * x.valuation
  | (n : ℕ) => by simp
  | .negSucc n => by simp [← neg_mul]; simp [Int.negSucc_eq]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ ↑n).valuation = ↑n * x.valuation

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ Int.negSucc n).valuation = Int.negSucc n * x.valuation

Tactic:
simp [← neg_mul]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ -1 + -↑n = Int.negSucc n ∨ x.valuation = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ -1 + -↑n = Int.negSucc n ∨ x.valuation = 0

Tactic:
simp [Int.negSucc_eq]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem zero_mkRat (n) : mkRat 0 n = 0

Proof state:
n : Nat
⊢ mkRat 0 n = 0

Tactic:
simp [mkRat_def]

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem min_right_comm (a b c : α) : min (min a b) c = min (min a c) b

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ⊓ b ⊓ c = a ⊓ c ⊓ b

Tactic:
rw [min_assoc, min_comm b, min_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_swap_of_ne (a : Vector α n) {i j : Nat} {hi hj} (hp : p < n)
    (hi' : p ≠ i) (hj' : p ≠ j) : (a.swap i j hi hj)[p] = a[p]

Proof state:
α : Type u_1
n p : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
hp : p < n
hi' : p ≠ i
hj' : p ≠ j
⊢ (a.swap i j hi hj)[p] = a[p]

Tactic:
simp_all [getElem_swap]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biproduct.map_eq [HasFiniteBiproducts C] {f g : J → C} {h : ∀ j, f j ⟶ g j} :
    biproduct.map h = ∑ j : J, biproduct.π f j ≫ h j ≫ biproduct.ι g j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
inst✝ : HasFiniteBiproducts C
f g : J → C
h : (j : J) → f j ⟶ g j
⊢ map h = ∑ j : J, π f j ≫ h j ≫ ι g j

Tactic:
ext

Result:
case w.w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
inst✝ : HasFiniteBiproducts C
f g : J → C
h : (j : J) → f j ⟶ g j
j✝¹ j✝ : J
⊢ ι f j✝ ≫ map h ≫ π g j✝¹ = ι f j✝ ≫ (∑ j : J, π f j ≫ h j ≫ ι g j) ≫ π g j✝¹

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
inst✝ : HasFiniteBiproducts C
f g : J → C
h : (j : J) → f j ⟶ g j
⊢ map h = ∑ j : J, π f j ≫ h j ≫ ι g j

Tactic:
classical
ext
simp [biproduct.ι_π, biproduct.ι_π_assoc, comp_sum, sum_comp, comp_dite, dite_comp]

Result:
no goals

Proof state:
case w.w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
inst✝ : HasFiniteBiproducts C
f g : J → C
h : (j : J) → f j ⟶ g j
j✝¹ j✝ : J
⊢ ι f j✝ ≫ map h ≫ π g j✝¹ = ι f j✝ ≫ (∑ j : J, π f j ≫ h j ≫ ι g j) ≫ π g j✝¹

Tactic:
simp [biproduct.ι_π, biproduct.ι_π_assoc, comp_sum, sum_comp, comp_dite, dite_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem _root_.IsClosed.measure_eq_one_iff_eq_univ [OpensMeasurableSpace X] [IsProbabilityMeasure μ]
    (hF : IsClosed F) :
    μ F = 1 ↔ F = univ

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsProbabilityMeasure μ
hF : IsClosed F
⊢ μ F = 1 ↔ F = univ

Tactic:
rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem abs_im_div_norm_le_one (z : ℂ) : |z.im / ‖z‖| ≤ 1 :=
  if hz : z = 0 then by simp [hz, zero_le_one]
  else by simp_rw [_root_.abs_div, abs_norm,
    div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_im_le_norm]

Proof state:
z : ℂ
hz : z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
simp [hz, zero_le_one]

Result:
no goals

Proof state:
z : ℂ
hz : ¬z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
simp_rw [_root_.abs_div, abs_norm,
div_le_iff₀ (norm_pos_iff.mpr hz), one_mul, abs_im_le_norm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux7 (y z : E) :
    ‖(I : 𝕜) • y + 2 • z‖ * ‖(I : 𝕜) • y + 2 • z‖ + ‖(I : 𝕜) • y‖ * ‖(I : 𝕜) • y‖ =
    2 * (‖(I : 𝕜) • y + z‖ * ‖(I : 𝕜) • y + z‖ + ‖z‖ * ‖z‖)

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)

Tactic:
convert parallelogram_identity ((I : 𝕜) • y + z) z using 4 <;> module

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean
theorem Assignment.toAIGAssignment_apply (assign : Assignment) (bit : BVBit) :
    assign.toAIGAssignment bit = (assign.get bit.var).bv.getLsbD bit.idx

Proof state:
assign : Assignment
bit : BVBit
⊢ assign.toAIGAssignment bit = (assign.get bit.var).bv.getLsbD ↑bit.idx

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_eq_getElem?_getD {x : BitVec w} {i : Nat} :
    x.getLsbD i = x[i]?.getD false

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x.getLsbD i = (if h : i < w then some x[i] else none).getD false

Tactic:
split

Result:
case isTrue
w : Nat
x : BitVec w
i : Nat
h✝ : i < w
⊢ x.getLsbD i = (some x[i]).getD false

case isFalse
w : Nat
x : BitVec w
i : Nat
h✝ : ¬i < w
⊢ x.getLsbD i = none.getD false

Proof state:
case isTrue
w : Nat
x : BitVec w
i : Nat
h✝ : i < w
⊢ x.getLsbD i = (some x[i]).getD false

Tactic:
rfl

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x.getLsbD i = x[i]?.getD false

Tactic:
rw [getElem?_def]

Result:
w : Nat
x : BitVec w
i : Nat
⊢ x.getLsbD i = (if h : i < w then some x[i] else none).getD false

Proof state:
case isFalse
w : Nat
x : BitVec w
i : Nat
h✝ : ¬i < w
⊢ x.getLsbD i = none.getD false

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem X_sub_C_dvd_sub_C_eval : X - C a ∣ p - C (p.eval a)

Proof state:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
⊢ X - C a ∣ p - C (eval a p)

Tactic:
rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem norm_mul_coe_unitary (A : E) (U : unitary E) : ‖A * U‖ = ‖A‖ :=
  calc
    _ = ‖((U : E)⋆ * A⋆)⋆‖

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
A : E
U : ↥(unitary E)
⊢ ‖((↑U)⋆ * A⋆)⋆‖ = ‖(↑U)⋆ * A⋆‖

Tactic:
rw [norm_star]

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
A : E
U : ↥(unitary E)
⊢ ‖A * ↑U‖ = ‖((↑U)⋆ * A⋆)⋆‖

Tactic:
simp only [star_star, star_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_empty [BEq α] [Hashable α] {c} : Raw.WFImp (empty c : Raw₀ α β).1 where
  buckets_hash_self

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c : Nat
⊢ IsHashSelf (empty c).val.buckets

Tactic:
simp [Raw.empty, Raw₀.empty]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c : Nat
⊢ DistinctKeys (toListModel (empty c).val.buckets)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c : Nat
⊢ (empty c).val.size = (toListModel (empty c).val.buckets).length

Tactic:
simp [Raw.empty, Raw₀.empty]

Result:
no goals
-- Mathlib/Dynamics/Newton.lean
theorem isNilpotent_iterate_newtonMap_sub_of_isNilpotent (h : IsNilpotent <| aeval x P) (n : ℕ) :
    IsNilpotent <| P.newtonMap^[n] x - x

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
n : ℕ
⊢ IsNilpotent (P.newtonMap^[n] x - x)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [iterate_succ', comp_apply, newtonMap_apply, sub_right_comm]
  refine (Commute.all _ _).isNilpotent_sub ih <| (Commute.all _ _).isNilpotent_mul_right ?_
  simpa using Commute.isNilpotent_add (Commute.all _ _)
    (isNilpotent_aeval_sub_of_isNilpotent_sub P ih) h

Result:
no goals

Proof state:
case zero
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
⊢ IsNilpotent (P.newtonMap^[0] x - x)

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
n : ℕ
ih : IsNilpotent (P.newtonMap^[n] x - x)
⊢ IsNilpotent (P.newtonMap^[n + 1] x - x)

Tactic:
rw [iterate_succ', comp_apply, newtonMap_apply, sub_right_comm]

Result:
case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
n : ℕ
ih : IsNilpotent (P.newtonMap^[n] x - x)
⊢ IsNilpotent
    (P.newtonMap^[n] x - x - Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P)

Proof state:
case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
n : ℕ
ih : IsNilpotent (P.newtonMap^[n] x - x)
⊢ IsNilpotent
    (P.newtonMap^[n] x - x - Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P)

Tactic:
refine (Commute.all _ _).isNilpotent_sub ih <| (Commute.all _ _).isNilpotent_mul_right ?_

Result:
case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
n : ℕ
ih : IsNilpotent (P.newtonMap^[n] x - x)
⊢ IsNilpotent ((aeval (P.newtonMap^[n] x)) P)

Proof state:
case succ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
n : ℕ
ih : IsNilpotent (P.newtonMap^[n] x - x)
⊢ IsNilpotent ((aeval (P.newtonMap^[n] x)) P)

Tactic:
simpa using Commute.isNilpotent_add (Commute.all _ _)
  (isNilpotent_aeval_sub_of_isNilpotent_sub P ih) h

Result:
no goals
-- Mathlib/Data/Nat/PSub.lean
theorem psub_eq_none {m n : ℕ} : psub m n = none ↔ m < n

Proof state:
m n : ℕ
⊢ m.psub n = none ↔ m < n

Tactic:
rcases s : psub m n <;> simp [eq_comm]

Result:
case none
m n : ℕ
s : m.psub n = none
⊢ m < n

case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ n ≤ m

Proof state:
case none
m n : ℕ
s : m.psub n = none
h : m ≥ n
⊢ False

Tactic:
obtain ⟨k, e⟩ := le.dest h

Result:
case none.intro
m n : ℕ
s : m.psub n = none
h : m ≥ n
k : ℕ
e : n + k = m
⊢ False

Proof state:
case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ n ≤ m

Tactic:
rw [← psub_eq_some.1 s]

Result:
case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ n ≤ val✝ + n

Proof state:
case none.intro
m n : ℕ
s : m.psub n = none
h : m ≥ n
k : ℕ
e : n + k = m
⊢ False

Tactic:
injection s.symm.trans (psub_eq_some.2 <| (add_comm _ _).trans e)

Result:
no goals

Proof state:
case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ n ≤ val✝ + n

Tactic:
apply Nat.le_add_left

Result:
no goals

Proof state:
case none
m n : ℕ
s : m.psub n = none
⊢ m < n

Tactic:
refine lt_of_not_ge fun h => ?_

Result:
case none
m n : ℕ
s : m.psub n = none
h : m ≥ n
⊢ False
-- Mathlib/Computability/Primrec.lean
theorem list_tail : Primrec (@List.tail α) :=
  (list_casesOn .id (const []) (snd.comp snd).to₂).of_eq fun l => by cases l <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ (List.casesOn (id l) [] fun b l_1 => (l, b, l_1).2.2) = l.tail

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
lemma unitBackward_unitForward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : C) :
    unitBackward η X ∘ unitForward η X = id

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

Tactic:
simpa [unitForward, unitBackward] using congrArg yonedaEquiv.symm p.snd.app_val

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
⊢ unitBackward η X ∘ unitForward η X = id

Tactic:
refine funext fun p => YonedaCollection.ext ?_ (OverArrows.ext ?_)

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((restrictedYonedaObj η).map (eqToHom ⋯) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((restrictedYonedaObj η).map (eqToHom ⋯) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Tactic:
simp [unitForward, unitBackward]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem finrank [NumberField K] : finrank ℝ (mixedSpace K) = finrank ℚ K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (mixedSpace K) = finrank ℚ K

Tactic:
rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
  card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, Algebra.id.smul_eq_mul,
  mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
  Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (mixedSpace K) = finrank ℚ K

Tactic:
classical
rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
  card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, Algebra.id.smul_eq_mul,
  mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
  Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem mem_measurableCylinders (t : Set (∀ i, α i)) :
    t ∈ measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = cylinder s S

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
t : Set ((i : ι) → α i)
⊢ t ∈ measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = cylinder s S

Tactic:
simp_rw [measurableCylinders, mem_iUnion, exists_prop, mem_singleton_iff]

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem IsChain.directed {f : β → α} {c : Set β} (h : IsChain (f ⁻¹'o r) c) :
    Directed r fun x : { a : β // a ∈ c } => f x :=
  fun ⟨a, ha⟩ ⟨b, hb⟩ =>
    (by_cases fun hab : a = b => by
      simp only [hab, exists_prop, and_self_iff, Subtype.exists]
      exact ⟨b, hb, refl _⟩)
    fun hab => ((h ha hb hab).elim fun h => ⟨⟨b, hb⟩, h, refl _⟩) fun h => ⟨⟨a, ha⟩, refl _, h⟩

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsRefl α r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a ∈ c, r (f b) (f a)

Tactic:
exact ⟨b, hb, refl _⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsRefl α r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ z, r ((fun x => f ↑x) ⟨a, ha⟩) ((fun x => f ↑x) z) ∧ r ((fun x => f ↑x) ⟨b, hb⟩) ((fun x => f ↑x) z)

Tactic:
simp only [hab, exists_prop, and_self_iff, Subtype.exists]

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : IsRefl α r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ a ∈ c, r (f b) (f a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBounds_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} :
    (s ++ t).setIfInBounds i x =
      if i < n then
        s.setIfInBounds i x ++ t
      else
        s ++ t.setIfInBounds (i - n) x

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
⊢ { toArray := if i < s.size then s.setIfInBounds i x ++ t else s ++ t.setIfInBounds (i - s.size) x,
      size_toArray := ⋯ } =
    if i < s.size then { toArray := s.setIfInBounds i x ++ t, size_toArray := ⋯ }
    else { toArray := s ++ t.setIfInBounds (i - s.size) x, size_toArray := ⋯ }

Tactic:
split <;> simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
⊢ ({ toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }).setIfInBounds i x =
    if i < s.size then { toArray := s, size_toArray := ⋯ }.setIfInBounds i x ++ { toArray := t, size_toArray := ⋯ }
    else { toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }.setIfInBounds (i - s.size) x

Tactic:
simp only [mk_append_mk, setIfInBounds_mk, Array.setIfInBounds_append]

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
⊢ { toArray := if i < s.size then s.setIfInBounds i x ++ t else s ++ t.setIfInBounds (i - s.size) x,
      size_toArray := ⋯ } =
    if i < s.size then { toArray := s.setIfInBounds i x ++ t, size_toArray := ⋯ }
    else { toArray := s ++ t.setIfInBounds (i - s.size) x, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
m : Nat
t : Vector α m
i : Nat
x : α
s : Array α
⊢ ({ toArray := s, size_toArray := ⋯ } ++ t).setIfInBounds i x =
    if i < s.size then { toArray := s, size_toArray := ⋯ }.setIfInBounds i x ++ t
    else { toArray := s, size_toArray := ⋯ } ++ t.setIfInBounds (i - s.size) x

Tactic:
rcases t with ⟨t, rfl⟩

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
⊢ ({ toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }).setIfInBounds i x =
    if i < s.size then { toArray := s, size_toArray := ⋯ }.setIfInBounds i x ++ { toArray := t, size_toArray := ⋯ }
    else { toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }.setIfInBounds (i - s.size) x

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
⊢ (s ++ t).setIfInBounds i x = if i < n then s.setIfInBounds i x ++ t else s ++ t.setIfInBounds (i - n) x

Tactic:
rcases s with ⟨s, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
t : Vector α m
i : Nat
x : α
s : Array α
⊢ ({ toArray := s, size_toArray := ⋯ } ++ t).setIfInBounds i x =
    if i < s.size then { toArray := s, size_toArray := ⋯ }.setIfInBounds i x ++ t
    else { toArray := s, size_toArray := ⋯ } ++ t.setIfInBounds (i - s.size) x