harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/CountableInter.lean
theorem countableGenerate_isGreatest :
    IsGreatest { f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets } (countableGenerate g)

Proof state:
α : Type u_2
g : Set (Set α)
⊢ IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)

Tactic:
refine ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩

Result:
α : Type u_2
g : Set (Set α)
⊢ countableGenerate g ∈ upperBounds {f | CountableInterFilter f ∧ g ⊆ f.sets}

Proof state:
case intro
α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ f ≤ countableGenerate g

Tactic:
rwa [@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct]

Result:
no goals

Proof state:
α : Type u_2
g : Set (Set α)
⊢ countableGenerate g ∈ upperBounds {f | CountableInterFilter f ∧ g ⊆ f.sets}

Tactic:
rintro f ⟨fct, hf⟩

Result:
case intro
α : Type u_2
g : Set (Set α)
f : Filter α
fct : CountableInterFilter f
hf : g ⊆ f.sets
⊢ f ≤ countableGenerate g
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive nsmul_sub]
lemma div_pow (a b : α) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
simp only [div_eq_mul_inv, mul_pow, inv_pow]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem associated_toQuadraticMap (B : BilinMap R M N) (x y : M) :
    associatedHom S B.toQuadraticMap x y = ⅟ (2 : Module.End R N) • (B x y + B y x)

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B : BilinMap R M N
x y : M
⊢ ⅟2 ((B x) x) + ⅟2 ((B y) x) + (⅟2 ((B x) y) + ⅟2 ((B y) y)) - ⅟2 ((B x) x) - ⅟2 ((B y) y) =
    ⅟2 ((B x) y) + ⅟2 ((B y) x)

Tactic:
abel_nf

Result:
no goals

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B : BilinMap R M N
x y : M
⊢ (((associatedHom S) B.toQuadraticMap) x) y = ⅟2 • ((B x) y + (B y) x)

Tactic:
simp only [associated_apply, BilinMap.toQuadraticMap_apply, map_add, LinearMap.add_apply,
  LinearMap.smul_def, _root_.map_sub]

Result:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B : BilinMap R M N
x y : M
⊢ ⅟2 ((B x) x) + ⅟2 ((B y) x) + (⅟2 ((B x) y) + ⅟2 ((B y) y)) - ⅟2 ((B x) x) - ⅟2 ((B y) y) =
    ⅟2 ((B x) y) + ⅟2 ((B y) x)
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_right (ha : a ∈ s) : Prod.mk a ⁻¹' s ×ˢ t = t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = t

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ t

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ t

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Control/Traversable/Equiv.lean
theorem id_traverse (x : t' α) : Equiv.traverse eqv (pure : α → Id α) x = x

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ Equiv.traverse eqv pure x = x

Tactic:
rw [Equiv.traverse, id_traverse, Id.map_eq, apply_symm_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_map_coe (l : Vector α n) (f : α → β) :
    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β
⊢ map (fun i => f i.val) l.attach = map f l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map (fun i => f i.val) { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    map f { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map (fun i => f i.val) { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    map f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem map_neg (x : M) : Q (-x) = Q x

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ Q (-x) = Q x

Tactic:
rw [← @neg_one_smul R _ _ _ _ x, map_smul, neg_one_mul, neg_neg, one_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem limit_ext (x y : limit F) (w : ∀ j, limit.π F j x = limit.π F j y) : x = y

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ x = y

Tactic:
apply (limitEquivSections F).injective

Result:
case a
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ (limitEquivSections F) x = (limitEquivSections F) y

Proof state:
case a.a.h
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
j : J
⊢ ↑((limitEquivSections F) x) j = ↑((limitEquivSections F) y) j

Tactic:
simp [w j]

Result:
no goals

Proof state:
case a
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ (limitEquivSections F) x = (limitEquivSections F) y

Tactic:
ext j

Result:
case a.a.h
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
j : J
⊢ ↑((limitEquivSections F) x) j = ↑((limitEquivSections F) y) j
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_zpow (f : N ≃ₗ[R] N) (n : ℤ) : f.lTensor M ^ n = (f ^ n).lTensor M

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N ≃ₗ[R] N
n : ℤ
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
simpa only [one_zpow] using TensorProduct.congr_zpow (1 : M ≃ₗ[R] M) f n

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Icc_pred_right_eq_Ico (a b : α) : Icc a (pred b) = Ico a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Icc a (pred b)) = ↑(Ico a b)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma sUnion_union_sUnion_disjointOfDiffUnion_of_subset (hC : IsSetSemiring C)
    (hs : s ∈ C) (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s) :
    ⋃₀ I ∪ ⋃₀ hC.disjointOfDiffUnion hs hI = s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
⊢ ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) = s

Tactic:
conv_rhs => rw [← union_diff_cancel (Set.sUnion_subset hI_ss : ⋃₀ ↑I ⊆ s),
  hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem eq_empty_iff {n m : ℕ} : Ico n m = [] ↔ m ≤ n :=
  Iff.intro (fun h => Nat.sub_eq_zero_iff_le.mp <| by rw [← length, h, List.length]) eq_nil_of_le

Proof state:
n m : ℕ
h : Ico n m = []
⊢ m - n = 0

Tactic:
rw [← length, h, List.length]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
@[simp] lemma natDegree_mul_X_pow (hp : p ≠ 0) : natDegree (p * X ^ n) = natDegree p + n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p * X ^ n).natDegree = p.natDegree + n

Tactic:
rw [natDegree_mul' (by simpa), natDegree_X_pow]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.leadingCoeff * (X ^ n).leadingCoeff ≠ 0

Tactic:
simpa

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem sum_eapproxDiff (f : α → ℝ≥0∞) (n : ℕ) (a : α) :
    (∑ k ∈ Finset.range (n + 1), (eapproxDiff f k a : ℝ≥0∞)) = eapprox f n a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f (n + 1)) a ≤ (eapprox f (n + 1)) a + (eapprox f n) a

Tactic:
exact le_self_add

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f (n + 1)) a - (eapprox f n) a ≠ ⊤

Tactic:
apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f (n + 1)) a - (eapprox f n) a ≤ (eapprox f (n + 1)) a

Proof state:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
⊢ ↑((eapproxDiff f 0) a) = (eapprox f 0) a

Tactic:
rfl

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
⊢ ∑ k ∈ Finset.range (0 + 1), ↑((eapproxDiff f k) a) = (eapprox f 0) a

Tactic:
simp only [Nat.zero_add, Finset.sum_singleton, Finset.range_one]

Result:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
⊢ ↑((eapproxDiff f 0) a) = (eapprox f 0) a

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ ∑ k ∈ Finset.range (n + 1 + 1), ↑((eapproxDiff f k) a) = (eapprox f (n + 1)) a

Tactic:
rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply,
  coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
  add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]

Result:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f (n + 1)) a - (eapprox f n) a ≠ ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f (n + 1)) a - (eapprox f n) a ≤ (eapprox f (n + 1)) a

Tactic:
rw [tsub_le_iff_right]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f (n + 1)) a ≤ (eapprox f (n + 1)) a + (eapprox f n) a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a

Tactic:
induction' n with n IH

Result:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
⊢ ∑ k ∈ Finset.range (0 + 1), ↑((eapproxDiff f k) a) = (eapprox f 0) a

case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ ∑ k ∈ Finset.range (n + 1 + 1), ↑((eapproxDiff f k) a) = (eapprox f (n + 1)) a
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_zero : basicOpen 𝒜 (0 : A) = ⊥ :=
  TopologicalSpace.Opens.ext <| by simp

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ↑(basicOpen 𝒜 0) = ↑⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
lemma sub_sq' (a b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b

Proof state:
R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b

Tactic:
rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) :
    l.attach.count a = l.count ↑a :=
  Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a x✝¹ : { x // x ∈ l }
x✝ : x✝¹ ∈ l.attach
⊢ (x✝¹ == a) = true ↔ (x✝¹.val == a.val) = true

Tactic:
simp [Subtype.ext_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {s : Set α} :
    TotallyBounded s ↔ ∀ U ∈ 𝓝 (1 : α), ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U :=
  (𝓝 (1 : α)).basis_sets.uniformity_of_nhds_one_inv_mul_swapped.totallyBounded_iff.trans <| by
    simp [← preimage_smul_inv, preimage]

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set α
⊢ (∀ i ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ {x | x.2⁻¹ * x.1 ∈ id i}}) ↔
    ∀ U ∈ 𝓝 1, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U

Tactic:
simp [← preimage_smul_inv, preimage]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma uniqueBaseOn_closure_eq (I E X : Set α) :
    (uniqueBaseOn I E).closure X = (X ∩ I ∩ E) ∪ (E \ I)

Proof state:
α : Type u_2
I E X : Set α
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I

Tactic:
rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm,
  inter_assoc (c := E), inter_self, inter_right_comm, freeOn_ground]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_le_of_surjective_injective (i : R → R') (j : M →+ M₁)
    (hi : Surjective i) (hj : Injective j)
    (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Module.rank R M ≤ Module.rank R' M₁

Proof state:
R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R → R'
j : M →+ M₁
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_le_of_surjective_injective i j hi hj hc

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
lemma IsInvertible.comp {g : M₂ →L[R] M₃} {f : M →L[R] M₂}
    (hg : g.IsInvertible) (hf : f.IsInvertible) : (g ∘L f).IsInvertible

Proof state:
case intro.intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
N : M₂ ≃L[R] M₃
M : M✝ ≃L[R] M₂
⊢ ((↑N).comp ↑M).IsInvertible

Tactic:
exact ⟨M.trans N, rfl⟩

Result:
no goals

Proof state:
case intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
hf : f.IsInvertible
N : M₂ ≃L[R] M₃
⊢ ((↑N).comp f).IsInvertible

Tactic:
rcases hf with ⟨M, rfl⟩

Result:
case intro.intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
N : M₂ ≃L[R] M₃
M : M✝ ≃L[R] M₂
⊢ ((↑N).comp ↑M).IsInvertible

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
hf : f.IsInvertible
⊢ (g.comp f).IsInvertible

Tactic:
rcases hg with ⟨N, rfl⟩

Result:
case intro
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
hf : f.IsInvertible
N : M₂ ≃L[R] M₃
⊢ ((↑N).comp f).IsInvertible
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
lemma spec (g : L ≃+* L) {t : Lˣ} (ht : t ∈ rootsOfUnity n L) :
    g t = t ^ ((ModularCyclotomicCharacter L hn g) : ZMod n).val

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ ↑t ^ (toFun n g).val = ↑t ^ (↑((ModularCyclotomicCharacter L hn) g)).val

Tactic:
congr 1

Result:
case e_a
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ (toFun n g).val = (↑((ModularCyclotomicCharacter L hn) g)).val

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ g ↑t = ↑t ^ (↑((ModularCyclotomicCharacter L hn) g)).val

Tactic:
rw [toFun_spec' g ht]

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ ↑t ^ (toFun n g).val = ↑t ^ (↑((ModularCyclotomicCharacter L hn) g)).val

Proof state:
case e_a
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ (toFun n g).val = (↑((ModularCyclotomicCharacter L hn) g)).val

Tactic:
exact (ZMod.ringEquivCongr_val _ _).symm

Result:
no goals
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem log_mul_moebius_eq_vonMangoldt : log * μ = Λ

Proof state:
⊢ log * ↑μ = Λ

Tactic:
rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
    getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i))

Proof state:
n hi lo : Nat
x : BitVec n
i : Nat
⊢ (extractLsb hi lo x).getLsbD i = (decide (i ≤ hi - lo) && x.getLsbD (lo + i))

Tactic:
simp [getLsbD, Nat.lt_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) :
    (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat))

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
i : Nat
h : i < w₁
⊢ (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat))

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
/-- The uniform neighborhoods of all points of a dense indexed collection cover the whole space. -/
lemma DenseRange.iUnion_uniformity_ball {ι : Type*} {xs : ι → α}
    (xs_dense : DenseRange xs) {U : Set (α × α)} (hU : U ∈ uniformity α) :
    ⋃ i, UniformSpace.ball (xs i) U = univ

Proof state:
α : Type ua
inst✝ : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ range xs, ball x U = univ

Tactic:
exact Dense.biUnion_uniformity_ball xs_dense hU

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ i, ball (xs i) U = univ

Tactic:
rw [← biUnion_range (f := xs) (g := fun x ↦ UniformSpace.ball x U)]

Result:
α : Type ua
inst✝ : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ range xs, ball x U = univ
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem noZeroDivisors_of_finite (R : Type u) (σ : Type v) [CommSemiring R] [Finite σ]
    [NoZeroDivisors R] : NoZeroDivisors (MvPolynomial σ R)

Proof state:
case intro
R : Type u
σ : Type v
inst✝² : CommSemiring R
inst✝¹ : Finite σ
inst✝ : NoZeroDivisors R
val✝ : Fintype σ
⊢ NoZeroDivisors (MvPolynomial σ R)

Tactic:
haveI := noZeroDivisors_fin R (Fintype.card σ)

Result:
case intro
R : Type u
σ : Type v
inst✝² : CommSemiring R
inst✝¹ : Finite σ
inst✝ : NoZeroDivisors R
val✝ : Fintype σ
this : NoZeroDivisors (MvPolynomial (Fin (Fintype.card σ)) R)
⊢ NoZeroDivisors (MvPolynomial σ R)

Proof state:
case intro
R : Type u
σ : Type v
inst✝² : CommSemiring R
inst✝¹ : Finite σ
inst✝ : NoZeroDivisors R
val✝ : Fintype σ
this : NoZeroDivisors (MvPolynomial (Fin (Fintype.card σ)) R)
⊢ NoZeroDivisors (MvPolynomial σ R)

Tactic:
exact (renameEquiv R (Fintype.equivFin σ)).injective.noZeroDivisors _ (map_zero _) (map_mul _)

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝² : CommSemiring R
inst✝¹ : Finite σ
inst✝ : NoZeroDivisors R
⊢ NoZeroDivisors (MvPolynomial σ R)

Tactic:
cases nonempty_fintype σ

Result:
case intro
R : Type u
σ : Type v
inst✝² : CommSemiring R
inst✝¹ : Finite σ
inst✝ : NoZeroDivisors R
val✝ : Fintype σ
⊢ NoZeroDivisors (MvPolynomial σ R)
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
theorem isωSup_iff_isLUB {α : Type u} [Preorder α] {c : Chain α} {x : α} :
    IsωSup c x ↔ IsLUB (range c) x

Proof state:
α : Type u
inst✝ : Preorder α
c : Chain α
x : α
⊢ IsωSup c x ↔ IsLUB (range ⇑c) x

Tactic:
simp [IsωSup, IsLUB, IsLeast, upperBounds, lowerBounds]

Result:
no goals