harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_and_epi_g_iff_g_is_cokernel [S.HasHomology] :
    S.Exact ∧ Epi S.g ↔ Nonempty (IsColimit (CokernelCofork.ofπ S.g S.zero))

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : S.Exact
right✝ : Epi S.g
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

Tactic:
exact ⟨hS.gIsCokernel⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
⊢ S.Exact ∧ Epi S.g

Tactic:
exact ⟨S.exact_of_g_is_cokernel hS, epi_of_isColimit_cofork hS⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g

Tactic:
intro ⟨hS⟩

Result:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
⊢ S.Exact ∧ Epi S.g

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Epi S.g ↔ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Epi S.g → Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Epi S.g → Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

Tactic:
intro ⟨hS, _⟩

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : S.Exact
right✝ : Epi S.g
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_top : (⊤ : AffineSubspace k P).direction = ⊤

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
⊢ ⊤.direction = ⊤

Tactic:
obtain ⟨p⟩ := S.nonempty

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
⊢ ⊤.direction = ⊤

Proof state:
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
v : V
⊢ v ∈ ⊤.direction ↔ v ∈ ⊤

Tactic:
refine ⟨imp_intro Submodule.mem_top, fun _hv => ?_⟩

Result:
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
v : V
_hv : v ∈ ⊤
⊢ v ∈ ⊤.direction

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
⊢ ⊤.direction = ⊤

Tactic:
ext v

Result:
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
v : V
⊢ v ∈ ⊤.direction ↔ v ∈ ⊤

Proof state:
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
v : V
_hv : v ∈ ⊤
hpv : (v +ᵥ p) -ᵥ p ∈ ⊤.direction
⊢ v ∈ ⊤.direction

Tactic:
rwa [vadd_vsub] at hpv

Result:
no goals

Proof state:
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
v : V
_hv : v ∈ ⊤
⊢ v ∈ ⊤.direction

Tactic:
have hpv : ((v +ᵥ p) -ᵥ p : V) ∈ (⊤ : AffineSubspace k P).direction :=
  vsub_mem_direction (mem_top k V _) (mem_top k V _)

Result:
case intro.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
v : V
_hv : v ∈ ⊤
hpv : (v +ᵥ p) -ᵥ p ∈ ⊤.direction
⊢ v ∈ ⊤.direction
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureInt_vars [Fintype idx] (Φ : MvPolynomial idx ℤ) (n : ℕ) :
    (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
have : Function.Injective (Int.castRingHom ℚ) := Int.cast_injective

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
apply wittStructureRat_vars

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
rw [← vars_map_of_injective _ this, map_wittStructureInt]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib/Logic/Function/Conjugate.lean
theorem comp {f' : β → γ} {gc : γ → γ → γ} (hf' : Semiconj₂ f' gb gc) (hf : Semiconj₂ f ga gb) :
    Semiconj₂ (f' ∘ f) ga gc := fun x y ↦ by simp only [hf'.eq, hf.eq, comp_apply]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
f' : β → γ
gc : γ → γ → γ
hf' : Semiconj₂ f' gb gc
hf : Semiconj₂ f ga gb
x y : α
⊢ (f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)

Tactic:
simp only [hf'.eq, hf.eq, comp_apply]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_neg_right : (f =o[l] fun x => -g' x) ↔ f =o[l] g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =o[l] fun x => -g' x) ↔ f =o[l] g'

Tactic:
simp only [IsLittleO_def]

Result:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f fun x => -g' x) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f fun x => -g' x) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_neg_right

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem ofReal_inv_of_pos {x : ℝ} (hx : 0 < x) : ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹

Proof state:
x : ℝ
hx : 0 < x
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
  ← Real.toNNReal_inv]

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
⊢ x.toNNReal ≠ 0

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_ideal_over_prime_of_isIntegral [Algebra.IsIntegral R S] (P : Ideal R) [IsPrime P]
    (I : Ideal S) (hIP : I.comap (algebraMap R S) ≤ P) :
    ∃ Q ≥ I, IsPrime Q ∧ Q.comap (algebraMap R S) = P

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
have ⟨P', hP, hP', hP''⟩ := exists_ideal_comap_le_prime P I hIP

Result:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (algebraMap R S) P' ≤ P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (algebraMap R S) P' ≤ P
Q : Ideal S
hQ : Q ≥ P'
hQ' : Q.IsPrime
hQ'' : comap (algebraMap R S) Q = P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
exact ⟨Q, hP.trans hQ, hQ', hQ''⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (algebraMap R S) P' ≤ P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
obtain ⟨Q, hQ, hQ', hQ''⟩ := exists_ideal_over_prime_of_isIntegral_of_isPrime P P' hP''

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hIP : comap (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (algebraMap R S) P' ≤ P
Q : Ideal S
hQ : Q ≥ P'
hQ' : Q.IsPrime
hQ'' : comap (algebraMap R S) Q = P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q = P
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem smul_eq_C_mul (f : R⟦X⟧) (a : R) : a • f = C R a * f

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a : R
n✝ : ℕ
⊢ (coeff R n✝) (a • f) = (coeff R n✝) ((C R) a * f)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a : R
⊢ a • f = (C R) a * f

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a : R
n✝ : ℕ
⊢ (coeff R n✝) (a • f) = (coeff R n✝) ((C R) a * f)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Y_ne_zero_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P)
    (hPz : P z = 0) : P y ≠ 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P y ≠ 0

Tactic:
intro hPy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPy : P y = 0
⊢ False

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPy : P y = 0
⊢ False

Tactic:
simp only [nonsingular_of_Z_eq_zero hPz, X_eq_zero_of_Z_eq_zero hP.left hPz, hPy, add_zero,
  sub_zero, mul_zero, zero_pow two_ne_zero, or_self, ne_self_iff_false, and_false] at hP

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_zero [HasZeroMorphisms C] {X Y : C} {P : Subobject Y}
    (h : P.Factors (0 : X ⟶ Y)) : P.factorThru 0 h = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : P.Factors 0
⊢ P.factorThru 0 h = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem min_comm (a b : Int) : min a b = min b a

Proof state:
case pos
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ a = b

Tactic:
exact Int.le_antisymm h₁ h₂

Result:
no goals

Proof state:
a b : Int
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

Tactic:
by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]

Result:
case pos
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ a = b

case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ b = a

Proof state:
case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ b = a

Tactic:
cases not_or_intro h₁ h₂ <| Int.le_total ..

Result:
no goals

Proof state:
a b : Int
⊢ min a b = min b a

Tactic:
simp [Int.min_def]

Result:
a b : Int
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
-- Mathlib/Topology/Perfect.lean
theorem Perfect.splitting [T25Space α] (hC : Perfect C) (hnonempty : C.Nonempty) :
    ∃ C₀ C₁ : Set α,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
⊢ ∃ x ∈ C, x ≠ y

Tactic:
rcases this univ univ_mem with ⟨x, xC, hxy⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
x : α
xC : x ∈ univ ∩ C
hxy : x ≠ y
⊢ ∃ x ∈ C, x ≠ y

Proof state:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x, xC, hxy⟩ : ∃ x ∈ C, x ≠ y := by
  have := hC.acc _ yC
  rw [accPt_iff_nhds] at this
  rcases this univ univ_mem with ⟨x, xC, hxy⟩
  exact ⟨x, xC.2, hxy⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Proof state:
case h.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ closure (V ∩ C) ⊆ C

Tactic:
rw [hC.closed.closure_subset_iff]

Result:
case h.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ V ∩ C ⊆ C

Proof state:
case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ closure (U ∩ C) ⊆ C

Tactic:
rw [hC.closed.closure_subset_iff]

Result:
case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ U ∩ C ⊆ C

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ U ∈ 𝓝 y, ∃ y_1 ∈ U ∩ C, y_1 ≠ y
x : α
xC : x ∈ univ ∩ C
hxy : x ≠ y
⊢ ∃ x ∈ C, x ≠ y

Tactic:
exact ⟨x, xC.2, hxy⟩

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem powersetCard_zero (s : Finset α) : s.powersetCard 0 = {∅}

Proof state:
α : Type u_1
s : Finset α
⊢ powersetCard 0 s = {∅}

Tactic:
ext

Result:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ∈ powersetCard 0 s ↔ a✝ ∈ {∅}

Proof state:
α : Type u_1
s a✝ : Finset α
h : a✝ = ∅
⊢ ∅ ⊆ s ∧ ∅ = ∅

Tactic:
exact ⟨empty_subset s, rfl⟩

Result:
no goals

Proof state:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ a✝ = ∅ ↔ a✝ = ∅

Tactic:
refine
  ⟨fun h => h.2, fun h => by
    rw [h]
    exact ⟨empty_subset s, rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_1
s a✝ : Finset α
h : a✝ = ∅
⊢ a✝ ⊆ s ∧ a✝ = ∅

Tactic:
rw [h]

Result:
α : Type u_1
s a✝ : Finset α
h : a✝ = ∅
⊢ ∅ ⊆ s ∧ ∅ = ∅

Proof state:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ∈ powersetCard 0 s ↔ a✝ ∈ {∅}

Tactic:
rw [mem_powersetCard, mem_singleton, card_eq_zero]

Result:
case h
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ a✝ = ∅ ↔ a✝ = ∅
-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma disjoint_span_singleton_of_not_mem (hx : x ∉ s) : Disjoint s (K ∙ x)

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ∉ s
⊢ x ∈ s → x = 0

Tactic:
intro h

Result:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ∉ s
h : x ∈ s
⊢ x = 0

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ∉ s
h : x ∈ s
⊢ x = 0

Tactic:
contradiction

Result:
no goals

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ∉ s
⊢ Disjoint s (span K {x})

Tactic:
rw [disjoint_span_singleton]

Result:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hx : x ∉ s
⊢ x ∈ s → x = 0
-- Mathlib/Probability/Density.lean
theorem integrable_pdf_smul_iff [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → F}
    (hf : AEStronglyMeasurable f μ) :
    Integrable (fun x => (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable (fun x => f (X x)) ℙ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable f (map X ℙ) ↔ Integrable f (μ.withDensity ((map X ℙ).rnDeriv μ))

Tactic:
rw [withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous]

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable (fun x => (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable (fun x => f (X x)) ℙ

Tactic:
rw [← Function.comp_def,
  ← integrable_map_measure (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),
  map_eq_withDensity_pdf X ℙ μ, pdf_def, integrable_rnDeriv_smul_iff HasPDF.absolutelyContinuous]

Result:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable f (map X ℙ) ↔ Integrable f (μ.withDensity ((map X ℙ).rnDeriv μ))
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.nhdsSet_inf_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) :
    (𝓝ˢ K) ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l

Proof state:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
this : ∀ (f : Filter X), f ⊓ l = comap (fun x => (x, x)) (f ×ˢ l)
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l

Tactic:
simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem inf_relrank_left : relrank (A ⊓ B) A = relrank B A

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
rw [inf_comm, inf_relrank_right]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
/-- This lemma allows the computation of the connecting homomorphism
`D.δ` when `D : SnakeInput C` and `C` is a concrete category. -/
lemma δ_apply' (x₃ : (forget₂ C Ab).obj D.L₀.X₃)
    (x₂ : (forget₂ C Ab).obj D.L₁.X₂) (x₁ : (forget₂ C Ab).obj D.L₂.X₁)
    (h₂ : (forget₂ C Ab).map D.L₁.g x₂ = (forget₂ C Ab).map D.v₀₁.τ₃ x₃)
    (h₁ : (forget₂ C Ab).map D.L₂.f x₁ = (forget₂ C Ab).map D.v₁₂.τ₂ x₂) :
    (forget₂ C Ab).map D.δ x₃ = (forget₂ C Ab).map D.v₂₃.τ₁ x₁

Proof state:
case a.refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
e : forget₂ C Ab ⋙ forget Ab ≅ forget C
⊢ ((forget₂ C Ab ⋙ forget Ab).map D.L₁.g ≫ e.hom.app D.L₁.X₃) x₂ =
    ((forget₂ C Ab ⋙ forget Ab).map D.v₀₁.τ₃ ≫ e.hom.app D.L₁.X₃) x₃

Tactic:
dsimp

Result:
case a.refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
e : forget₂ C Ab ⋙ forget Ab ≅ forget C
⊢ e.hom.app D.L₁.X₃ ((ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂) =
    e.hom.app D.L₁.X₃ ((ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃)
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem pow_add : I ^ (m + n) = I ^ m * I ^ n

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
exact Submodule.pow_add _ h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
obtain rfl | h := eq_or_ne n 0

Result:
case inl
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m : ℕ
⊢ I ^ (m + 0) = I ^ m * I ^ 0

case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m : ℕ
⊢ I ^ (m + 0) = I ^ m * I ^ 0

Tactic:
rw [add_zero, Submodule.pow_zero, IsTwoSided.mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n

Proof state:
α : Type u
n : Nat
a : α
⊢ (replicate n a).length = n

Tactic:
induction n with
| zero => simp
| succ n ih => simp only [ih, replicate_succ, length_cons, Nat.succ_eq_add_one]

Result:
no goals

Proof state:
case succ
α : Type u
a : α
n : Nat
ih : (replicate n a).length = n
⊢ (replicate (n + 1) a).length = n + 1

Tactic:
simp only [ih, replicate_succ, length_cons, Nat.succ_eq_add_one]

Result:
no goals

Proof state:
case zero
α : Type u
a : α
⊢ (replicate 0 a).length = 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem iUnion_spanningSets (μ : Measure α) [SigmaFinite μ] : ⋃ i : ℕ, spanningSets μ i = univ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ ⋃ i, spanningSets μ i = univ

Tactic:
simp_rw [spanningSets, iUnion_accumulate, μ.toFiniteSpanningSetsIn.spanning]

Result:
no goals