harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
/-- A convenience variant of `LinearMap.BilinForm.nondegenerate_iff` characterising nondegeneracy as
positive definiteness. -/
lemma nondegenerate_iff' (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm) :
    B.Nondegenerate ↔ ∀ x, x ≠ 0 → 0 < B x x

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ (¬∀ (x : M), (B x) x = 0 ↔ x = 0) ↔ ¬∀ (x : M), x ≠ 0 → 0 < (B x) x

Tactic:
push_neg

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ (∃ x, (B x) x = 0 ∧ x ≠ 0 ∨ (B x) x ≠ 0 ∧ x = 0) ↔ ∃ x, x ≠ 0 ∧ (B x) x ≤ 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
⊢ (B x) x = 0 ∧ x ≠ 0 ∨ (B x) x ≠ 0 ∧ x = 0 → x ≠ 0 ∧ (B x) x ≤ 0

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ (∃ x, (B x) x = 0 ∧ x ≠ 0 ∨ (B x) x ≠ 0 ∧ x = 0) ↔ ∃ x, x ≠ 0 ∧ (B x) x ≤ 0

Tactic:
exact exists_congr fun x ↦ ⟨by aesop, fun ⟨h₀, h⟩ ↦ Or.inl ⟨le_antisymm h (hs x), h₀⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ Nondegenerate B ↔ ∀ (x : M), x ≠ 0 → 0 < (B x) x

Tactic:
rw [B.nondegenerate_iff hs hB, ← not_iff_not]

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ (¬∀ (x : M), (B x) x = 0 ↔ x = 0) ↔ ¬∀ (x : M), x ≠ 0 → 0 < (B x) x
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem continuousLinearMapAt_model_space (b b' : F) :
    (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).continuousLinearMapAt 𝕜 b' = (1 : F →L[𝕜] F)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' : F
⊢ Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b' = 1

Tactic:
rw [TangentBundle.trivializationAt_continuousLinearMapAt, coordChange_model_space]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' : F
⊢ b' ∈ (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).baseSet

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
b b' : F
⊢ b' ∈ (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).baseSet

Tactic:
apply mem_univ

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem eval_range {ι : Type*} [Finite ι] (b : Basis ι R M) :
    LinearMap.range (Dual.eval R M) = ⊤

Proof state:
case intro
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ range (Dual.eval R M) = ⊤

Tactic:
rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
⊢ range (Dual.eval R M) = ⊤

Tactic:
classical
  cases nonempty_fintype ι
  rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
⊢ range (Dual.eval R M) = ⊤

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ range (Dual.eval R M) = ⊤
-- Mathlib/LinearAlgebra/Orientation.lean
theorem adjustToOrientation_apply_eq_or_eq_neg [Nonempty ι] (e : Basis ι R M)
    (x : Orientation R M ι) (i : ι) :
    e.adjustToOrientation x i = e i ∨ e.adjustToOrientation x i = -e i

Proof state:
case pos
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : e.orientation = x
⊢ e i = e i ∨ e i = -e i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
⊢ (if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = e i ∨
    (if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = -e i

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : e.orientation = x
⊢ e i = e i ∨ e i = -e i

case neg
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : ¬e.orientation = x
⊢ (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = e i ∨
    (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = -e i

Proof state:
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
⊢ (e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i

Tactic:
rw [adjustToOrientation]

Result:
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
⊢ (if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = e i ∨
    (if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = -e i

Proof state:
case neg
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : ¬e.orientation = x
⊢ (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = e i ∨
    (e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))) i = -e i

Tactic:
by_cases hi : i = Classical.arbitrary ι <;> simp [unitsSMul_apply, hi]

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma coborder_inter_closure :
    coborder s ∩ closure s = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s ∩ closure s = s

Tactic:
rw [coborder, ← diff_eq_compl_inter, diff_diff_right_self, inter_eq_right]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ closure s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ closure s

Tactic:
exact subset_closure

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma subsingleton_of_ediam_eq_zero (h : G.ediam = 0) : Subsingleton α

Proof state:
α : Type u_1
G : SimpleGraph α
h : ¬Subsingleton α
⊢ G.ediam ≠ 0

Tactic:
apply not_subsingleton_iff_nontrivial.mp at h

Result:
α : Type u_1
G : SimpleGraph α
h : Nontrivial α
⊢ G.ediam ≠ 0

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.ediam = 0
⊢ Subsingleton α

Tactic:
contrapose! h

Result:
α : Type u_1
G : SimpleGraph α
h : ¬Subsingleton α
⊢ G.ediam ≠ 0

Proof state:
α : Type u_1
G : SimpleGraph α
h : Nontrivial α
⊢ G.ediam ≠ 0

Tactic:
exact ediam_ne_zero

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
/-- If `X` is compactly generated, to prove that `f : X → Y` is continuous it is enough to show
that for every compact Hausdorff space `K` and every continuous map `g : K → X`,
`f ∘ g` is continuous. -/
lemma continuous_from_uCompactlyGeneratedSpace [UCompactlyGeneratedSpace.{u} X] (f : X → Y)
    (h : ∀ (S : CompHaus.{u}) (g : C(S, X)), Continuous (f ∘ g)) : Continuous f

Proof state:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)
⊢ Continuous f

Tactic:
exact continuous_from_compactlyGenerated f h

Result:
no goals
-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem toLp_denseRange [μ.WeaklyRegular] [IsFiniteMeasure μ] (hp : p ≠ ∞) :
    DenseRange (toLp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)

Proof state:
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : NormalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
⊢ DenseRange ⇑(toLp p μ 𝕜)

Tactic:
haveI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E

Result:
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : NormalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
this : NormedSpace ℝ E
⊢ DenseRange ⇑(toLp p μ 𝕜)

Proof state:
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : NormalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ⊤
this : NormedSpace ℝ E
⊢ DenseRange ⇑(toLp p μ 𝕜)

Tactic:
simpa only [← range_toLp p μ (𝕜 := 𝕜)]
  using MeasureTheory.Lp.boundedContinuousFunction_dense E μ hp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem interior_eq_nhds' : interior s = { x | s ∈ 𝓝 x } :=
  Set.ext fun x => by simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
x : X
⊢ x ∈ interior s ↔ x ∈ {x | s ∈ 𝓝 x}

Tactic:
simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem one_smul_aux (p : LocalizedModule S M) : (1 : T) • p = p

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 1 = IsLocalization.mk' T 1 1

Tactic:
rw [IsLocalization.mk'_one, map_one]

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
p : LocalizedModule S M
⊢ 1 • p = p

Tactic:
induction' p with m s

Result:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 1 • mk m s = mk m s

Proof state:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ 1 • mk m s = mk m s

Tactic:
rw [show (1 : T) = IsLocalization.mk' T (1 : R) (1 : S) by rw [IsLocalization.mk'_one, map_one]]

Result:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ IsLocalization.mk' T 1 1 • mk m s = mk m s

Proof state:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
m : M
s : ↥S
⊢ IsLocalization.mk' T 1 1 • mk m s = mk m s

Tactic:
rw [mk'_smul_mk, one_smul, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Cones.lean
theorem Cocone.w {F : J ⥤ C} (c : Cocone F) {j j' : J} (f : j ⟶ j') :
    F.map f ≫ c.ι.app j' = c.ι.app j

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ c.ι.app j ≫ ((const J).obj c.pt).map f = c.ι.app j

Tactic:
apply comp_id

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ c.ι.app j' = c.ι.app j

Tactic:
rw [c.ι.naturality f]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ c.ι.app j ≫ ((const J).obj c.pt).map f = c.ι.app j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem count_toArray [BEq α] (a : α) (v : Vector α n) :
    v.toArray.count a = v.count a

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
v : Vector α n
⊢ Array.count a v.toArray = count a v

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.count a { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    count a { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.count a { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    count a { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem isOrthoᵢ_flip (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M) {v : n → M₁} :
    B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v

Tactic:
simp_rw [isOrthoᵢ_def]

Result:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0) ↔ ∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0) ↔ ∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0

Tactic:
constructor <;> exact fun h i j hij ↦ h j i hij.symm

Result:
no goals
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_union_inter [DecidableEq α] (s₁ s₂ : Multiset α) (b₁ b₂ : α) :
    ((s₁ ∪ s₂).fold op b₁ * (s₁ ∩ s₂).fold op b₂) = s₁.fold op b₁ * s₂.fold op b₂

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)

Tactic:
rw [← fold_add op, union_add_inter, fold_add op]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
@[simp] lemma iInf_ulift {ι : Type*} [InfSet α] (f : ULift ι → α) :
    ⨅ i : ULift ι, f i = ⨅ i, f (.up i)

Proof state:
α : Type u_1
ι : Type u_8
inst✝ : InfSet α
f : ULift.{u_9, u_8} ι → α
⊢ sInf (range fun i => f i) = sInf (range fun i => f { down := i })

Tactic:
congr with x

Result:
case e_a.h
α : Type u_1
ι : Type u_8
inst✝ : InfSet α
f : ULift.{u_9, u_8} ι → α
x : α
⊢ (x ∈ range fun i => f i) ↔ x ∈ range fun i => f { down := i }

Proof state:
case e_a.h
α : Type u_1
ι : Type u_8
inst✝ : InfSet α
f : ULift.{u_9, u_8} ι → α
x : α
⊢ (x ∈ range fun i => f i) ↔ x ∈ range fun i => f { down := i }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_8
inst✝ : InfSet α
f : ULift.{u_9, u_8} ι → α
⊢ ⨅ i, f i = ⨅ i, f { down := i }

Tactic:
simp [iInf]

Result:
α : Type u_1
ι : Type u_8
inst✝ : InfSet α
f : ULift.{u_9, u_8} ι → α
⊢ sInf (range fun i => f i) = sInf (range fun i => f { down := i })
-- Mathlib/Data/Fin/Tuple/Reflection.lean
theorem forall_iff : ∀ {m} (P : (Fin m → α) → Prop), Forall P ↔ ∀ x, P x
  | 0, P => by
    simp only [Forall, Fin.forall_fin_zero_pi]
    rfl
  | .succ n, P => by simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]

Proof state:
α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin n.succ → α), P x

Tactic:
simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]

Result:
no goals

Proof state:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x

Tactic:
simp only [Forall, Fin.forall_fin_zero_pi]

Result:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim

Proof state:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
/-- In a finitary matroid, every element spanned by a set `X` is in fact
spanned by a finite independent subset of `X`. -/
lemma exists_mem_finite_closure_of_mem_closure [M.Finitary] (he : e ∈ M.closure X) :
    ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Proof state:
case pos
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis {e}

Result:
case pos.intro
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Proof state:
case neg.intro.intro.intro
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
C : Set α
hCs : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
exact ⟨C \ {e}, by simpa, hC.finite.diff, hC.diff_singleton_indep heC,
  hC.mem_closure_diff_singleton_of_mem heC⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
C : Set α
hCs : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ X

Tactic:
simpa

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
obtain ⟨C, hCs, hC, heC⟩ := exists_isCircuit_of_mem_closure he heY

Result:
case neg.intro.intro.intro
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
C : Set α
hCs : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
by_cases heY : e ∈ X

Result:
case pos
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

case neg
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ {e} ⊆ X

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ e ∈ M.closure J

Tactic:
simpa using hJ.subset_closure

Result:
no goals

Proof state:
case pos.intro
α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

Tactic:
exact ⟨J, hJ.subset.trans (by simpa), (finite_singleton e).subset hJ.subset, hJ.indep,
  by simpa using hJ.subset_closure⟩

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_map {s : σ₁} (f₂ : α → β) :
    (mapAccumr f₁ (map f₂ xs) s) = (mapAccumr (fun x s => f₁ (f₂ x) s) xs s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
s : σ₁
f₂ : α → β
⊢ mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun x s => f₁ (f₂ x) s) xs s

Tactic:
induction xs using Vector.revInductionOn generalizing s <;> simp_all

Result:
no goals
-- Mathlib/Topology/MetricSpace/Polish.lean
theorem _root_.IsOpen.polishSpace {α : Type*} [TopologicalSpace α] [PolishSpace α] {s : Set α}
    (hs : IsOpen s) : PolishSpace s

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsOpen s
⊢ PolishSpace ↑s

Tactic:
letI := upgradePolishSpace α

Result:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsOpen s
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ PolishSpace ↑s

Proof state:
case intro
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
this : UpgradedPolishSpace α := upgradePolishSpace α
s : Opens α
⊢ PolishSpace ↑↑s

Tactic:
exact inferInstanceAs (PolishSpace s.CompleteCopy)

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsOpen s
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ PolishSpace ↑s

Tactic:
lift s to Opens α using hs

Result:
case intro
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
this : UpgradedPolishSpace α := upgradePolishSpace α
s : Opens α
⊢ PolishSpace ↑↑s
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma denselyOrdered_units_iff {G₀ : Type*} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] :
    DenselyOrdered G₀ˣ ↔ DenselyOrdered G₀

Proof state:
case mpr.intro.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
hz : ↑x < 0 ∧ 0 < ↑y
⊢ ∃ a, x < a ∧ a < y

Tactic:
simp at hz

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem closure_singleton_zero : closure ({0} : Set A) = ⊥

Proof state:
A : Type u_2
inst✝ : AddMonoid A
⊢ closure {0} = ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton, nsmul_zero]

Result:
no goals