harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Composition.lean
theorem comp_stdBasisMatrix_stdBasisMatrix
    [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (i j k l r) :
    comp I J K L R (stdBasisMatrix i j (stdBasisMatrix k l r))
      = stdBasisMatrix (i, k) (j, l) r

Proof state:
case a.mk.mk.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i j' k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j', l')

Tactic:
obtain hj | rfl := ne_or_eq j j'

Result:
case a.mk.mk.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i j' k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j', l')

case a.mk.mk.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i j k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j, l')

Proof state:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
⊢ (comp I J K L R) (stdBasisMatrix i j (stdBasisMatrix k l r)) = stdBasisMatrix (i, k) (j, l) r

Tactic:
ext ⟨i', k'⟩ ⟨j', l'⟩

Result:
case a.mk.mk
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ (comp I J K L R) (stdBasisMatrix i j (stdBasisMatrix k l r)) (i', k') (j', l') =
    stdBasisMatrix (i, k) (j, l) r (i', k') (j', l')
-- Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean
theorem homotopyPToId_eventually_constant {q n : ℕ} (hqn : n < q) :
    ((homotopyPToId X (q + 1)).hom n (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌) =
      (homotopyPToId X q).hom n (n + 1)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ (homotopyPToId X (q + 1)).hom n (n + 1) = (homotopyPToId X q).hom n (n + 1)

Tactic:
simp only [homotopyHσToZero, AlternatingFaceMapComplex.obj_X, Nat.add_eq, Homotopy.trans_hom,
  Homotopy.ofEq_hom, Pi.zero_apply, Homotopy.add_hom, Homotopy.compLeft_hom, add_zero,
  Homotopy.nullHomotopy'_hom, ComplexShape.down_Rel, hσ'_eq_zero hqn (c_mk (n + 1) n rfl),
  dite_eq_ite, ite_self, comp_zero, zero_add, homotopyPToId]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Center.lean
@[simp] lemma zero_mem_center : (0 : M₀) ∈ center M₀ where
  comm _

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ 0 * x✝ = x✝ * 0

Tactic:
rw [zero_mul, mul_zero]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ x✝¹ * 0 * x✝ = x✝¹ * (0 * x✝)

Tactic:
rw [mul_zero, zero_mul, mul_zero]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 * (x✝¹ * x✝) = 0 * x✝¹ * x✝

Tactic:
rw [zero_mul, zero_mul, zero_mul]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ x✝¹ * x✝ * 0 = x✝¹ * (x✝ * 0)

Tactic:
rw [mul_zero, mul_zero, mul_zero]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q

Proof state:
p q : Prop
⊢ (p → q) ∧ (¬p → q) ↔ q

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem lt_sizeof_cons' {b} (a : Lists' α b) (l) :
    SizeOf.sizeOf (⟨b, a⟩ : Lists α) < SizeOf.sizeOf (Lists'.cons' a l)

Proof state:
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l

Tactic:
apply sizeof_pos

Result:
no goals

Proof state:
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ sizeOf ⟨b, a⟩ < sizeOf (a.cons' l)

Tactic:
simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]

Result:
α : Type u_1
b : Bool
a : Lists' α b
l : Lists' α true
⊢ 0 < sizeOf l
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
/-- If `F` preserves the pullback of `f, g`, it also preserves the pullback of `g, f`. -/
lemma preservesPullback_symmetry : PreservesLimit (cospan g f) G where
  preserves {c} hc := ⟨by
    apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).toFun
    apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm
    apply PullbackCone.isLimitOfFlip
    apply (isLimitMapConePullbackConeEquiv _ _).toFun
    · refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_
      · apply PullbackCone.isLimitOfFlip
        apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
        exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
      · dsimp
        infer_instance
    · exact
        (c.π.naturality WalkingCospan.Hom.inr).symm.trans
          (c.π.naturality WalkingCospan.Hom.inl :)⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯)

Tactic:
apply PullbackCone.isLimitOfFlip

Result:
case ht
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯).flip
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail

Proof state:
case cons
α : Type u_1
head✝ : α
l : List α
ih : ∀ (n : Nat), (enumFrom n l).tail = enumFrom (n + 1) l.tail
n : Nat
⊢ (enumFrom n (head✝ :: l)).tail = enumFrom (n + 1) (head✝ :: l).tail

Tactic:
simp [ih, enumFrom_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
n : Nat
⊢ (enumFrom n []).tail = enumFrom (n + 1) [].tail

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (enumFrom n l).tail = enumFrom (n + 1) l.tail

Tactic:
induction l generalizing n with
| nil => simp
| cons _ l ih => simp [ih, enumFrom_cons]

Result:
no goals
-- Mathlib/RingTheory/Localization/Ideal.lean
theorem isPrime_of_isPrime_disjoint (I : Ideal R) (hp : I.IsPrime) (hd : Disjoint (M : Set R) ↑I) :
    (Ideal.map (algebraMap R S) I).IsPrime

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hp : I.IsPrime
hd : Disjoint ↑M ↑I
⊢ (Ideal.map (algebraMap R S) I).IsPrime

Tactic:
rw [isPrime_iff_isPrime_disjoint M S, comap_map_of_isPrime_disjoint M S I hp hd]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hp : I.IsPrime
hd : Disjoint ↑M ↑I
⊢ I.IsPrime ∧ Disjoint ↑M ↑I

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hp : I.IsPrime
hd : Disjoint ↑M ↑I
⊢ I.IsPrime ∧ Disjoint ↑M ↑I

Tactic:
exact ⟨hp, hd⟩

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOn.comp {γ : Type*} (hf : UniformCauchySeqOn F p s) (g : γ → α) :
    UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
γ : Type u_1
hf : UniformCauchySeqOnFilter F p (𝓟 s)
g : γ → α
⊢ UniformCauchySeqOnFilter (fun n => F n ∘ g) p (𝓟 (g ⁻¹' s))

Tactic:
simpa only [UniformCauchySeqOn, comap_principal] using hf.comp g

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
γ : Type u_1
hf : UniformCauchySeqOn F p s
g : γ → α
⊢ UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)

Tactic:
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
γ : Type u_1
hf : UniformCauchySeqOnFilter F p (𝓟 s)
g : γ → α
⊢ UniformCauchySeqOnFilter (fun n => F n ∘ g) p (𝓟 (g ⁻¹' s))
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem range_familyOfBFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o}
    (ho : type r = o) (f : ∀ a < o, α) : range (familyOfBFamily' r ho f) = brange o f

Proof state:
case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ o.brange f → a ∈ range (familyOfBFamily' r ho f)

Tactic:
rintro ⟨i, hi, rfl⟩

Result:
case refine_2.intro.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ f i hi ∈ range (familyOfBFamily' r ho f)

Proof state:
case refine_1.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
b : ι
⊢ familyOfBFamily' r ho f b ∈ o.brange f

Tactic:
apply mem_brange_self

Result:
no goals

Proof state:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
⊢ range (familyOfBFamily' r ho f) = o.brange f

Tactic:
refine Set.ext fun a => ⟨?_, ?_⟩

Result:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ range (familyOfBFamily' r ho f) → a ∈ o.brange f

case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ o.brange f → a ∈ range (familyOfBFamily' r ho f)

Proof state:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ range (familyOfBFamily' r ho f) → a ∈ o.brange f

Tactic:
rintro ⟨b, rfl⟩

Result:
case refine_1.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
b : ι
⊢ familyOfBFamily' r ho f b ∈ o.brange f

Proof state:
case refine_2.intro.intro
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ f i hi ∈ range (familyOfBFamily' r ho f)

Tactic:
exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem map_bracket_eq [LieModule R L M] : map f ⁅I, N⁆ = ⁅I, map f N⁆

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
x : ↥I
n : M
hn : n ∈ N
hm₂ : f n ∈ map f N
⊢ ↑f ⁅x, n⁆ = ⁅↑x, ↑⟨f n, hm₂⟩⁆

Tactic:
simp

Result:
no goals

Proof state:
case e_s.h.mp.intro.intro.intro.intro.mk
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
x : ↥I
n : M
hn : n ∈ N
hm : ↑f ⁅↑x, ↑⟨n, hn⟩⁆ = m
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
simp only [LieModuleHom.coe_toLinearMap, LieModuleHom.map_lie] at hm

Result:
case e_s.h.mp.intro.intro.intro.intro.mk
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
x : ↥I
n : M
hn : n ∈ N
hm : ⁅↑x, f n⁆ = m
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
case e_s.h.mp.intro.intro.intro.intro.mk
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
m : M₂
x : ↥I
n : M
hn : n ∈ N
hm : ⁅↑x, f n⁆ = m
⊢ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
exact ⟨x, ⟨f n, (mem_map (f n)).mpr ⟨n, hn, rfl⟩⟩, hm⟩

Result:
no goals

Proof state:
case e_s.h.mpr.intro.intro.mk.intro.intro
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
x : ↥I
n : M
hn : n ∈ N
hm₂ : f n ∈ map f N
⊢ ⁅↑x, ↑⟨f n, hm₂⟩⁆ ∈ ⇑↑f '' {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
exact ⟨⁅x, n⁆, ⟨x, ⟨n, hn⟩, rfl⟩, by simp⟩

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
@[simp]
lemma lt_sub_iff {n : ℕ} {a b : Fin n} : a < a - b ↔ a < b

Proof state:
case succ.mpr.intro
n : ℕ
a b : Fin (n + 1)
h : a < b
k : ℕ
hk : n + 1 = ↑b + k + 1
this : n + 1 - ↑b = k + 1
⊢ ↑a < (n + 1 - ↑b + ↑a) % (n + 1)

Tactic:
rw [this, Nat.mod_eq_of_lt (hk.ge.trans_lt' ?_), Nat.lt_add_left_iff_pos] <;>
omega

Result:
no goals

Proof state:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ a < a - b ↔ a < b

Tactic:
constructor

Result:
case succ.mp
n : ℕ
a b : Fin (n + 1)
⊢ a < a - b → a < b

case succ.mpr
n : ℕ
a b : Fin (n + 1)
⊢ a < b → a < a - b

Proof state:
case succ.mpr
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a < a - b

Tactic:
rw [lt_iff_val_lt_val, sub_def]

Result:
case succ.mpr
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ↑a < ↑⟨(n + 1 - ↑b + ↑a) % (n + 1), ⋯⟩

Proof state:
case succ.mpr
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ↑a < (n + 1 - ↑b + ↑a) % (n + 1)

Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt b.is_lt

Result:
case succ.mpr.intro
n : ℕ
a b : Fin (n + 1)
h : a < b
k : ℕ
hk : n + 1 = ↑b + k + 1
⊢ ↑a < (n + 1 - ↑b + ↑a) % (n + 1)

Proof state:
case succ.mp
n : ℕ
a b : Fin (n + 1)
⊢ a < a - b → a < b

Tactic:
contrapose!

Result:
case succ.mp
n : ℕ
a b : Fin (n + 1)
⊢ ¬a < b → ¬a < a - b

Proof state:
case succ.mp.intro
n : ℕ
a b : Fin (n + 1)
h : ¬a < b
l : ℕ
hl : ↑a = ↑b + l
⊢ ¬a < a - b

Tactic:
simpa only [Fin.not_lt, le_iff_val_le_val, sub_def, hl, ← Nat.add_assoc, Nat.add_mod_left,
  Nat.mod_eq_of_lt, Nat.sub_add_cancel b.is_lt.le] using
    (le_trans (mod_le _ _) (le_add_left _ _))

Result:
no goals

Proof state:
n : ℕ
a b : Fin (n + 1)
h : a < b
k : ℕ
hk : n + 1 = ↑b + k + 1
⊢ n + 1 - ↑b = k + 1

Tactic:
simp_rw [hk, Nat.add_assoc, Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
case succ.mpr
n : ℕ
a b : Fin (n + 1)
⊢ a < b → a < a - b

Tactic:
intro h

Result:
case succ.mpr
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a < a - b

Proof state:
case succ.mpr.intro
n : ℕ
a b : Fin (n + 1)
h : a < b
k : ℕ
hk : n + 1 = ↑b + k + 1
⊢ ↑a < (n + 1 - ↑b + ↑a) % (n + 1)

Tactic:
have : n + 1 - b = k + 1 := by
  simp_rw [hk, Nat.add_assoc, Nat.add_sub_cancel_left]

Result:
case succ.mpr.intro
n : ℕ
a b : Fin (n + 1)
h : a < b
k : ℕ
hk : n + 1 = ↑b + k + 1
this : n + 1 - ↑b = k + 1
⊢ ↑a < (n + 1 - ↑b + ↑a) % (n + 1)

Proof state:
case succ.mp
n : ℕ
a b : Fin (n + 1)
h : ¬a < b
⊢ ¬a < a - b

Tactic:
obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_le (Fin.not_lt.mp h)

Result:
case succ.mp.intro
n : ℕ
a b : Fin (n + 1)
h : ¬a < b
l : ℕ
hl : ↑a = ↑b + l
⊢ ¬a < a - b

Proof state:
case zero
a b : Fin 0
⊢ a < a - b ↔ a < b

Tactic:
exact a.elim0

Result:
no goals

Proof state:
n : ℕ
a b : Fin n
⊢ a < a - b ↔ a < b

Tactic:
rcases n with - | n

Result:
case zero
a b : Fin 0
⊢ a < a - b ↔ a < b

case succ
n : ℕ
a b : Fin (n + 1)
⊢ a < a - b ↔ a < b

Proof state:
case succ.mpr
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ↑a < ↑⟨(n + 1 - ↑b + ↑a) % (n + 1), ⋯⟩

Tactic:
simp only

Result:
case succ.mpr
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ↑a < (n + 1 - ↑b + ↑a) % (n + 1)

Proof state:
case succ.mp
n : ℕ
a b : Fin (n + 1)
⊢ ¬a < b → ¬a < a - b

Tactic:
intro h

Result:
case succ.mp
n : ℕ
a b : Fin (n + 1)
h : ¬a < b
⊢ ¬a < a - b
-- Mathlib/RingTheory/Frobenius.lean
lemma finite_quotient : _root_.Finite (R ⧸ Q.under R)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
h : Infinite (R ⧸ Ideal.under R Q)
⊢ False

Tactic:
obtain rfl : Q = ⊤ := by simpa [Nat.card_eq_zero_of_infinite, ← Ideal.eq_top_iff_one] using H 0

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
H : φ.IsArithFrobAt ⊤
h : Infinite (R ⧸ Ideal.under R ⊤)
⊢ False

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
⊢ ¬Infinite (R ⧸ Ideal.under R Q)

Tactic:
intro h

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
h : Infinite (R ⧸ Ideal.under R Q)
⊢ False

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
H : φ.IsArithFrobAt ⊤
h : Infinite (R ⧸ Ideal.under R ⊤)
⊢ False

Tactic:
simp only [Ideal.comap_top] at h

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
H : φ.IsArithFrobAt ⊤
h : Infinite (R ⧸ ⊤)
⊢ False

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
⊢ _root_.Finite (R ⧸ Ideal.under R Q)

Tactic:
rw [← not_infinite_iff_finite]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
⊢ ¬Infinite (R ⧸ Ideal.under R Q)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
h : Infinite (R ⧸ Ideal.under R Q)
⊢ Q = ⊤

Tactic:
simpa [Nat.card_eq_zero_of_infinite, ← Ideal.eq_top_iff_one] using H 0

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
H : φ.IsArithFrobAt ⊤
h : Infinite (R ⧸ ⊤)
⊢ False

Tactic:
exact not_finite (R ⧸ (⊤ : Ideal R))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_append {x : BitVec w} {y : BitVec v} :
    (x ++ y).msb = if w = 0 then y.msb else x.msb

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
⊢ 0 < w + v

Tactic:
omega

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Tactic:
by_cases h : w = 0

Result:
case pos
w v : Nat
x : BitVec w
y : BitVec v
h : w = 0
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

case neg
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
⊢ (x ++ y).msb = if w = 0 then y.msb else x.msb

Tactic:
rw [← append_eq, append]

Result:
w v : Nat
x : BitVec w
y : BitVec v
⊢ (x.shiftLeftZeroExtend v ||| setWidth' ⋯ y).msb = if w = 0 then y.msb else x.msb

Proof state:
case pos
v : Nat
y : BitVec v
x : BitVec 0
⊢ (x.msb || decide (0 < 0 + v) && y.getLsbD (0 + v - 1)) = if 0 = 0 then y.msb else x.msb

Tactic:
simp [BitVec.msb, getMsbD]

Result:
no goals

Proof state:
case neg
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Tactic:
have q : 0 < w + v := by omega

Result:
case neg
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
q : 0 < w + v
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Proof state:
case neg
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
q : 0 < w + v
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Tactic:
have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)

Result:
case neg
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
q : 0 < w + v
t : y.getLsbD (w + v - 1) = false
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Proof state:
case pos
w v : Nat
x : BitVec w
y : BitVec v
h : w = 0
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Tactic:
subst h

Result:
case pos
v : Nat
y : BitVec v
x : BitVec 0
⊢ (x.msb || decide (0 < 0 + v) && y.getLsbD (0 + v - 1)) = if 0 = 0 then y.msb else x.msb

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
q : 0 < w + v
⊢ v ≤ w + v - 1

Tactic:
omega

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
y : BitVec v
⊢ (x.shiftLeftZeroExtend v ||| setWidth' ⋯ y).msb = if w = 0 then y.msb else x.msb

Tactic:
simp only [msb_or, msb_shiftLeftZeroExtend, msb_setWidth']

Result:
w v : Nat
x : BitVec w
y : BitVec v
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Proof state:
case neg
w v : Nat
x : BitVec w
y : BitVec v
h : ¬w = 0
q : 0 < w + v
t : y.getLsbD (w + v - 1) = false
⊢ (x.msb || decide (0 < w + v) && y.getLsbD (w + v - 1)) = if w = 0 then y.msb else x.msb

Tactic:
simp [h, q, t, BitVec.msb, getMsbD]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem prod_mul_tprod_subtype_compl [T2Space α] {f : β → α} (hf : Multipliable f) (s : Finset β) :
    (∏ x ∈ s, f x) * ∏' x : { x // x ∉ s }, f x = ∏' x, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : β), f x

Tactic:
rw [← tprod_subtype_mul_tprod_subtype_compl hf s]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = (∏' (x : ↑↑s), f ↑x) * ∏' (x : ↑(↑s)ᶜ), f ↑x

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : ↑(↑s)ᶜ), f ↑x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = (∏' (x : ↑↑s), f ↑x) * ∏' (x : ↑(↑s)ᶜ), f ↑x

Tactic:
simp only [Finset.tprod_subtype', mul_right_inj]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : UniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : ↑(↑s)ᶜ), f ↑x