harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Comma.lean
theorem projectQuotient_factors [HasFiniteColimits C] [PreservesFiniteColimits S]
    {A : CostructuredArrow S T} :
    ∀ P : Subobject (op A), ∃ q, S.map (projectQuotient P).arrow.unop ≫ q = A.hom :=
  Subobject.ind _ fun P f hf =>
    ⟨S.map (Subobject.underlyingIso _).unop.inv ≫ P.unop.hom, by
      dsimp
      rw [← Category.assoc, ← S.map_comp, ← unop_comp]
      simp⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (Subobject.mk f.unop.left.op).arrow.unop ≫
      S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ (unop P).hom =
    A.hom

Tactic:
rw [← Category.assoc, ← S.map_comp, ← unop_comp]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ (Subobject.mk f.unop.left.op).arrow).unop ≫ (unop P).hom = A.hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫
      S.map (Subobject.underlyingIso (MonoOver.mk' f).arrow.unop.left.op).unop.inv ≫ (unop P).hom =
    A.hom

Tactic:
dsimp

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (Subobject.mk f.unop.left.op).arrow.unop ≫
      S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ (unop P).hom =
    A.hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ (Subobject.mk f.unop.left.op).arrow).unop ≫ (unop P).hom = A.hom

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem measure_univ : volume (Set.univ : Set UnitAddCircle) = 1

Proof state:
⊢ volume univ = 1

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma toPerfectPairing_apply_CoPolarization (x : N) :
    P.toPerfectPairing (P.CoPolarization x) = P.CorootForm x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : N
⊢ P.toPerfectPairing (P.CoPolarization x) = P.CorootForm x

Tactic:
ext y

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x y : N
⊢ (P.toPerfectPairing (P.CoPolarization x)) y = (P.CorootForm x) y

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x y : N
⊢ (P.toPerfectPairing (P.CoPolarization x)) y = (P.CorootForm x) y

Tactic:
exact P.flip.toPerfectPairing_apply_apply_Polarization x y

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a

Proof state:
a b : Nat
h : ¬a ∣ b
⊢ 0 < b % a

Tactic:
rw [dvd_iff_mod_eq_zero] at h

Result:
a b : Nat
h : ¬b % a = 0
⊢ 0 < b % a

Proof state:
a b : Nat
h : ¬b % a = 0
⊢ 0 < b % a

Tactic:
exact Nat.pos_of_ne_zero h

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem frobeniusBoundedSMul [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α]
    [BoundedSMul R α] :
    BoundedSMul R (Matrix m n α) :=
  (by infer_instance : BoundedSMul R (PiLp 2 fun i : m => PiLp 2 fun j : n => α))

Proof state:
R : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : SeminormedRing R
inst✝² : SeminormedAddCommGroup α
inst✝¹ : Module R α
inst✝ : BoundedSMul R α
⊢ BoundedSMul R (PiLp 2 fun i => PiLp 2 fun j => α)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem L_mul {G : Type*} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I ∞ G]
    (g h : G) : 𝑳 I (g * h) = (𝑳 I g).comp (𝑳 I h)

Proof state:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h x✝ : G
⊢ (𝑳 I (g * h)) x✝ = ((𝑳 I g).comp (𝑳 I h)) x✝

Tactic:
simp only [ContMDiffMap.comp_apply, L_apply, mul_assoc]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h : G
⊢ 𝑳 I (g * h) = (𝑳 I g).comp (𝑳 I h)

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h x✝ : G
⊢ (𝑳 I (g * h)) x✝ = ((𝑳 I g).comp (𝑳 I h)) x✝
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normalClosure_le_iSup_adjoin :
    normalClosure F K L ≤ ⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L) :=
  iSup_le fun f _ ⟨x, hx⟩ ↦ le_iSup (α := IntermediateField F L) _ x <|
    IntermediateField.subset_adjoin F _ <| by
      rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]

Proof state:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x✝¹ : L
x✝ : x✝¹ ∈ f.fieldRange
x : K
hx : f.toRingHom x = x✝¹
⊢ x✝¹ ∈ (minpoly F x).rootSet L

Tactic:
rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
  AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_zero' : eLpNorm (fun _ : α => (0 : F)) p μ = 0

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
⊢ eLpNorm (fun x => 0) p μ = 0

Tactic:
convert eLpNorm_zero (F := F)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem diff_cons_right (l₁ l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.diff l₂).erase a

Proof state:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (l₁.diff l₂).erase a = l₁.diff (a :: l₂)

Tactic:
induction l₂ generalizing l₁ <;> simp [erase_comm, *]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ l₁.diff (a :: l₂) = (l₁.diff l₂).erase a

Tactic:
apply Eq.symm

Result:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (l₁.diff l₂).erase a = l₁.diff (a :: l₂)
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem hundred_le_m [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α)
    (hPε : 100 ≤ (4 : ℝ) ^ #P.parts * ε ^ 5) (hε : ε ≤ 1) : 100 ≤ m :=
  mod_cast
    (hundred_div_ε_pow_five_le_m hPα hPε).trans'
      (le_div_self (by norm_num) (by sz_positivity) <| pow_le_one₀ (by sz_positivity) hε)

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε : ε ≤ 1
⊢ 0 ≤ 100

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε : ε ≤ 1
⊢ 0 < ε ^ 5

Tactic:
sz_positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε : ε ≤ 1
⊢ 0 ≤ ε

Tactic:
sz_positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α}
    {k k' : α} (k_beq : k == k')
    (not_mem : ¬ k ∈ m) (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l) {h} :
    getKey (insertManyIfNewUnit m l) k' h = k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
not_mem : ¬k ∈ m
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
h : k' ∈ insertManyIfNewUnit m l
⊢ (insertManyIfNewUnit m l).getKey k' h = k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
h : k' ∈ insertManyIfNewUnit m l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey k' h = k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
h : k' ∈ insertManyIfNewUnit m l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey k' h = k

Tactic:
exact Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
  not_mem distinct mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_signExtend : eval assign (.signExtend v expr) = BitVec.signExtend v (eval assign expr)

Proof state:
assign : Assignment
v a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (signExtend v expr) = BitVec.signExtend v (eval assign expr)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Defs.lean
theorem prod_eq_pow_card (l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.prod = m ^ l.length

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = m ^ l.length

Tactic:
rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
theorem lift_map_single (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (r : R) :
    (lift R F).map (single f r) = r • F.map f

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : C
f : X ⟶ Y
r : R
⊢ (lift R F).map (single f r) = r • F.map f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/NatAntidiagonal.lean
theorem card_antidiagonal (n : ℕ) : card (antidiagonal n) = n + 1

Proof state:
n : ℕ
⊢ (antidiagonal n).card = n + 1

Tactic:
rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_preimage_eq_of_subset {f : α → β} {s : Set β} (hs : s ⊆ range f) :
    f '' (f ⁻¹' s) = s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s ⊆ range f
⊢ f '' (f ⁻¹' s) = s

Tactic:
rw [image_preimage_eq_range_inter, inter_eq_self_of_subset_right hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_one_add_one {a : Nat} (h : a ≠ 0) : a - 1 + 1 = a

Proof state:
case succ
n✝ : Nat
a✝ : n✝ ≠ 0 → n✝ - 1 + 1 = n✝
h : n✝ + 1 ≠ 0
⊢ n✝ + 1 - 1 + 1 = n✝ + 1

Tactic:
rfl

Result:
no goals

Proof state:
case zero
h : 0 ≠ 0
⊢ 0 - 1 + 1 = 0

Tactic:
contradiction

Result:
no goals

Proof state:
a : Nat
h : a ≠ 0
⊢ a - 1 + 1 = a

Tactic:
induction a with
| zero => contradiction
| succ => rfl

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atTop_zsmul_neg_const {f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atBot

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atBot

Tactic:
simpa using hf.atTop_zsmul_const (neg_pos.2 hr)

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem intCast_div (a b : ℤ) (h : b ∣ a) : ((a / b : ℤ) : ℚ) = a / b

Proof state:
a b : ℤ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b

Tactic:
rcases h with ⟨c, rfl⟩

Result:
case intro
b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b

Proof state:
case intro
b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b

Tactic:
rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul,
  intCast_div_self, Int.cast_mul, mul_div_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹ = ↑h.unit⁻¹ • A.adjugate

Tactic:
rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_image_preimage {f : α → β} {s : Set β} : f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s

Tactic:
rw [image_preimage_eq_range_inter, preimage_range_inter]

Result:
no goals
-- Mathlib/Order/Cover.lean
@[simp] lemma coe_covBy_top : (a : WithTop α) ⋖ ⊤ ↔ IsMax a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑a ⋖ ⊤ ↔ IsMax a

Tactic:
simp only [covBy_iff_Ioo_eq, ← image_coe_Ioi, coe_lt_top, image_eq_empty,
  true_and, Ioi_eq_empty_iff]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepSet_iff_iIndep (s : ι → Set Ω) (μ : Measure Ω) :
    iIndepSet s μ ↔ iIndep (fun i ↦ generateFrom {s i}) μ

Proof state:
Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s μ ↔ iIndep (fun i => generateFrom {s i}) μ

Tactic:
simp only [iIndepSet, iIndep, Kernel.iIndepSet]

Result:
no goals
-- Mathlib/Computability/TuringMachine.lean
theorem stk_nth_val {K : Type*} {Γ : K → Type*} {L : ListBlank (∀ k, Option (Γ k))} {k S} (n)
    (hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse) :
    L.nth n k = S.reverse[n]?

Proof state:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (Option.map some S.reverse[n]?).iget = S.reverse[n]?

Tactic:
cases S.reverse[n]? <;> rfl

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ L.nth n k = S.reverse[n]?

Tactic:
rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk,
  List.getI_eq_iget_getElem?, List.getElem?_map]

Result:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
k : K
S : List (Γ k)
n : ℕ
hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse
⊢ (Option.map some S.reverse[n]?).iget = S.reverse[n]?
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem rank_span {v : ι → M} (hv : LinearIndependent R v) :
    Module.rank R ↑(span R (range v)) = #(range v)

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
⊢ Module.rank R ↥(span R (range v)) = #↑(range v)

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Module.rank R ↥(span R (range v)) = #↑(range v)

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
this : Nontrivial R
⊢ Module.rank R ↥(span R (range v)) = #↑(range v)

Tactic:
rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
  Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
lemma colimitsOfShape_discrete_le_llp_rlp (J : Type w) :
    T.colimitsOfShape (Discrete J) ≤ T.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type w
⊢ T.colimitsOfShape (Discrete J) ≤ T.rlp.llp

Tactic:
intro A B i hi

Result:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type w
A B : C
i : A ⟶ B
hi : T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type w
A B : C
i : A ⟶ B
hi : T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i

Tactic:
exact (T.rlp.llp.isStableUnderColimitsOfShape_iff_colimitsOfShape_le (Discrete J)).1
  (llp_isStableUnderCoproductsOfShape _ _) _
    (colimitsOfShape_monotone T.le_llp_rlp _ _ hi)

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
theorem MonoidHom.comp_id_commMonCat {G : CommMonCat.{u}} {H : Type u} [CommMonoid H] (f : G →* H) :
    f.comp (CommMonCat.Hom.hom (𝟙 G)) = f

Proof state:
G : CommMonCat
H : Type u
inst✝ : CommMonoid H
f : ↑G →* H
⊢ f.comp (CommMonCat.Hom.hom (𝟙 G)) = f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {a fallback : α} :
    m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a fallback : α
⊢ m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)

Tactic:
simp_to_raw using Raw₀.getKey?_eq_some_getKeyD

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem minNatAbs_eq_nonzero_iff (xs : List Int) (w : z ≠ 0) :
    xs.minNatAbs = z ↔ (∃ y ∈ xs, y.natAbs = z) ∧ (∀ y ∈ xs, z ≤ y.natAbs ∨ y = 0)

Proof state:
z : Nat
xs : List Int
w : z ≠ 0
⊢ xs.minNatAbs = z ↔ (∃ y, y ∈ xs ∧ y.natAbs = z) ∧ ∀ (y : Int), y ∈ xs → z ≤ y.natAbs ∨ y = 0

Tactic:
simp [minNatAbs, nonzeroMinimum_eq_nonzero_iff w]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.map_mk₂ {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (L R : List Γ) :
    (Tape.mk₂ L R).map f = Tape.mk₂ (L.map f) (R.map f)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
L R : List Γ
⊢ map f (mk₂ L R) = mk₂ (List.map f.f L) (List.map f.f R)

Tactic:
simp only [Tape.mk₂, Tape.map_mk', ListBlank.map_mk]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem xgcdAux_val (x y) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)

Proof state:
x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = (x.gcd y, x.xgcd y)

Tactic:
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq {y : M'}
    (hg : MDifferentiableWithinAt I' I'' g u y)
    (hf : MDifferentiableWithinAt I I' f s x) (h : f ⁻¹' u ∈ 𝓝[s] x) (hy : f x = y) :
    MDifferentiableWithinAt I I'' (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin _ hg hf h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
y : M'
hg : MDifferentiableWithinAt I' I'' g u y
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hy : f x = y
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x
-- Mathlib/Data/Nat/Totient.lean
theorem filter_coprime_Ico_eq_totient (a n : ℕ) :
    #{x ∈ Ico n (n + a) | a.Coprime x} = totient a

Proof state:
case pp
a n : ℕ
⊢ Function.Periodic (fun x => a.Coprime x) a

Tactic:
exact periodic_coprime a

Result:
no goals

Proof state:
a n : ℕ
⊢ #(filter (fun x => a.Coprime x) (Ico n (n + a))) = φ a

Tactic:
rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]

Result:
case pp
a n : ℕ
⊢ Function.Periodic (fun x => a.Coprime x) a
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem nhds_translation_div (x : G) : comap (· / x) (𝓝 1) = 𝓝 x

Proof state:
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ comap (fun x_1 => x_1 / x) (𝓝 1) = 𝓝 x

Tactic:
simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x

Result:
no goals