harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Martingale/OptionalStopping.lean
theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnonneg : 0 ≤ f) {ε : ℝ≥0}
    (n : ℕ) : ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω} ≤
    ENNReal.ofReal (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω},
      f n ω ∂μ)

Proof state:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₁ : ω ∈ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}
hω₂ : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
⊢ ω ∈ ⊥

Tactic:
change (ε : ℝ) ≤ _ at hω₁

Result:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₂ : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
hω₁ : ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω
⊢ ω ∈ ⊥

Proof state:
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ⊓ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε} ≤ ⊥

Tactic:
rintro ω ⟨hω₁, hω₂⟩

Result:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω₁ : ω ∈ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}
hω₂ : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
⊢ ω ∈ ⊥
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem fromSpec_image_basicOpen :
    hU.fromSpec ''ᵁ (PrimeSpectrum.basicOpen f) = X.basicOpen f

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(X.basicOpen f) ⊆ ↑U

Tactic:
exact Scheme.basicOpen_le _ _

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) '' (⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen f)) =
    ↑(X.basicOpen f)

Tactic:
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, hU.range_fromSpec]

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(X.basicOpen f) ⊆ ↑U

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f) = ↑(X.basicOpen f)

Tactic:
change hU.fromSpec.base '' (hU.fromSpec.base ⁻¹' (X.basicOpen f : Set X)) = _

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) '' (⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen f)) =
    ↑(X.basicOpen f)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f

Tactic:
rw [← hU.fromSpec_preimage_basicOpen]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f

Tactic:
ext1

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ ↑(hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f) = ↑(X.basicOpen f)
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem abs_areaForm_le (x y : E) : |ω x y| ≤ ‖x‖ * ‖y‖

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ |(o.areaForm x) y| ≤ ‖x‖ * ‖y‖

Tactic:
simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.abs_volumeForm_apply_le ![x, y]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma toCLM_injective : Function.Injective (toCLM (A := A) (m := m) (n := n))

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
h : toCLM M = 0
⊢ M = 0

Tactic:
ext i j

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ M i j = 0 i j

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
⊢ Function.Injective ⇑toCLM

Tactic:
classical
rw [injective_iff_map_eq_zero]
intro M h
ext i j
rw [Matrix.zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_self_mul_star,
  ← toCLM_apply_single_apply]
simp [h]

Result:
no goals

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ M i j = 0 i j

Tactic:
rw [Matrix.zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_self_mul_star,
  ← toCLM_apply_single_apply]

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ ‖(toCLM M) ((WithCStarModule.equiv (n → A)).symm (Pi.single j (star (M i j)))) i‖ = 0

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
⊢ Function.Injective ⇑toCLM

Tactic:
rw [injective_iff_map_eq_zero]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
⊢ ∀ (a : CStarMatrix m n A), toCLM a = 0 → a = 0

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ ‖(toCLM M) ((WithCStarModule.equiv (n → A)).symm (Pi.single j (star (M i j)))) i‖ = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
⊢ ∀ (a : CStarMatrix m n A), toCLM a = 0 → a = 0

Tactic:
intro M h

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
h : toCLM M = 0
⊢ M = 0
-- Mathlib/Topology/Connected/Clopen.lean
theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (π i)] {s : Set (Σi, π i)} :
    IsConnected s ↔ ∃ i t, IsConnected t ∧ s = Sigma.mk i '' t

Proof state:
case refine_2.intro.intro.intro
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
t : Set (π i)
ht : IsConnected t
⊢ IsConnected (mk i '' t)

Tactic:
exact ht.image _ continuous_sigmaMk.continuousOn

Result:
no goals

Proof state:
case refine_1.intro.mk
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsConnected s
i : ι
x : π i
hx : ⟨i, x⟩ ∈ s
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
have : s ⊆ range (Sigma.mk i) :=
  hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩

Result:
case refine_1.intro.mk
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsConnected s
i : ι
x : π i
hx : ⟨i, x⟩ ∈ s
this : s ⊆ range (mk i)
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Proof state:
case refine_1
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsConnected s
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty

Result:
case refine_1.intro.mk
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsConnected s
i : ι
x : π i
hx : ⟨i, x⟩ ∈ s
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Proof state:
case refine_2
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
⊢ (∃ i t, IsConnected t ∧ s = mk i '' t) → IsConnected s

Tactic:
rintro ⟨i, t, ht, rfl⟩

Result:
case refine_2.intro.intro.intro
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
t : Set (π i)
ht : IsConnected t
⊢ IsConnected (mk i '' t)

Proof state:
case refine_1.intro.mk
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsConnected s
i : ι
x : π i
hx : ⟨i, x⟩ ∈ s
this : s ⊆ range (mk i)
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
exact ⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_isOpenMap sigma_mk_injective isOpenMap_sigmaMk this,
  (Set.image_preimage_eq_of_subset this).symm⟩

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
⊢ IsConnected s ↔ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩

Result:
case refine_1
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsConnected s
⊢ ∃ i t, IsConnected t ∧ s = mk i '' t

case refine_2
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
⊢ (∃ i t, IsConnected t ∧ s = mk i '' t) → IsConnected s
-- Mathlib/CategoryTheory/Preadditive/LeftExact.lean
/-- A functor between preadditive categories preserves the equalizer of two
morphisms if it preserves all kernels. -/
lemma preservesEqualizer_of_preservesKernels
    [∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F]
    {X Y : C} (f g : X ⟶ Y) : PreservesLimit (parallelPair f g) F

Proof state:
case preserves.val
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := isLimitForkMapOfIsLimit' F ⋯ c'
⊢ IsLimit (F.mapCone c)

Tactic:
apply IsLimit.ofIsoLimit _ ((Cones.functoriality _ F).mapIso (Fork.isoForkOfι c).symm)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := isLimitForkMapOfIsLimit' F ⋯ c'
⊢ IsLimit ((Cones.functoriality (parallelPair f g) F).obj (Fork.ofι (Fork.ι c) ⋯))
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_succ_right (n : ℕ) :
    ascPochhammer S (n + 1) = ascPochhammer S n * (X + (n : S[X]))

Proof state:
case succ
S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
⊢ ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * (X + ↑(n + 1))

Tactic:
conv_lhs =>
  rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
      X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]

Result:
no goals

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * (X + ↑n)

Tactic:
apply_fun Polynomial.map (algebraMap ℕ S) at h

Result:
S : Type u
inst✝ : Semiring S
n : ℕ
h : map (algebraMap ℕ S) (ascPochhammer ℕ (n + 1)) = map (algebraMap ℕ S) (ascPochhammer ℕ n * (X + ↑n))
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * (X + ↑n)

Proof state:
case zero
S : Type u
inst✝ : Semiring S
⊢ ascPochhammer ℕ (0 + 1) = ascPochhammer ℕ 0 * (X + ↑0)

Tactic:
simp

Result:
no goals

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * (X + ↑n)

Tactic:
suffices h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + (n : ℕ[X])) by
  apply_fun Polynomial.map (algebraMap ℕ S) at h
  simpa only [ascPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
    Polynomial.map_natCast] using h

Result:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  conv_lhs =>
    rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
        X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]

Result:
no goals

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
h : map (algebraMap ℕ S) (ascPochhammer ℕ (n + 1)) = map (algebraMap ℕ S) (ascPochhammer ℕ n * (X + ↑n))
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * (X + ↑n)

Tactic:
simpa only [ascPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
  Polynomial.map_natCast] using h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[simp] lemma sum_extend_zero {ι ι' : Type*} {f : ι → ι'} (hf : Injective f) (m : ι → Measure α) :
    sum (Function.extend f m 0) = sum m

Proof state:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
⊢ sum (Function.extend f m 0) = sum m

Tactic:
ext s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum (Function.extend f m 0)) s = (sum m) s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum (Function.extend f m 0)) s = (sum m) s

Tactic:
simp [*, Function.apply_extend (fun μ : Measure α ↦ μ s)]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_eval_eq_apply (f : M₁ →ₗ[R] M₂) (i : ι₂) (c : ι₁ →₀ R) :
    eval c (f.toMvPolynomial b₁ b₂ i) = b₂.repr (f (b₁.repr.symm c)) i

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
c : ι₁ →₀ R
⊢ (eval ⇑c) (toMvPolynomial b₁ b₂ f i) = (b₂.repr (f (b₁.repr.symm c))) i

Tactic:
rw [toMvPolynomial, Matrix.toMvPolynomial_eval_eq_apply,
  ← LinearMap.toMatrix_mulVec_repr b₁ b₂, LinearEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem ω_mul_ωb (q : ℕ+) : (ω : X q) * ωb = 1

Proof state:
case h₁
q : ℕ+
⊢ 2 * 2 + -3 = 1

Tactic:
ring

Result:
no goals

Proof state:
q : ℕ+
⊢ (2, 1) * (2, -1) = 1

Tactic:
ext <;> simp

Result:
case h₁
q : ℕ+
⊢ 2 * 2 + -3 = 1

Proof state:
q : ℕ+
⊢ ω * ωb = 1

Tactic:
dsimp [ω, ωb]

Result:
q : ℕ+
⊢ (2, 1) * (2, -1) = 1
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem IsClosed.pathComponent (x : X) : IsClosed (pathComponent x)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
⊢ ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1

Tactic:
intro y hxy

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
⊢ (pathComponent x)ᶜ ∈ 𝓝 y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
⊢ IsClosed (pathComponent x)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
⊢ ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
z : X
hz : z ∈ V
hxz : z ∈ pathComponent x
⊢ False

Tactic:
exact hxy <|  hxz.trans (hVc.joinedIn _ hz _ (mem_of_mem_nhds hVy)).joined

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
⊢ (pathComponent x)ᶜ ∈ 𝓝 y

Tactic:
filter_upwards [hVy] with z hz hxz

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
z : X
hz : z ∈ V
hxz : z ∈ pathComponent x
⊢ False

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
⊢ (pathComponent x)ᶜ ∈ 𝓝 y

Tactic:
rcases (path_connected_basis y).ex_mem with ⟨V, hVy, hVc⟩

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
⊢ (pathComponent x)ᶜ ∈ 𝓝 y
-- Mathlib/Topology/JacobsonSpace.lean
lemma jacobsonSpace_iff_locallyClosed :
    JacobsonSpace X ↔ ∀ Z, Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure (closure Z ∩ closedPoints X) ⊆ closure Z \ Z

Tactic:
rw [hZ'.closure_subset_iff, Set.subset_diff, Set.disjoint_iff, Set.inter_assoc,
  Set.inter_comm _ Z, e]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure Z ∩ closedPoints X ⊆ closure Z ∧ closure Z ∩ ∅ ⊆ ∅

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure Z ∧ Z = ∅
⊢ False

Tactic:
exact hZ this.2

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure Z ⊆ closure Z \ Z

Tactic:
nth_rw 1 [← H isClosed_closure]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure (closure Z ∩ closedPoints X) ⊆ closure Z \ Z

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
H' : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ¬Z ∩ closedPoints X ⊆ closure (Z ∩ closedPoints X)
⊢ False

Tactic:
exact this subset_closure

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp]
lemma isNClique_singleton : G.IsNClique n {a} ↔ n = 1

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
a : α
⊢ G.IsNClique n {a} ↔ n = 1

Tactic:
simp [isNClique_iff, eq_comm]

Result:
no goals
-- Mathlib/Analysis/Convex/Quasiconvex.lean
theorem QuasiconvexOn.sup [SemilatticeSup β] (hf : QuasiconvexOn 𝕜 s f)
    (hg : QuasiconvexOn 𝕜 s g) : QuasiconvexOn 𝕜 s (f ⊔ g)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ (f ⊔ g) x ≤ r}

Tactic:
simp_rw [Pi.sup_def, sup_le_iff, Set.sep_and]

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ r} ∩ {x | x ∈ s ∧ g x ≤ r})

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ r} ∩ {x | x ∈ s ∧ g x ≤ r})

Tactic:
exact (hf r).inter (hg r)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
⊢ QuasiconvexOn 𝕜 s (f ⊔ g)

Tactic:
intro r

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ (f ⊔ g) x ≤ r}
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem mem_setOfIdeal {I : Ideal C(X, R)} {x : X} :
    x ∈ setOfIdeal I ↔ ∃ f ∈ I, (f : C(X, R)) x ≠ 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (∃ f ∈ I, f x ≠ 0) ↔ ∃ f ∈ I, f x ≠ 0

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∈ setOfIdeal I ↔ ∃ f ∈ I, f x ≠ 0

Tactic:
simp_rw [setOfIdeal, Set.mem_compl_iff, Set.mem_setOf]

Result:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (¬∀ f ∈ I, f x = 0) ↔ ∃ f ∈ I, f x ≠ 0

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (¬∀ f ∈ I, f x = 0) ↔ ∃ f ∈ I, f x ≠ 0

Tactic:
push_neg

Result:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (∃ f ∈ I, f x ≠ 0) ↔ ∃ f ∈ I, f x ≠ 0