harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean
theorem LinearMap.exists_map_addHaar_eq_smul_addHaar (h : Function.Surjective L) :
    ∃ (c : ℝ≥0∞), 0 < c ∧ μ.map L = c • ν

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
c : ℝ≥0∞
c_pos : 0 < c
hc : map (⇑L) μ = (c * addHaar univ) • ν
⊢ 0 < c * addHaar univ

Tactic:
simp [c_pos, NeZero.ne addHaar]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
⊢ ∃ c, 0 < c ∧ map (⇑L) μ = c • ν

Tactic:
rcases L.exists_map_addHaar_eq_smul_addHaar' μ ν h with ⟨c, c_pos, -, hc⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
c : ℝ≥0∞
c_pos : 0 < c
hc : map (⇑L) μ = (c * addHaar univ) • ν
⊢ ∃ c, 0 < c ∧ map (⇑L) μ = c • ν

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
c : ℝ≥0∞
c_pos : 0 < c
hc : map (⇑L) μ = (c * addHaar univ) • ν
⊢ ∃ c, 0 < c ∧ map (⇑L) μ = c • ν

Tactic:
exact ⟨_, by simp [c_pos, NeZero.ne addHaar], hc⟩

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem insert_diff_eq_singleton {a : α} {s : Set α} (h : a ∉ s) : insert a s \ s = {a}

Proof state:
case h
α : Type u
s : Set α
x✝ : α
h : x✝ ∉ s
⊢ x✝ ∉ s

Tactic:
exact h

Result:
no goals

Proof state:
case h
α : Type u
a : α
s : Set α
h : a ∉ s
x✝ : α
⊢ x✝ ∈ insert a s \ s ↔ x✝ ∈ {a}

Tactic:
rw [Set.mem_diff, Set.mem_insert_iff, Set.mem_singleton_iff, or_and_right, and_not_self_iff,
  or_false, and_iff_left_iff_imp]

Result:
case h
α : Type u
a : α
s : Set α
h : a ∉ s
x✝ : α
⊢ x✝ = a → x✝ ∉ s

Proof state:
α : Type u
a : α
s : Set α
h : a ∉ s
⊢ insert a s \ s = {a}

Tactic:
ext

Result:
case h
α : Type u
a : α
s : Set α
h : a ∉ s
x✝ : α
⊢ x✝ ∈ insert a s \ s ↔ x✝ ∈ {a}

Proof state:
case h
α : Type u
a : α
s : Set α
h : a ∉ s
x✝ : α
⊢ x✝ = a → x✝ ∉ s

Tactic:
rintro rfl

Result:
case h
α : Type u
s : Set α
x✝ : α
h : x✝ ∉ s
⊢ x✝ ∉ s
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem FinrankQuotientMap.span_eq_top [IsDomain R] [IsDomain S] [Algebra K L] [Module.Finite R S]
    [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Algebra.IsAlgebraic R S]
    [NoZeroSMulDivisors R K] (hp : p ≠ ⊤) (b : Set S)
    (hb' : Submodule.span R b ⊔ (p.map (algebraMap R S)).restrictScalars R = ⊤) :
    Submodule.span K (algebraMap S L '' b) = ⊤

Proof state:
case intro.intro.refine_1.calc_2
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : Algebra R S
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : NoZeroSMulDivisors R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
span_d : Submodule.restrictScalars R (Submodule.span S {(algebraMap R S) A.det}) ≤ M
this : Nontrivial (R ⧸ p)
⊢ (Matrix.det fun i j => (Quotient.mk p) (A' i j) - 1 i j) = (-1).det

Tactic:
refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)

Result:
case intro.intro.refine_1.calc_2
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : Algebra R S
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : NoZeroSMulDivisors R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
span_d : Submodule.restrictScalars R (Submodule.span S {(algebraMap R S) A.det}) ≤ M
this : Nontrivial (R ⧸ p)
i j : Fin n
⊢ (Quotient.mk p) (A' i j) - 1 i j = (-1) i j
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem FinrankQuotientMap.span_eq_top [IsDomain R] [IsDomain S] [Algebra K L] [Module.Finite R S]
    [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Algebra.IsAlgebraic R S]
    [NoZeroSMulDivisors R K] (hp : p ≠ ⊤) (b : Set S)
    (hb' : Submodule.span R b ⊔ (p.map (algebraMap R S)).restrictScalars R = ⊤) :
    Submodule.span K (algebraMap S L '' b) = ⊤

Proof state:
case intro
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : Algebra R S
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : NoZeroSMulDivisors R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ Submodule.span S {(algebraMap R S) A.det}
⊢ A.det • Submodule.Quotient.mk x' = 0

Tactic:
obtain ⟨a', _, quot_x_eq⟩ := exists_sum (Submodule.Quotient.mk x')

Result:
case intro.intro.intro
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : Algebra R S
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : NoZeroSMulDivisors R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j : Fin n, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ Submodule.span S {(algebraMap R S) A.det}
a' : Fin n → R
left✝ : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : ∑ i : Fin n, a' i • a i = Submodule.Quotient.mk x'
⊢ A.det • Submodule.Quotient.mk x' = 0
-- Mathlib/CategoryTheory/Functor/FunctorHom.lean
@[ext]
lemma functorHom_ext {X : C} {x y : (F.functorHom G).obj X}
    (h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f) : x = y :=
  HomObj.ext (by ext; apply h)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
⊢ x.app = y.app

Tactic:
ext

Result:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
x✝¹ : C
x✝ : (Opposite.unop (coyoneda.rightOp.obj X)).obj x✝¹
⊢ x.app x✝¹ x✝ = y.app x✝¹ x✝

Proof state:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
x✝¹ : C
x✝ : (Opposite.unop (coyoneda.rightOp.obj X)).obj x✝¹
⊢ x.app x✝¹ x✝ = y.app x✝¹ x✝

Tactic:
apply h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mulVec_surjective_iff_exists_right_inverse
    [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} :
    Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1

Proof state:
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
⊢ Function.Surjective A.mulVec ↔ ∃ B, A * B = 1

Tactic:
cases nonempty_fintype m

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
⊢ Function.Surjective A.mulVec ↔ ∃ B, A * B = 1

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
⊢ Function.Surjective A.mulVec ↔ ∃ B, A * B = 1

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
⊢ ∃ B, A * B = 1

Proof state:
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
x✝ : ∃ B, A * B = 1
y : m → R
B : Matrix n m R
hBA : A * B = 1
⊢ A *ᵥ B *ᵥ y = y

Tactic:
simp [hBA]

Result:
no goals

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = 1 i j

Tactic:
rw [one_eq_pi_single, Pi.single_comm, ← hcols j]

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = (A *ᵥ cols j) i

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
⊢ ∃ B, A * B = 1

Tactic:
refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩

Result:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = 1 i j

Proof state:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = (A *ᵥ cols j) i

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem compl_neighborSet_disjoint (G : SimpleGraph V) (v : V) :
    Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)

Proof state:
case intro
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : w ∈ Gᶜ.neighborSet v
⊢ w ∈ ∅

Tactic:
rw [mem_neighborSet, compl_adj] at h'

Result:
case intro
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : v ≠ w ∧ ¬G.Adj v w
⊢ w ∈ ∅

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)

Tactic:
rw [Set.disjoint_iff]

Result:
V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∩ Gᶜ.neighborSet v ⊆ ∅

Proof state:
case intro
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : v ≠ w ∧ ¬G.Adj v w
⊢ w ∈ ∅

Tactic:
exact h'.2 h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∩ Gᶜ.neighborSet v ⊆ ∅

Tactic:
rintro w ⟨h, h'⟩

Result:
case intro
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : w ∈ Gᶜ.neighborSet v
⊢ w ∈ ∅
-- Mathlib/Data/Set/Lattice.lean
theorem prod_sInter {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) :
    s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t

Tactic:
simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t

Tactic:
rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]

Result:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b ↔ (o = some b ∨ o = none ∧ a = b)

Proof state:
α : Type u_1
o : Option α
a b : α
⊢ o.getD a = b ↔ o = some b ∨ o = none ∧ a = b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
protected lemma Commute.pow_eq_pow_iff_of_coprime (hab : Commute a b) (hmn : m.Coprime n) :
    a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m

Proof state:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases m = 0

Result:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean
theorem coe_eq_algebraMap : (DoubleCentralizer.coe 𝕜 : 𝕜 → 𝓜(𝕜, 𝕜)) = algebraMap 𝕜 𝓜(𝕜, 𝕜)

Proof state:
case h.h.snd
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x y : 𝕜
⊢ (↑𝕜 x).toProd.2 y = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.2 y

Tactic:
exact mul_comm y x

Result:
no goals

Proof state:
case h.h.fst
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ (↑𝕜 x).toProd.1 = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.1

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ ↑𝕜 = ⇑(algebraMap 𝕜 𝓜(𝕜, 𝕜))

Tactic:
ext x : 3

Result:
case h.h.fst
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ (↑𝕜 x).toProd.1 = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.1

case h.h.snd
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ (↑𝕜 x).toProd.2 = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.2

Proof state:
case h.h.snd
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ (↑𝕜 x).toProd.2 = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.2

Tactic:
refine ContinuousLinearMap.ext fun y => ?_

Result:
case h.h.snd
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x y : 𝕜
⊢ (↑𝕜 x).toProd.2 y = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.2 y
-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), emultiplicity 2 n ! < n

Proof state:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n)! < ↑(2 * n) + 1

Tactic:
refine this.trans ?_

Result:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ ↑(2 * n) < ↑(2 * n) + 1
-- Mathlib/Order/Bounded.lean
theorem unbounded_lt_inter_le [LinearOrder α] (a : α) :
    Unbounded (· < ·) (s ∩ { b | a ≤ b }) ↔ Unbounded (· < ·) s

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Unbounded (fun x1 x2 => x1 < x2) (s ∩ {b | a ≤ b}) ↔ Unbounded (fun x1 x2 => x1 < x2) s

Tactic:
convert @unbounded_lt_inter_not_lt _ s _ a

Result:
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a ≤ x✝ ↔ ¬x✝ < a

Proof state:
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a ≤ x✝ ↔ ¬x✝ < a

Tactic:
exact not_lt.symm

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
lemma isIso_of_isIso_map {X Y : C} (f : X ⟶ Y) [IsIso (F.map f)] :
    IsIso f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ IsIso f

Tactic:
simpa using (hF.preimageIso (asIso (F.map f))).isIso_hom

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem cantor (a : Cardinal.{u}) : a < 2 ^ a

Proof state:
case h.intro.mk
α : Type u
f : Set α → α
hf : Injective f
⊢ False

Tactic:
exact cantor_injective f hf

Result:
no goals

Proof state:
case h
α : Type u
⊢ #α < #(Set α)

Tactic:
refine ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, ?_⟩

Result:
case h
α : Type u
⊢ ¬Quotient.liftOn₂ (#(Set α)) (#α) (fun α β => Nonempty (α ↪ β)) instLE.proof_1

Proof state:
case h
α : Type u
⊢ ¬Quotient.liftOn₂ (#(Set α)) (#α) (fun α β => Nonempty (α ↪ β)) instLE.proof_1

Tactic:
rintro ⟨⟨f, hf⟩⟩

Result:
case h.intro.mk
α : Type u
f : Set α → α
hf : Injective f
⊢ False

Proof state:
case h
α : Type u
⊢ #α < 2 ^ #α

Tactic:
rw [← mk_set]

Result:
case h
α : Type u
⊢ #α < #(Set α)

Proof state:
a : Cardinal.{u}
⊢ a < 2 ^ a

Tactic:
induction' a using Cardinal.inductionOn with α

Result:
case h
α : Type u
⊢ #α < 2 ^ #α
-- Mathlib/Order/InitialSeg.lean
theorem lt_apply_iff [LinearOrder α] (f : α ≤i β) : b < f a ↔ ∃ a' < a, f a' = b

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b < f a
c : α
hc : f c = b
⊢ ∃ a' < a, f a' = b

Tactic:
refine ⟨c, ?_, hc⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b < f a
c : α
hc : f c = b
⊢ c < a

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b < f a
c : α
hc : f c = b
⊢ c < a

Tactic:
rwa [← hc, f.lt_iff_lt] at h

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ b < f a → ∃ a' < a, f a' = b

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b < f a
⊢ ∃ a' < a, f a' = b

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b < f a
⊢ ∃ a' < a, f a' = b

Tactic:
obtain ⟨c, hc⟩ := f.mem_range_of_rel h

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b < f a
c : α
hc : f c = b
⊢ ∃ a' < a, f a' = b

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
c : α
hc : c < a
⊢ f c < f a

Tactic:
exact f.strictMono hc

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ b < f a ↔ ∃ a' < a, f a' = b

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ b < f a → ∃ a' < a, f a' = b

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ (∃ a' < a, f a' = b) → b < f a

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ (∃ a' < a, f a' = b) → b < f a

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
c : α
hc : c < a
⊢ f c < f a