harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Mul.lean
theorem submatrix_id_mul_left [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*}
    (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → m) (e₂ : n ≃ o) :
    M.submatrix e₁ id * N.submatrix e₂ id = M.submatrix e₁ e₂.symm * N

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
⊢ M.submatrix e₁ id * N.submatrix (⇑e₂) id = M.submatrix e₁ ⇑e₂.symm * N

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
i✝ : l
j✝ : p
⊢ (M.submatrix e₁ id * N.submatrix (⇑e₂) id) i✝ j✝ = (M.submatrix e₁ ⇑e₂.symm * N) i✝ j✝

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
p : Type u_10
M : Matrix m n α
N : Matrix o p α
e₁ : l → m
e₂ : n ≃ o
i✝ : l
j✝ : p
⊢ (M.submatrix e₁ id * N.submatrix (⇑e₂) id) i✝ j✝ = (M.submatrix e₁ ⇑e₂.symm * N) i✝ j✝

Tactic:
simp [mul_apply, ← e₂.bijective.sum_comp]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem prod_eq_top_iff {s : Submonoid M} {t : Submonoid N} : s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
s : Submonoid M
t : Submonoid N
⊢ s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Tactic:
simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← mrange_eq_map, mrange_fst,
  mrange_snd]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem exists_dist_lt_of_hausdorffDist_lt {r : ℝ} (h : x ∈ s) (H : hausdorffDist s t < r)
    (fin : hausdorffEdist s t ≠ ⊤) : ∃ y ∈ t, dist x y < r

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
exact ⟨y, hy, yr⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ hausdorffEdist s t < ENNReal.ofReal r

Tactic:
rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
  ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ y ∈ t, dist x y < r

Tactic:
have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ ∃ y ∈ t, dist x y < r

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : edist x y < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : dist x y < r
⊢ ∃ y ∈ t, dist x y < r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
have : hausdorffEdist s t < ENNReal.ofReal r := by
  rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
    ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
rcases exists_edist_lt_of_hausdorffEdist_lt h this with ⟨y, hy, yr⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
r0 : 0 < r
this : hausdorffEdist s t < ENNReal.ofReal r
y : α
hy : y ∈ t
yr : edist x y < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.inter_right (hs : IsCompact s) (ht : IsClosed t) : IsCompact (s ∩ t)

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
have : x ∈ t := ht.mem_of_nhdsWithin_neBot <|
  hx.mono <| le_trans hstf (le_principal_iff.2 inter_subset_right)

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
this : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f :=
  hs (le_trans hstf (le_principal_iff.2 inter_subset_left))

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
this : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
exact ⟨x, ⟨hsx, this⟩, hx⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
⊢ IsCompact (s ∩ t)

Tactic:
intro f hnf hstf

Result:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
-- Mathlib/GroupTheory/Complement.lean
@[to_additive (attr := deprecated exists_isComplement_right (since := "2024-12-18"))]
lemma exists_right_transversal (H : Subgroup G) (g : G) :
    ∃ S ∈ rightTransversals (H : Set G), g ∈ S

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
by_cases hq : q = Quotient.mk'' g

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ S ∈ rightTransversals ↑H, g ∈ S

Tactic:
refine
  ⟨Set.range (Function.update Quotient.out _ g), range_mem_rightTransversals fun q => ?_,
    Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact Eq.trans (congr_arg _ (Function.update_of_ne hq g Quotient.out)) q.out_eq'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_nonneg_of_le {a b : Int} (h : b ≤ a) : 0 ≤ a - b

Proof state:
a b : Int
h : b ≤ a
⊢ 0 ≤ a - b

Tactic:
have h := Int.add_le_add_right h (-b)

Result:
a b : Int
h✝ : b ≤ a
h : b + -b ≤ a + -b
⊢ 0 ≤ a - b

Proof state:
a b : Int
h✝ : b ≤ a
h : b + -b ≤ a + -b
⊢ 0 ≤ a - b

Tactic:
rwa [Int.add_right_neg] at h

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem succ_descFactorial_succ (n : ℕ) :
    ∀ k : ℕ, (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k
  | 0 => by rw [descFactorial_zero, descFactorial_one, Nat.mul_one]
  | succ k => by
    rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]

Proof state:
n k : ℕ
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ

Tactic:
rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
  Nat.mul_left_comm]

Result:
no goals

Proof state:
n : ℕ
⊢ (n + 1).descFactorial (0 + 1) = (n + 1) * n.descFactorial 0

Tactic:
rw [descFactorial_zero, descFactorial_one, Nat.mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem inv_prodComparison_map_snd [IsIso (prodComparison F A B)] :
    inv (prodComparison F A B) ≫ F.map prod.snd = prod.snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map prod.snd = prod.snd

Tactic:
simp [IsIso.inv_comp_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Opposite.lean
lemma oppositeShiftFunctorAdd'_hom_app :
    (shiftFunctorAdd' (OppositeShift C A) a b c h).hom.app X =
      ((shiftFunctorAdd' C a b c h).inv.app X.unop).op

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ (shiftFunctorAdd' (OppositeShift C A) a b (a + b) ⋯).hom.app X =
    ((shiftFunctorAdd' C a b (a + b) ⋯).inv.app (Opposite.unop X)).op

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, oppositeShiftFunctorAdd_hom_app]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b c : A
h : a + b = c
⊢ (shiftFunctorAdd' (OppositeShift C A) a b c h).hom.app X = ((shiftFunctorAdd' C a b c h).inv.app (Opposite.unop X)).op

Tactic:
subst h

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ (shiftFunctorAdd' (OppositeShift C A) a b (a + b) ⋯).hom.app X =
    ((shiftFunctorAdd' C a b (a + b) ⋯).inv.app (Opposite.unop X)).op
-- Mathlib/Data/Set/Pairwise/Basic.lean
lemma PairwiseDisjoint.eq_or_disjoint
    (h : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) :
    i = j ∨ Disjoint (f i) (f j)

Proof state:
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j

Tactic:
exact h.elim hi hj

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i = j ∨ Disjoint (f i) (f j)

Tactic:
rw [or_iff_not_imp_right]

Result:
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
h : s.PairwiseDisjoint f
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ¬Disjoint (f i) (f j) → i = j
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma assoc (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) :
    π c₁₂ c₃ c ⟨π c₁ c₂ c₁₂ ⟨i₁, i₂⟩, i₃⟩ = π c₁ c₂₃ c ⟨i₁, π c₂ c₃ c₂₃ ⟨i₂, i₃⟩⟩

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))

Tactic:
apply Associative.assoc

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndepOn.id_union {s t : Set M} (hs : LinearIndepOn R id s)
    (ht : LinearIndepOn R id t) (hst : Disjoint (span R s) (span R t)) :
    LinearIndepOn R id (s ∪ t)

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hs : LinearIndepOn R id s
ht : LinearIndepOn R id t
hst : Disjoint (span R s) (span R t)
h : LinearIndependent R (Sum.elim (fun x => id ↑x) fun x => id ↑x)
⊢ LinearIndepOn R id (s ∪ t)

Tactic:
simpa [id_eq] using h.linearIndepOn_id

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hs : LinearIndepOn R id s
ht : LinearIndepOn R id t
hst : Disjoint (span R s) (span R t)
⊢ Disjoint (span R (range fun x => id ↑x)) (span R (range fun x => id ↑x))

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hs : LinearIndepOn R id s
ht : LinearIndepOn R id t
hst : Disjoint (span R s) (span R t)
⊢ LinearIndepOn R id (s ∪ t)

Tactic:
have h := hs.linearIndependent.sum_type ht.linearIndependent (by simpa)

Result:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hs : LinearIndepOn R id s
ht : LinearIndepOn R id t
hst : Disjoint (span R s) (span R t)
h : LinearIndependent R (Sum.elim (fun x => id ↑x) fun x => id ↑x)
⊢ LinearIndepOn R id (s ∪ t)
-- Mathlib/Analysis/Calculus/Deriv/AffineMap.lean
theorem hasDerivAtFilter : HasDerivAtFilter f (f.linear 1) x L

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter 𝕜
x : 𝕜
⊢ HasDerivAtFilter (⇑f) (f.linear 1) x L

Tactic:
rw [f.decomp]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter 𝕜
x : 𝕜
⊢ HasDerivAtFilter (⇑f.linear + fun x => f 0) (f.linear 1) x L

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter 𝕜
x : 𝕜
⊢ HasDerivAtFilter (⇑f.linear + fun x => f 0) (f.linear 1) x L

Tactic:
exact f.linear.hasDerivAtFilter.add_const (f 0)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_sub {x y : BitVec w} :
    (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w)

Proof state:
w : Nat
x y : BitVec w
⊢ (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w)

Tactic:
simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ y.toNat ≤ 2 ^ w

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_neg_one :
    ∀ L : List ℕ, ofDigits (-1 : ℤ) L = (L.map fun n : ℕ => (n : ℤ)).alternatingSum
  | [] => rfl
  | [n] => by simp [ofDigits, List.alternatingSum]
  | a :: b :: t => by
    simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]
    ring

Proof state:
n : ℕ
⊢ ofDigits (-1) [n] = (List.map (fun n => ↑n) [n]).alternatingSum

Tactic:
simp [ofDigits, List.alternatingSum]

Result:
no goals

Proof state:
a b : ℕ
t : List ℕ
⊢ ↑a + -1 * (↑b + -1 * (List.map (fun n => ↑n) t).alternatingSum) = ↑a + -↑b + (List.map (fun n => ↑n) t).alternatingSum

Tactic:
ring

Result:
no goals

Proof state:
a b : ℕ
t : List ℕ
⊢ ofDigits (-1) (a :: b :: t) = (List.map (fun n => ↑n) (a :: b :: t)).alternatingSum

Tactic:
simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]

Result:
a b : ℕ
t : List ℕ
⊢ ↑a + -1 * (↑b + -1 * (List.map (fun n => ↑n) t).alternatingSum) = ↑a + -↑b + (List.map (fun n => ↑n) t).alternatingSum
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem of_d (j : α) : (of X d sq).d (j + 1) j = d j

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j

Tactic:
rw [if_pos rfl, Category.id_comp]

Result:
no goals

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ (of X d sq).d (j + 1) j = d j

Tactic:
dsimp [of]

Result:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
-- Mathlib/GroupTheory/PushoutI.lean
theorem prod_smul_empty (w : NormalWord d) : w.prod • empty = w

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : NormalWord d
⊢ w.prod • empty = w

Tactic:
induction w using consRecOn with
| h_empty => simp
| h_cons i g w _ _ _ _ ih =>
  rw [prod_cons, mul_smul, ih, cons_eq_smul]
| h_base h w _ ih =>
  rw [prod_smul, mul_smul, ih]

Result:
no goals

Proof state:
case h_base
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
a✝ : w.head = 1
ih : w.prod • empty = w
⊢ ((base φ) h • w).prod • empty = (base φ) h • w

Tactic:
rw [prod_smul, mul_smul, ih]

Result:
no goals

Proof state:
case h_empty
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
⊢ empty.prod • empty = empty

Tactic:
simp

Result:
no goals

Proof state:
case h_cons
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw✝ : w.fstIdx ≠ some i
_hgn✝ : g ∈ d.set i
hgr✝ : g ∉ (φ i).range
_hw1✝ : w.head = 1
ih : w.prod • empty = w
⊢ (cons g w hmw✝ hgr✝).prod • empty = cons g w hmw✝ hgr✝

Tactic:
rw [prod_cons, mul_smul, ih, cons_eq_smul]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_span (s : Set R) : zeroLocus (Ideal.span s : Set R) = zeroLocus s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus ↑(Ideal.span s) = zeroLocus s

Tactic:
ext x

Result:
case h
R : Type u
inst✝ : CommSemiring R
s : Set R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus ↑(Ideal.span s) ↔ x ∈ zeroLocus s

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
s : Set R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus ↑(Ideal.span s) ↔ x ∈ zeroLocus s

Tactic:
exact (Submodule.gi R R).gc s x.asIdeal

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma natDegree_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) : (C a * p).natDegree = p.natDegree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).natDegree = p.natDegree

Tactic:
simp [natDegree, degree_C_mul_of_isUnit ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
by rw [H2, Nat.mul_div_cancel_left _ H1]

Proof state:
n m k : Nat
H1 : 0 < n
H2 : m = n * k
⊢ m / n = k

Tactic:
rw [H2, Nat.mul_div_cancel_left _ H1]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_singleton_mul_left_unit {a : α} (h2 : IsUnit a) (x : α) :
    span ({a * x} : Set α) = span {x}

Proof state:
case a
α : Type u
inst✝ : Semiring α
a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * x = a * x

case a
α : Type u
inst✝ : Semiring α
a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * (a * x) = x

Tactic:
exacts [⟨a, rfl⟩, ⟨_, h2.unit.inv_mul_cancel_left x⟩]

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
a : α
h2 : IsUnit a
x : α
⊢ span {a * x} = span {x}

Tactic:
apply le_antisymm <;> rw [span_singleton_le_iff_mem, mem_span_singleton']

Result:
case a
α : Type u
inst✝ : Semiring α
a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * x = a * x

case a
α : Type u
inst✝ : Semiring α
a : α
h2 : IsUnit a
x : α
⊢ ∃ a_1, a_1 * (a * x) = x
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma finsetCongr_piAntidiag_eq_antidiag (n : μ) :
    Equiv.finsetCongr (Equiv.boolArrowEquivProd _) (piAntidiag univ n) = antidiagonal n

Proof state:
case h.mk
μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (∃ a ∈ univ.piAntidiag n, a = (Equiv.boolArrowEquivProd μ).symm (x₁, x₂)) ↔ (x₁, x₂) ∈ antidiagonal n

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
⊢ (Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) = antidiagonal n

Tactic:
ext ⟨x₁, x₂⟩

Result:
case h.mk
μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (x₁, x₂) ∈ (Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) ↔ (x₁, x₂) ∈ antidiagonal n

Proof state:
case h.mk
μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (x₁, x₂) ∈ (Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) ↔ (x₁, x₂) ∈ antidiagonal n

Tactic:
simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk,
  ← Equiv.eq_symm_apply]

Result:
case h.mk
μ : Type u_2
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n x₁ x₂ : μ
⊢ (∃ a ∈ univ.piAntidiag n, a = (Equiv.boolArrowEquivProd μ).symm (x₁, x₂)) ↔ (x₁, x₂) ∈ antidiagonal n
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem mem_normalizer_iff' (x : L) : x ∈ H.normalizer ↔ ∀ y : L, y ∈ H → ⁅y, x⁆ ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅↑x_1, x⁆ ∈ H

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H

Tactic:
rw [Subtype.forall']

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅↑x_1, x⁆ ∈ H