harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem ZLattice.comap_span_top (hL : span K (L : Set E) = ⊤) {e : F →ₗ[K] E}
    (he : (L : Set E) ⊆ LinearMap.range e) :
    span K (ZLattice.comap K L e : Set F) = ⊤

Proof state:
K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
hL : span K ↑L = ⊤
e : F →ₗ[K] E
he : ↑L ⊆ ↑(LinearMap.range e)
⊢ span K ↑(ZLattice.comap K L e) = ⊤

Tactic:
rw [ZLattice.coe_comap, Submodule.span_preimage_eq (Submodule.nonempty L) he, hL, comap_top]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem mul_singleton_mem_nhds (a : α) {b : α} (h : s ∈ 𝓝 b) : s * {a} ∈ 𝓝 (b * a)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ (fun x => x * a) '' s ∈ 𝓝 (b * a)

Tactic:
exact smul_mem_nhds_smul (op a) h

Result:
no goals

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ s * {a} ∈ 𝓝 (b * a)

Tactic:
rw [mul_singleton]

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ (fun x => x * a) '' s ∈ 𝓝 (b * a)
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem QInfty_f_0 : (QInfty.f 0 : X _⦋0⦌ ⟶ X _⦋0⦌) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 𝟙 (X _⦋0⦌) - 𝟙 (X _⦋0⦌) = 0

Tactic:
simp only [sub_self]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty.f 0 = 0

Tactic:
dsimp [QInfty]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 𝟙 (X _⦋0⦌) - 𝟙 (X _⦋0⦌) = 0
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
lemma coneπApp_eq (j j' : J) (α : j' ⟶ i₀) (β : j' ⟶ j) :
    h.coneπApp j = (h.isoMap α ⟨𝟙 _⟩).inv ≫ F.map β

Proof state:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
dsimp [coneπApp]

Result:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = (h.isoMap α ⋯).inv ≫ F.map β

Proof state:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
  ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
  ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
  isoMap_hom_inv_id_assoc]

Result:
no goals

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
obtain ⟨s, γ, δ, h₁, h₂⟩ := IsCofiltered.bowtie
  (IsCofiltered.minToRight i₀ j) β (IsCofiltered.minToLeft i₀ j) α

Result:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem constr_apply (f : ι → M') (x : M) :
    constr (M' := M') b S f x = (b.repr x).sum fun b a => a • f b

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
S : Type u_10
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((mapDomain f (↑b.repr x)).sum fun i a => a • id i) = (b.repr x).sum fun b a => a • f b

Tactic:
rw [Finsupp.sum_mapDomain_index] <;> simp [add_smul]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
S : Type u_10
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((b.constr S) f) x = (b.repr x).sum fun b a => a • f b

Tactic:
simp only [constr_def, LinearMap.comp_apply, lmapDomain_apply, linearCombination_apply]

Result:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
S : Type u_10
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ((mapDomain f (↑b.repr x)).sum fun i a => a • id i) = (b.repr x).sum fun b a => a • f b
-- Mathlib/Probability/Kernel/Basic.lean
lemma lintegral_id' {f : α → ℝ≥0∞} (hf : Measurable f) (a : α) :
    ∫⁻ a, f a ∂(@Kernel.id α mα a) = f a

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (a : α), f a ∂Kernel.id a = f a

Tactic:
rw [id_apply, lintegral_dirac' _ hf]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Pi.lean
lemma cauchy_pi_iff' {l : Filter (∀ i, α i)} [l.NeBot] :
    Cauchy l ↔ ∀ i, Cauchy (map (eval i) l)

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
l : Filter ((i : ι) → α i)
inst✝ : l.NeBot
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)

Tactic:
simp_rw [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace', cauchy_comap_uniformSpace]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma piAntidiag_insert [DecidableEq (ι → μ)] (hi : i ∉ s) (n : μ) :
    piAntidiag (insert i s) n = (antidiagonal n).biUnion fun p : μ × μ ↦ (piAntidiag s p.snd).image
      (fun f j ↦ f j + if j = i then p.fst else 0)

Proof state:
ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCancelCommMonoid μ
inst✝² : HasAntidiagonal μ
inst✝¹ : DecidableEq μ
i : ι
s : Finset ι
inst✝ : DecidableEq (ι → μ)
hi : i ∉ s
n : μ
⊢ (insert i s).piAntidiag n =
    (antidiagonal n).biUnion fun p => image (fun f j => f j + if j = i then p.1 else 0) (s.piAntidiag p.2)

Tactic:
simpa [map_eq_image, addRightEmbedding] using piAntidiag_cons hi n

Result:
no goals
-- Mathlib/CategoryTheory/Types.lean
theorem epi_iff_surjective {X Y : Type u} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f

Proof state:
X Y : Type u
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective f

Tactic:
constructor

Result:
case mp
X Y : Type u
f : X ⟶ Y
⊢ Epi f → Function.Surjective f

case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Surjective f → Epi f

Proof state:
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ f ≫ ⇑Equiv.ulift.symm ∘ g₁ = f ≫ ⇑Equiv.ulift.symm ∘ g₂

Tactic:
change ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f

Result:
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f

Proof state:
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ⇑Equiv.ulift.symm ∘ g₁ = ⇑Equiv.ulift.symm ∘ g₂

Tactic:
apply H

Result:
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ f ≫ ⇑Equiv.ulift.symm ∘ g₁ = f ≫ ⇑Equiv.ulift.symm ∘ g₂

Proof state:
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ g₁ = g₂

Tactic:
rw [← Equiv.ulift.symm.injective.comp_left.eq_iff]

Result:
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ⇑Equiv.ulift.symm ∘ g₁ = ⇑Equiv.ulift.symm ∘ g₂

Proof state:
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f

Tactic:
rw [hg]

Result:
no goals

Proof state:
case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Surjective f → Epi f

Tactic:
exact fun H => ⟨fun g g' h => H.injective_comp_right h⟩

Result:
no goals

Proof state:
case mp
X Y : Type u
f : X ⟶ Y
⊢ Epi f → Function.Surjective f

Tactic:
rintro ⟨H⟩

Result:
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
⊢ Function.Surjective f

Proof state:
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
⊢ Function.Surjective f

Tactic:
refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_

Result:
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ g₁ = g₂
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasStrictFDerivAt.sum (h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) :
    HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun p => A i p.1 - A i p.2 - (A' i) (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2
⊢ (fun p => ∑ i ∈ u, A i p.1 - ∑ i ∈ u, A i p.2 - (∑ i ∈ u, A' i) (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2

Tactic:
convert IsLittleO.sum h

Result:
case h.e'_7.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun p => A i p.1 - A i p.2 - (A' i) (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2
x✝ : E × E
⊢ ∑ i ∈ u, A i x✝.1 - ∑ i ∈ u, A i x✝.2 - (∑ i ∈ u, A' i) (x✝.1 - x✝.2) =
    ∑ i ∈ u, (A i x✝.1 - A i x✝.2 - (A' i) (x✝.1 - x✝.2))

Proof state:
case h.e'_7.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun p => A i p.1 - A i p.2 - (A' i) (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2
x✝ : E × E
⊢ ∑ i ∈ u, A i x✝.1 - ∑ i ∈ u, A i x✝.2 - (∑ i ∈ u, A' i) (x✝.1 - x✝.2) =
    ∑ i ∈ u, (A i x✝.1 - A i x✝.2 - (A' i) (x✝.1 - x✝.2))

Tactic:
simp [Finset.sum_sub_distrib, ContinuousLinearMap.sum_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x
⊢ HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Tactic:
simp only [hasStrictFDerivAt_iff_isLittleO] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun p => A i p.1 - A i p.2 - (A' i) (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2
⊢ (fun p => ∑ i ∈ u, A i p.1 - ∑ i ∈ u, A i p.2 - (∑ i ∈ u, A' i) (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem countP_toArray (p : α → Bool) (v : Vector α n) :
    v.toArray.countP p = v.countP p

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ Array.countP p v.toArray = countP p v

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.countP p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.countP p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem le_add_iff_sub_le {a b c : Int} : a ≤ b + c ↔ a - c ≤ b

Proof state:
a b c : Int
⊢ a + -c ≤ b ↔ a - c ≤ b

Tactic:
rfl

Result:
no goals

Proof state:
a b c : Int
⊢ a ≤ b + c ↔ a - c ≤ b

Tactic:
conv =>
  lhs
  rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]

Result:
a b c : Int
⊢ a + -c ≤ b ↔ a - c ≤ b
-- Mathlib/RingTheory/Algebraic/Cardinality.lean
theorem cardinalMk_le_sigma_polynomial :
    #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L })

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })

Tactic:
simpa only [lift_id] using lift_cardinalMk_le_sigma_polynomial R L

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma mul_prod_Iio_eq_prod_Iic (a : α) : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x

Tactic:
rw [Iic_eq_cons_Iio, prod_cons]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : EqvGen r a b) :
    EqvGen p a b

Proof state:
case trans
α : Type u_1
a✝² b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b c : α
a✝¹ : EqvGen r a b
a✝ : EqvGen r b c
hab : EqvGen p a b
hbc : EqvGen p b c
⊢ EqvGen p a c

Tactic:
exact EqvGen.trans _ _ _ hab hbc

Result:
no goals

Proof state:
case symm
α : Type u_1
a✝¹ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
a✝ : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a

Tactic:
exact EqvGen.symm _ _ ih

Result:
no goals

Proof state:
case rel
α : Type u_1
a✝ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : r a b
⊢ EqvGen p a b

Tactic:
exact EqvGen.rel _ _ (hrp _ _ h)

Result:
no goals

Proof state:
case refl
α : Type u_1
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
x✝ : α
⊢ EqvGen p x✝ x✝

Tactic:
exact EqvGen.refl _

Result:
no goals

Proof state:
α : Type u_1
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
⊢ EqvGen p a b

Tactic:
induction h with
| rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
| refl => exact EqvGen.refl _
| symm a b _ ih => exact EqvGen.symm _ _ ih
| trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Equivalence.lean
lemma eq_inducedTopology_of_isDenseSubsite [e.inverse.IsDenseSubsite K J] :
    K = e.inverse.inducedTopology J

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
⊢ K = e.inverse.inducedTopology J

Tactic:
ext

Result:
case h.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
x✝¹ : D
x✝ : Sieve x✝¹
⊢ x✝ ∈ K x✝¹ ↔ x✝ ∈ (e.inverse.inducedTopology J) x✝¹

Proof state:
case h.h.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
x✝¹ : D
x✝ : Sieve x✝¹
⊢ x✝ ∈ K x✝¹ ↔ x✝ ∈ (e.inverse.inducedTopology J) x✝¹

Tactic:
exact (e.inverse.functorPushforward_mem_iff K J).symm

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsStrictRestriction.ne (h : N <r M) : N ≠ M

Proof state:
α : Type u_1
N : Matroid α
h : N <r N
⊢ False

Tactic:
rw [← ofMatroid_lt_iff] at h

Result:
α : Type u_1
N : Matroid α
h : { toMatroid := N } < { toMatroid := N }
⊢ False

Proof state:
α : Type u_1
M N : Matroid α
h : N <r M
⊢ N ≠ M

Tactic:
rintro rfl

Result:
α : Type u_1
N : Matroid α
h : N <r N
⊢ False

Proof state:
α : Type u_1
N : Matroid α
h : { toMatroid := N } < { toMatroid := N }
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_eq_some_getElem_iff (a : Array α) (i : Nat) (h : i < a.size) :
    (a[i]? = some a[i]) ↔ True

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
⊢ a[i]? = some a[i] ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integral_comp_inv_smul (f : E → F) (R : ℝ) :
    ∫ x, f (R⁻¹ • x) ∂μ = |R ^ finrank ℝ E| • ∫ x, f x ∂μ

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ finrank ℝ E| • ∫ (x : E), f x ∂μ

Tactic:
rw [integral_comp_smul μ f R⁻¹, inv_pow, inv_inv]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
@[simp 1100, norm_cast]
lemma norm_intCast (n : ℤ) : ‖(n : ℂ)‖ = |(n : ℝ)|

Proof state:
n : ℤ
⊢ ‖↑n‖ = |↑n|

Tactic:
rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem getElem?_unattach {p : α → Prop} {l : Vector { x // p x } n} (i : Nat) :
    l.unattach[i]? = l[i]?.map Subtype.val

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector { x // p x } n
i : Nat
⊢ l.unattach[i]? = Option.map Subtype.val l[i]?

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[simp, norm_cast] lemma even_coe_nat (n : ℕ) : Even (n : ℤ) ↔ Even n

Proof state:
n : ℕ
⊢ Even ↑n ↔ Even n

Tactic:
rw_mod_cast [even_iff, Nat.even_iff]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem singleton_prod : ({a} : Set α) ×ˢ t = Prod.mk a '' t

Proof state:
α : Type u_1
β : Type u_2
t : Set β
a : α
⊢ {a} ×ˢ t = Prod.mk a '' t

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
t : Set β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ Prod.mk a '' t

Proof state:
case h.mk
α : Type u_1
β : Type u_2
t : Set β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ Prod.mk a '' t

Tactic:
simp [and_left_comm, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem toList_reverse (t : RBNode α) : t.reverse.toList = t.toList.reverse

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.toList = t.toList.reverse

Tactic:
induction t <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem T_inv_mul_apply_one (g : SL(2, ℤ)) : (T⁻¹ * g) 1 = g 1

Proof state:
g : SL(2, ℤ)
⊢ ↑(T⁻¹ * g) 1 = ↑g 1

Tactic:
simpa using T_pow_mul_apply_one (-1) g

Result:
no goals
-- Mathlib/Probability/Variance.lean
lemma variance_eq_integral (hX : AEMeasurable X μ) : Var[X; μ] = ∫ ω, (X ω - μ[X]) ^ 2 ∂μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ Var[X; μ] = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ

Tactic:
simp [variance, evariance, toReal_enorm, ← integral_toReal ((hX.sub_const _).enorm.pow_const _) <|
  .of_forall fun _ ↦ ENNReal.pow_lt_top enorm_lt_top _]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
theorem liftAlternating_ι (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (m : M) :
    liftAlternating (R := R) (M := M) (N := N) f (ι R m) = f 1 ![m]

Proof state:
case h.e_6.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ Matrix.vecCons m 0 = ![m]

Tactic:
rw [Matrix.zero_empty]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m) 0) 0 = (f 1) ![m]

Tactic:
rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (f (0 + 1)) (Matrix.vecCons m 0) = (f 1) ![m]

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (f (0 + 1)) (Matrix.vecCons m 0) = (f 1) ![m]

Tactic:
congr

Result:
case h.e_6.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ Matrix.vecCons m 0 = ![m]

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (liftAlternating f) ((ι R) m) = (f 1) ![m]

Tactic:
dsimp [liftAlternating]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m) 0) 0 = (f 1) ![m]
-- Mathlib/Data/Multiset/UnionInter.lean
theorem inter_replicate (s : Multiset α) (n : ℕ) (x : α) :
    s ∩ replicate n x = replicate (min (s.count x) n) x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ s ∩ replicate n x = replicate (count x s ⊓ n) x

Tactic:
rw [inter_comm, replicate_inter, min_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjCyclesSelfIso_inv_homologyπ  :
    (singleObjCyclesSelfIso _ _ _).inv ≫ ((single C c j).obj A).homologyπ j =
      (singleObjHomologySelfIso _ _ _).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjCyclesSelfIso c j A).inv ≫ ((single C c j).obj A).homologyπ j = (singleObjHomologySelfIso c j A).inv

Tactic:
simp [singleObjCyclesSelfIso, singleObjHomologySelfIso]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
@[to_additive (attr := simp) add_mem_addCentralizer]
lemma mul_mem_centralizer (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
    a * b ∈ centralizer S := fun g hg ↦ by
  rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]

Proof state:
M : Type u_1
S : Set M
inst✝ : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * (a * b) = a * b * g

Tactic:
rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]

Result:
no goals