harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Homeomorph.lean
theorem map_coclosedCompact (h : X ≃ₜ Y) : map h (coclosedCompact X) = coclosedCompact Y

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ map (⇑h) (coclosedCompact X) = coclosedCompact Y

Tactic:
rw [← h.comap_coclosedCompact, map_comap_of_surjective h.surjective]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
@[simp, reassoc]
lemma Functor.map_braiding (F : C ⥤ D) (X Y : C) [F.Braided] :
    F.map (β_ X Y).hom =
    δ F X Y ≫ (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
X Y : C
inst✝ : F.Braided
⊢ F.map (β_ X Y).hom = δ F X Y ≫ (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X

Tactic:
rw [← Functor.Braided.braided, δ_μ_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma eval_polynomialY_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    eval P W.polynomialY / P z ^ 2 = W.toAffine.polynomialY.evalEval (P x / P z) (P y / P z)

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2) / P z ^ 2 +
        (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (2 * (P y / P z) + (toAffine W).a₁ * (P x / P z) + (toAffine W).a₃ +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) + W.a₃ * (P z ^ 2 / P z ^ 2))) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 2 = Polynomial.evalEval (P x / P z) (P y / P z) (toAffine W).polynomialY

Tactic:
linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
  2 * P y / P z * div_self hPz + W.a₁ * P x / P z * div_self hPz
    + W.a₃ * div_self (pow_ne_zero 2 hPz)

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 2 + (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (Polynomial.evalEval (P x / P z) (P y / P z) (toAffine W).polynomialY +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) + W.a₃ * (P z ^ 2 / P z ^ 2))) =
    0

Tactic:
rw [eval_polynomialY, Affine.evalEval_polynomialY]

Result:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2) / P z ^ 2 +
        (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (2 * (P y / P z) + (toAffine W).a₁ * (P x / P z) + (toAffine W).a₃ +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) + W.a₃ * (P z ^ 2 / P z ^ 2))) =
    0
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_univ : dimH (univ : Set ℝ) = 1

Proof state:
⊢ dimH univ = 1

Tactic:
rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one]

Result:
no goals
-- Mathlib/Probability/CDF.lean
/-- If two real probability distributions have the same cdf, they are equal. -/
lemma MeasureTheory.Measure.eq_of_cdf (μ ν : Measure ℝ) [IsProbabilityMeasure μ]
    [IsProbabilityMeasure ν] (h : cdf μ = cdf ν) : μ = ν

Proof state:
μ ν : Measure ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h : cdf μ = cdf ν
⊢ μ = ν

Tactic:
rw [← measure_cdf μ, ← measure_cdf ν, h]

Result:
no goals
-- Mathlib/Topology/FiberBundle/IsHomeomorphicTrivialBundle.lean
theorem surjective_proj [Nonempty F] (h : IsHomeomorphicTrivialFiberBundle F proj) :
    Function.Surjective proj

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
proj : Z → B
inst✝ : Nonempty F
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Function.Surjective proj

Tactic:
obtain ⟨e, rfl⟩ := h.proj_eq

Result:
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty F
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)
⊢ Function.Surjective (Prod.fst ∘ ⇑e)

Proof state:
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty F
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)
⊢ Function.Surjective (Prod.fst ∘ ⇑e)

Tactic:
exact Prod.fst_surjective.comp e.surjective

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Prime.dvd_iff_one_le_factorization {p n : ℕ} (pp : Prime p) (hn : n ≠ 0) :
    p ∣ n ↔ 1 ≤ n.factorization p :=
  Iff.trans (by simp) (pp.pow_dvd_iff_le_factorization hn)

Proof state:
p n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ∣ n ↔ p ^ 1 ∣ n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem AddSubgroup.int_mul_mem {G : AddSubgroup R} (k : ℤ) {g : R} (h : g ∈ G) :
    (k : R) * g ∈ G

Proof state:
case h.e'_5
R : Type u
inst✝ : Ring R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g = k • g

Tactic:
rw [zsmul_eq_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g ∈ G

Tactic:
convert AddSubgroup.zsmul_mem G h k using 1

Result:
case h.e'_5
R : Type u
inst✝ : Ring R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g = k • g
-- Mathlib/Topology/Category/TopCat/Basic.lean
lemma inv_hom_id_apply {X Y : TopCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y

Proof state:
X Y : TopCat
f : X ≅ Y
y : ↑Y
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom f.inv) y) = y

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_comp_coe_Ioo_atTop (h : a < b) :
    Tendsto (fun x : Ioo a b => f x) atTop l ↔ Tendsto f (𝓝[<] b) l

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : α → β
h : a < b
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : α → β
h : a < b
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f (𝓝[<] b) l

Tactic:
rw [← map_coe_Ioo_atTop h, tendsto_map'_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : α → β
h : a < b
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_measure_zero_of_exponent_zero {f : α → ε} : eLpNorm' f 0 (0 : Measure α) = 1

Proof state:
α : Type u_1
ε : Type u_2
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
⊢ eLpNorm' f 0 0 = 1

Tactic:
simp [eLpNorm']

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem bddAbove_iff_exists_ge [SemilatticeSup γ] {s : Set γ} (x₀ : γ) :
    BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Proof state:
γ : Type v
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x => ∀ y ∈ s, y ≤ x

Tactic:
exact Monotone.ball fun x _ => monotone_le

Result:
no goals

Proof state:
γ : Type v
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Tactic:
rw [bddAbove_def, exists_ge_and_iff_exists]

Result:
γ : Type v
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone fun x => ∀ y ∈ s, y ≤ x
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma cyclesMap'_sub :
    cyclesMap' (φ - φ') h₁ h₂ = cyclesMap' φ h₁ h₂ -
      cyclesMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' (φ - φ') h₁ h₂ = cyclesMap' φ h₁ h₂ - cyclesMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, cyclesMap'_add, cyclesMap'_neg]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow (q : ℕ) [hF : ExpChar F q] :
    IsPurelyInseparable F E ↔
    ∀ x : E, ∃ n : ℕ, (minpoly F x).map (algebraMap F E) = (X - C x) ^ q ^ n

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one,
  minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow q]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem disjoint_map {f : α → β} {s t : List α} (hf : Function.Injective f)
    (h : Disjoint s t) : Disjoint (s.map f) (t.map f)

Proof state:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (pmap (fun a x => f a) s ⋯).Disjoint (pmap (fun a x => f a) t ⋯)

Tactic:
exact disjoint_pmap _ _ (fun _ _ _ _ h' ↦ hf h') h

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (map f s).Disjoint (map f t)

Tactic:
rw [← pmap_eq_map _ _ _ (fun _ _ ↦ trivial), ← pmap_eq_map _ _ _ (fun _ _ ↦ trivial)]

Result:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (pmap (fun a x => f a) s ⋯).Disjoint (pmap (fun a x => f a) t ⋯)
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_of_nonempty_iUnion
    {s : ι → Set α} (h_Union : (⋃ i, s i).Nonempty) : Nonempty ι

Proof state:
α : Type u_1
ι : Sort u_5
s : ι → Set α
h_Union : (⋃ i, s i).Nonempty
⊢ Nonempty ι

Tactic:
obtain ⟨x, hx⟩ := h_Union

Result:
case intro
α : Type u_1
ι : Sort u_5
s : ι → Set α
x : α
hx : x ∈ ⋃ i, s i
⊢ Nonempty ι

Proof state:
case intro
α : Type u_1
ι : Sort u_5
s : ι → Set α
x : α
hx : x ∈ ⋃ i, s i
⊢ Nonempty ι

Tactic:
exact ⟨Classical.choose <| mem_iUnion.mp hx⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem smulTower_leftMulMatrix_algebraMap (x : S) :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) = blockDiagonal fun _ ↦ leftMulMatrix b x

Proof state:
case a.mk.mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) (if (i, k).2 = (j, k').2 then (algebraMap S S) x else 0) (i, k).1 (j, k').1 =
    if (i, k).2 = (j, k').2 then (leftMulMatrix b) x (i, k).1 (j, k').1 else 0

Tactic:
split_ifs with h <;> simp only at h <;> simp [h]

Result:
no goals

Proof state:
case a.mk.mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') =
    blockDiagonal (fun x_1 => (leftMulMatrix b) x) (i, k) (j, k')

Tactic:
rw [smulTower_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]

Result:
case a.mk.mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) (if (i, k).2 = (j, k').2 then (algebraMap S S) x else 0) (i, k).1 (j, k').1 =
    if (i, k).2 = (j, k').2 then (leftMulMatrix b) x (i, k).1 (j, k').1 else 0

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) = blockDiagonal fun x_1 => (leftMulMatrix b) x

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

Result:
case a.mk.mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') =
    blockDiagonal (fun x_1 => (leftMulMatrix b) x) (i, k) (j, k')
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem cocyclesMap_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) :
    cocyclesMap (MonoidHom.id G) (φ ≫ ψ) n =
      cocyclesMap (MonoidHom.id G) φ n ≫ cocyclesMap (MonoidHom.id G) ψ n

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ cocyclesMap (MonoidHom.id G) (φ ≫ ψ) n = cocyclesMap (MonoidHom.id G) φ n ≫ cocyclesMap (MonoidHom.id G) ψ n

Tactic:
simp [cocyclesMap, cochainsMap_id_comp, HomologicalComplex.cyclesMap_comp]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[reassoc]
lemma resLE_comp_resLE {Z : Scheme.{u}} (g : Y ⟶ Z) {W : Z.Opens} (e') :
    f.resLE U V e ≫ g.resLE W U e' = (f ≫ g).resLE W V
      (e.trans ((Opens.map f.base).map (homOfLE e')).le)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
Z : Scheme
g : Y ⟶ Z
W : Z.Opens
e' : U ≤ g ⁻¹ᵁ W
⊢ resLE f U V e ≫ resLE g W U e' = resLE (f ≫ g) W V ⋯

Tactic:
simp [← cancel_mono W.ι]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_div_self' : √x / x = 1 / √x

Proof state:
x : ℝ
⊢ √x / x = 1 / √x

Tactic:
rw [← div_sqrt, one_div_div, div_sqrt]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mker_one : mker (1 : M →* N) = ⊤

Proof state:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M
⊢ x✝ ∈ mker 1 ↔ x✝ ∈ ⊤

Tactic:
simp [mem_mker]

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker 1 = ⊤

Tactic:
ext

Result:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M
⊢ x✝ ∈ mker 1 ↔ x✝ ∈ ⊤
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ne_of_mem_sphere (h : y ∈ sphere x ε) (hε : ε ≠ 0) : y ≠ x :=
  ne_of_mem_of_not_mem h <| by simpa using hε.symm

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ sphere x ε
hε : ε ≠ 0
⊢ x ∉ sphere x ε

Tactic:
simpa using hε.symm

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma IsScalarTower.of_smul_one_mul {M N} [Monoid N] [SMul M N]
    (h : ∀ (x : M) (y : N), x • (1 : N) * y = x • y) : IsScalarTower M N N :=
  ⟨fun x y z ↦ by rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]⟩

Proof state:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • y) • z = x • y • z

Tactic:
rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateRow_sum (A : Matrix n n R) (j : n) (c : n → R) :
    (A.updateRow j (∑ k, (c k) • A k)).det = (c j) • A.det

Proof state:
case h.e'_2.h.e'_6.h.e'_7
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ ∑ k : n, c k • A k = c j • A j + ∑ k ∈ univ.erase j, c k • A k

Tactic:
rw [← Finset.univ.add_sum_erase _ (Finset.mem_univ j)]

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ (A.updateRow j (∑ k : n, c k • A k)).det = c j • A.det

Tactic:
convert det_updateRow_sum_aux A (Finset.univ.erase j) (Finset.univ.not_mem_erase j) c (c j)

Result:
case h.e'_2.h.e'_6.h.e'_7
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ ∑ k : n, c k • A k = c j • A j + ∑ k ∈ univ.erase j, c k • A k
-- Mathlib/Data/Set/Card.lean
theorem coe_fintypeCard (s : Set α) [Fintype s] : Fintype.card s = s.encard

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ ↑(Fintype.card ↑s) = s.encard

Tactic:
simp [encard_eq_coe_toFinset_card]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_def (l : Array α) (f : α → Array β) : l.flatMap f = flatten (map f l)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ flatMap f { toList := l } = (map f { toList := l }).flatten

Tactic:
simp [flatten_toArray, Function.comp_def, List.flatMap_def]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ flatMap f l = (map f l).flatten

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
l : List α
⊢ flatMap f { toList := l } = (map f { toList := l }).flatten
-- Mathlib/Order/Atoms.lean
theorem isCoatomistic_dual_iff_isAtomistic : IsCoatomistic αᵒᵈ ↔ IsAtomistic α :=
  ⟨fun h => ⟨fun b => by apply h.eq_sInf_coatoms⟩, fun h => ⟨fun b => by apply h.eq_sSup_atoms⟩⟩

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsCoatomistic αᵒᵈ
b : α
⊢ ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
apply h.eq_sInf_coatoms

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsAtomistic α
b : αᵒᵈ
⊢ ∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a

Tactic:
apply h.eq_sSup_atoms

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem Indep.restrict_eq_freeOn (hI : M.Indep I) : M ↾ I = freeOn I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M ↾ I = freeOn I

Tactic:
rwa [restrict_eq_freeOn_iff]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma card_sdiff_comm (h : #s = #t) : #(s \ t) = #(t \ s) :=
  Nat.add_right_cancel (m := #t) <| by
    simp_rw [card_sdiff_add_card, ← h, card_sdiff_add_card, union_comm]

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ #(s \ t) + #t = #(t \ s) + #t

Tactic:
simp_rw [card_sdiff_add_card, ← h, card_sdiff_add_card, union_comm]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem bagInter_nil (l : List α) : l.bagInter [] = []

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.bagInter [] = []

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem inv_zpow (A : M) : ∀ n : ℤ, A⁻¹ ^ n = (A ^ n)⁻¹
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, inv_pow']
  | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, inv_pow']

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹

Tactic:
rw [zpow_negSucc, zpow_negSucc, inv_pow']

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ ↑n = (A ^ ↑n)⁻¹

Tactic:
rw [zpow_natCast, zpow_natCast, inv_pow']

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_eq [DivisionRing α] {x : α} (h : x ≠ 1) (n : ℕ) :
    ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Proof state:
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Tactic:
have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]

Result:
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Proof state:
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ x - 1 ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Result:
no goals

Proof state:
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Tactic:
rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/PreservesSheafification.lean
lemma sheafComposeNatTrans_fac (P : Cᵒᵖ ⥤ A) :
    adj₂.unit.app (P ⋙ F) ≫
      (sheafToPresheaf J B).map ((sheafComposeNatTrans J F adj₁ adj₂).app P) =
        whiskerRight (adj₁.unit.app P) F

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{u_3, u_1} A
inst✝¹ : Category.{u_4, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
⊢ adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map ((sheafComposeNatTrans J F adj₁ adj₂).app P) =
    whiskerRight (adj₁.unit.app P) F

Tactic:
simp [sheafComposeNatTrans, -sheafToPresheaf_obj, -sheafToPresheaf_map,
  Adjunction.homEquiv_counit]

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.mem_support_iff_exists_annihilator :
    p ∈ Module.support R M ↔ ∃ m : M, (R ∙ m).annihilator ≤ p.asIdeal

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, (Submodule.span R {m}).annihilator ≤ p.asIdeal

Tactic:
simp_rw [not_imp_not, SetLike.le_def, Submodule.mem_annihilator_span_singleton]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ p ∈ support R M ↔ ∃ m, (Submodule.span R {m}).annihilator ≤ p.asIdeal

Tactic:
rw [Module.mem_support_iff']

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, (Submodule.span R {m}).annihilator ≤ p.asIdeal
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isInitial_one : IsInitial 1

Proof state:
⊢ IsInitial 1

Tactic:
exact_mod_cast isInitial_natCast 1

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem keys_kreplace (a : α) (b : β a) : ∀ l : List (Sigma β), (kreplace a b l).keys = l.keys :=
  lookmap_map_eq _ _ <| by
    rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩
    dsimp
    split_ifs with h <;> simp +contextual [h]

Proof state:
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = ⟨a₁, b₂✝⟩.fst then some ⟨a, b⟩ else none) → ⟨a₁, b₂✝⟩.fst = ⟨a₂, b₂⟩.fst

Tactic:
dsimp

Result:
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = a₁ then some ⟨a, b⟩ else none) → a₁ = a₂

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ ∀ (a_1 b_1 : Sigma β), (b_1 ∈ if a = a_1.fst then some ⟨a, b⟩ else none) → a_1.fst = b_1.fst

Tactic:
rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩

Result:
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = ⟨a₁, b₂✝⟩.fst then some ⟨a, b⟩ else none) → ⟨a₁, b₂✝⟩.fst = ⟨a₂, b₂⟩.fst

Proof state:
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = a₁ then some ⟨a, b⟩ else none) → a₁ = a₂

Tactic:
split_ifs with h <;> simp +contextual [h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem Sphere.mk_center_radius (s : Sphere P) : (⟨s.center, s.radius⟩ : Sphere P) = s

Proof state:
P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
⊢ { center := s.center, radius := s.radius } = s

Tactic:
ext <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isLE_swap {o : Ordering} : o.swap.isLE = o.isGE

Proof state:
o : Ordering
⊢ o.swap.isLE = o.isGE

Tactic:
cases o <;> simp

Result:
no goals