harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α)
    (h : Raw.WFImp m.1) (h' : m.containsₘ a = true) : Raw.WFImp (m.eraseₘaux a).1 where
  buckets_hash_self := isHashSelf_eraseₘaux m a h
  size_eq

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : m.containsₘ a = true
⊢ ⟨{ size := m.val.size - 1, buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.erase a l }, ⋯⟩.val.size =
    if true = true then (toListModel m.val.buckets).length - 1 else (toListModel m.val.buckets).length

Tactic:
simp [h.size_eq]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : m.containsₘ a = true
⊢ (m.eraseₘaux a).val.size = (toListModel (m.eraseₘaux a).val.buckets).length

Tactic:
rw [(toListModel_eraseₘaux m a h).length_eq, eraseₘaux, length_eraseKey,
  ← containsₘ_eq_containsKey h, h']

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : m.containsₘ a = true
⊢ ⟨{ size := m.val.size - 1, buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.erase a l }, ⋯⟩.val.size =
    if true = true then (toListModel m.val.buckets).length - 1 else (toListModel m.val.buckets).length
-- Mathlib/Data/List/Sigma.lean
theorem sizeOf_kerase [SizeOf (Sigma β)] (x : α)
    (xs : List (Sigma β)) : SizeOf.sizeOf (List.kerase x xs) ≤ SizeOf.sizeOf xs

Proof state:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
xs : List (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

Tactic:
induction' xs with y ys

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x []) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) []

case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x ys) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) ys
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x (y :: ys)) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (y :: ys)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
xs : List (Sigma β)
⊢ sizeOf (kerase x xs) ≤ sizeOf xs

Tactic:
simp only [SizeOf.sizeOf, _sizeOf_1]

Result:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
xs : List (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x []) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x ys) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) ys
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x (y :: ys)) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (y :: ys)

Tactic:
by_cases x = y.1 <;> simp [*]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNF_of_le_one {b o : Ordinal} (hb : b ≤ 1) (ho : o ≠ 0) : CNF b o = [(0, o)]

Proof state:
b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]

Tactic:
rcases le_one_iff.1 hb with (rfl | rfl)

Result:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 ≤ 1
⊢ CNF 0 o = [(0, o)]

case inr
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 1 ≤ 1
⊢ CNF 1 o = [(0, o)]

Proof state:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 ≤ 1
⊢ CNF 0 o = [(0, o)]

case inr
o : Ordinal.{u_1}
ho : o ≠ 0
hb : 1 ≤ 1
⊢ CNF 1 o = [(0, o)]

Tactic:
exacts [zero_CNF ho, one_CNF ho]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem getElem?_unattach {p : α → Prop} {l : Array { x // p x }} (i : Nat) :
    l.unattach[i]? = l[i]?.map Subtype.val

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
i : Nat
⊢ l.unattach[i]? = Option.map Subtype.val l[i]?

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive add_abs_nonneg] lemma one_le_mul_mabs (a : α) : 1 ≤ a * |a|ₘ

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ 1 ≤ a * mabs a

Tactic:
rw [← mul_inv_cancel a]

Result:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a * a⁻¹ ≤ a * mabs a

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a * a⁻¹ ≤ a * mabs a

Tactic:
exact mul_le_mul_left' (inv_le_mabs a) _

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem leadingCoeff_sub {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R}
    (hxy : x.orderTop < y.orderTop) : (x - y).leadingCoeff = x.leadingCoeff

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
⊢ (x - y).leadingCoeff = x.leadingCoeff

Tactic:
rw [sub_eq_add_neg]

Result:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff

Tactic:
exact leadingCoeff_add_eq_left hxy

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff

Tactic:
rw [← orderTop_neg (x := y)] at hxy

Result:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff
-- Mathlib/CategoryTheory/Localization/Construction.lean
theorem fac : W.Q ⋙ lift G hG = G :=
  Functor.ext (fun _ => rfl)
    (by
      intro X Y f
      simp only [Functor.comp_map, eqToHom_refl, comp_id, id_comp]
      dsimp [MorphismProperty.Q, Quot.liftOn, Quotient.functor]
      rw [composePath_toPath])

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ (lift G hG).map (W.Q.map f) = G.map f

Tactic:
dsimp [MorphismProperty.Q, Quot.liftOn, Quotient.functor]

Result:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ composePath (G.map f).toPath = G.map f

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ (W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
simp only [Functor.comp_map, eqToHom_refl, comp_id, id_comp]

Result:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ (lift G hG).map (W.Q.map f) = G.map f

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (X Y : C) (f : X ⟶ Y), (W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
intro X Y f

Result:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ (W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ composePath (G.map f).toPath = G.map f

Tactic:
rw [composePath_toPath]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem glued_cover_cocycle_fst (x y z : 𝒰.J) :
    gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y ≫ pullback.fst _ _ =
      pullback.fst _ _

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))

Tactic:
apply pullback.hom_ext <;> simp

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
/-- If `i + 1 < j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i` and `i + 1`, respectively. -/
lemma mkOfSucc_δ_lt {n : ℕ} {i : Fin n} {j : Fin (n + 2)}
    (h : i.succ.castSucc < j) :
    mkOfSucc i ≫ δ j = mkOfSucc i.castSucc

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i => i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i => i) ⟨1, ⋯⟩))

Tactic:
simp [δ, Fin.succAbove_of_castSucc_lt _ _ h]

Result:
no goals

Proof state:
case a.h.h.h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) x)

Tactic:
fin_cases x

Result:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i => i) ⟨0, ⋯⟩))

case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i => i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i => i) ⟨1, ⋯⟩))

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
simp [δ, Fin.succAbove_of_castSucc_lt _ _ (Nat.lt_trans _ h)]

Result:
no goals

Proof state:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ mkOfSucc i ≫ δ j = mkOfSucc i.castSucc

Tactic:
ext x

Result:
case a.h.h.h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) x)
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
theorem rightOp {W : MorphismProperty C} {L : Cᵒᵖ ⥤ D} (h : W.op.IsInvertedBy L) :
    W.IsInvertedBy L.rightOp := fun X Y f hf => by
  haveI := h f.op hf
  dsimp
  infer_instance

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.rightOp.map f)

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.map f.op).op

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.map f.op).op

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.rightOp.map f)

Tactic:
haveI := h f.op hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.rightOp.map f)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem satAssignment_inr :
    (cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, x.isLt⟩, assign1⟧

Proof state:
aig : AIG Nat
assign1 : Nat → Bool
x : Fin aig.decls.size
⊢ cnfSatAssignment aig assign1 (Sum.inr x) = ⟦assign1, { aig := aig, ref := { gate := ↑x, hgate := ⋯ } }⟧

Tactic:
simp [cnfSatAssignment, mixAssigns]

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
theorem iff_algebraMap_injective [IsDomain A] :
    NoZeroSMulDivisors R A ↔ Injective (algebraMap R A)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain A
⊢ NoZeroSMulDivisors R A ↔ Injective ⇑(algebraMap R A)

Tactic:
rw [iff_faithfulSMul]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain A
⊢ FaithfulSMul R A ↔ Injective ⇑(algebraMap R A)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain A
⊢ FaithfulSMul R A ↔ Injective ⇑(algebraMap R A)

Tactic:
exact faithfulSMul_iff_algebraMap_injective R A

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isShortNF_of_char_three : W.c₆ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.c₆ = 0

Tactic:
rw [c₆_of_isShortNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -864 * W.a₆ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -864 * W.a₆ = 0

Tactic:
linear_combination -288 * W.a₆ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem eval_nil : (lc : LinearCombo).eval .nil = lc.const

Proof state:
lc : LinearCombo
⊢ lc.eval [] = lc.const

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma genWeightSpace_neg_zsmul_add_ne_bot {n : ℕ} (hn : n ≤ chainBotCoeff α β) :
    genWeightSpace M ((-n : ℤ) • α + β : 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
n : ℕ
hn : n ≤ chainBotCoeff α β
⊢ genWeightSpace M (-↑n • α + ⇑β) ≠ ⊥

Tactic:
apply genWeightSpace_zsmul_add_ne_bot α β <;> omega

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castPred_lt_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) :
    castPred i hi < j ↔ i < castSucc j

Proof state:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi < j ↔ i < j.castSucc

Tactic:
rw [← castSucc_lt_castSucc_iff, castSucc_castPred]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean
theorem isPartition_splitCenter (I : Box ι) : IsPartition (splitCenter I) := fun x hx => by
  simp [hx]

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
x : ι → ℝ
hx : x ∈ I
⊢ ∃ J ∈ splitCenter I, x ∈ J

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/RingTheory/PiTensorProduct.lean
theorem constantBaseRingEquiv_tprod (x : ι → R) :
    constantBaseRingEquiv ι R (tprod R x) = ∏ i, x i

Proof state:
ι : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
x : ι → R
⊢ (constantBaseRingEquiv ι R) ((tprod R) x) = ∏ i : ι, x i

Tactic:
simp [constantBaseRingEquiv]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem IsSemisimpleModule.of_sSup_simples_eq_top
    (h : sSup { m : Submodule R M | IsSimpleModule R m } = ⊤) : IsSemisimpleModule R M :=
  complementedLattice_of_sSup_atoms_eq_top (by simp_rw [← h, isSimpleModule_iff_isAtom])

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : sSup {m | IsSimpleModule R ↥m} = ⊤
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
simp_rw [← h, isSimpleModule_iff_isAtom]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem ne_neg_self_iff {θ : Angle} : θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ π

Proof state:
θ : Angle
⊢ θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
rw [← not_or, ← eq_neg_self_iff.not]

Result:
no goals
-- Mathlib/Logic/Embedding/Set.lean
theorem Function.Embedding.sigmaSet_range {s : ι → Set α}
    (h : Pairwise (Disjoint on s)) : Set.range (Function.Embedding.sigmaSet h) = ⋃ i, s i

Proof state:
α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ range ⇑(sigmaSet h) = ⋃ i, s i

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem funMap_unify_equiv {n : ℕ} (F : L.Functions n) (x : Fin n → Σˣ f) (i j : ι)
    (hi : i ∈ upperBounds (range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (range (Sigma.fst ∘ x))) :
    Structure.Sigma.mk f i (funMap F (unify f x i hi)) ≈ .mk f j (funMap F (unify f x j hj))

Proof state:
case intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ Structure.Sigma.mk f i (funMap F (unify f x i hi)) ≈ Structure.Sigma.mk f j (funMap F (unify f x j hj))

Tactic:
refine ⟨k, ik, jk, ?_⟩

Result:
case intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ (f i k ik) (funMap F (unify f x i hi)) = (f j k jk) (funMap F (unify f x j hj))

Proof state:
case intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
n : ℕ
F : L.Functions n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ (f i k ik) (funMap F (unify f x i hi)) = (f j k jk) (funMap F (unify f x j hj))

Tactic:
rw [(f i k ik).map_fun, (f j k jk).map_fun, comp_unify, comp_unify]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem interleave_even_odd (s₁ : Stream' α) : even s₁ ⋈ odd s₁ = s₁ :=
  eq_of_bisim (fun s' s => s' = even s ⋈ odd s)
    (fun s' s (h : s' = even s ⋈ odd s) => by
      rw [h]; constructor
      · rfl
      · simp [odd_eq, odd_eq, tail_interleave, tail_even])
    rfl

Proof state:
case left
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun s' s => s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
constructor

Result:
case left
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head

case right
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (fun s' s => s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Proof state:
case right
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (fun s' s => s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
simp [odd_eq, odd_eq, tail_interleave, tail_even]

Result:
no goals

Proof state:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ s'.head = s.head ∧ (fun s' s => s' = s.even ⋈ s.odd) s'.tail s.tail

Tactic:
rw [h]

Result:
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head ∧ (fun s' s => s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[gcongr] lemma shatterer_mono (h : 𝒜 ⊆ ℬ) : 𝒜.shatterer ⊆ ℬ.shatterer :=
  fun _ ↦ by simpa using Shatters.mono_left h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h : 𝒜 ⊆ ℬ
x✝ : Finset α
⊢ x✝ ∈ 𝒜.shatterer → x✝ ∈ ℬ.shatterer

Tactic:
simpa using Shatters.mono_left h

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem nnnorm_inl (r : R) : ‖(inl r : tsze R M)‖₊ = ‖r‖₊

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
r : R
⊢ ‖inl r‖₊ = ‖r‖₊

Tactic:
simp [nnnorm_def]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Algebra.lean
theorem smul_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R)
    (x : AdicCauchySequence I M) :
    r.val n • Submodule.Quotient.mk (p := (I ^ m • ⊤ : Submodule R M)) (x.val n) =
      r.val m • Submodule.Quotient.mk (p := (I ^ m • ⊤ : Submodule R M)) (x.val m)

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ ↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)

Tactic:
rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
  AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
  Submodule.Quotient.mk_smul]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem divided_by_X_pow_order_of_X_eq_one : divided_by_X_pow_order X_ne_zero = (1 : R⟦X⟧)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X * divided_by_X_pow_order ⋯ = X

Tactic:
simpa using self_eq_X_pow_order_mul_divided_by_X_pow_order (@X_ne_zero R _ _)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ divided_by_X_pow_order ⋯ = 1

Tactic:
rw [← mul_eq_left₀ X_ne_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X * divided_by_X_pow_order ⋯ = X
-- Mathlib/Logic/Equiv/Set.lean
theorem sumCompl_symm_apply_of_mem {α : Type u} {s : Set α} [DecidablePred (· ∈ s)] {x : α}
    (hx : x ∈ s) : (Equiv.Set.sumCompl s).symm x = Sum.inl ⟨x, hx⟩

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
⊢ (Set.sumCompl s).symm x = Sum.inl ⟨x, hx⟩

Tactic:
simp [Equiv.Set.sumCompl, Equiv.Set.univ, union_apply_left, hx]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem map_id : v.map id = v :=
  ext fun i hi => by rw [map_apply v measurable_id hi, Set.preimage_id]

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(v.map id) i = ↑v i

Tactic:
rw [map_apply v measurable_id hi, Set.preimage_id]

Result:
no goals