harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem neighborSet_union_compl_neighborSet_eq (G : SimpleGraph V) (v : V) :
    G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v

Tactic:
tauto

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ

Tactic:
have h := @ne_of_adj _ G

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ

Tactic:
ext w

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ

Tactic:
simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem star_mem {x : CliffordAlgebra Q} (hx : x ∈ pinGroup Q) : star x ∈ pinGroup Q

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid

Tactic:
simp only [Submonoid.mem_map, Subgroup.mem_toSubmonoid, Units.coeHom_apply, exists_prop]

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ∃ x_1 ∈ lipschitzGroup Q, ↑x_1 = star x

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ y * star y = 1

Tactic:
rw [← Units.eq_iff]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ↑(y * star y) = ↑1

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ↑(star y) = star x

Tactic:
simp only [hy₂, Units.coe_star]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ star y ∈ lipschitzGroup Q

Tactic:
have hy₃ : y * star y = 1 := by
  rw [← Units.eq_iff]
  simp only [hx₃, Units.val_mul, Units.coe_star, Units.val_one]

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : ↑y * star ↑y = 1
hy₁ : y ∈ lipschitzGroup Q
hy₃ : y * star y = 1
⊢ star y ∈ lipschitzGroup Q
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_lt_add_one (a : α) : (⌈a⌉ : α) < a + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌈a⌉ < ⌈a⌉ + 1

Tactic:
apply lt_add_one

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ↑⌈a⌉ < a + 1

Tactic:
rw [← lt_ceil, ← Int.cast_one, ceil_add_int]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌈a⌉ < ⌈a⌉ + 1
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem measurable_mapNatBool [MeasurableSpace α] [CountablyGenerated α] :
    Measurable (mapNatBool α)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
n : ℕ
⊢ MeasurableSet (natGeneratingSequence α n)

Tactic:
apply measurableSet_natGeneratingSequence

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
n : ℕ
⊢ MeasurableSet ((fun x => mapNatBool α x n) ⁻¹' {true})

Tactic:
simp only [preimage, mem_singleton_iff, mapNatBool,
  Bool.decide_iff, setOf_mem_eq]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
n : ℕ
⊢ MeasurableSet (natGeneratingSequence α n)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ Measurable (mapNatBool α)

Tactic:
rw [measurable_pi_iff]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ∀ (a : ℕ), Measurable fun x => mapNatBool α x a

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ∀ (a : ℕ), Measurable fun x => mapNatBool α x a

Tactic:
refine fun n ↦ measurable_to_bool ?_

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
n : ℕ
⊢ MeasurableSet ((fun x => mapNatBool α x n) ⁻¹' {true})
-- Mathlib/Topology/GDelta/Basic.lean
theorem residual_of_dense_Gδ {s : Set X} (ho : IsGδ s) (hd : Dense s) : s ∈ residual X

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
To : ∀ t ∈ T, IsOpen t
Tct : T.Countable
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual X

Tactic:
exact
  (countable_sInter_mem Tct).mpr fun t tT =>
    residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
ho : IsGδ s
hd : Dense s
⊢ s ∈ residual X

Tactic:
rcases ho with ⟨T, To, Tct, rfl⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
To : ∀ t ∈ T, IsOpen t
Tct : T.Countable
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual X
-- Mathlib/Probability/Integration.lean
theorem IndepFun.integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β}
    [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (hX : Integrable X μ)
    (hY : Integrable Y μ) : Integrable (X * Y) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ
⊢ HasFiniteIntegral (X * Y) μ

Tactic:
simp only [nX, nY] at hmul

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
hX : Integrable X μ
hY : Integrable Y μ
nX : Ω → ℝ≥0∞ := fun a => ‖X a‖ₑ
nY : Ω → ℝ≥0∞ := fun a => ‖Y a‖ₑ
hXY' : IndepFun nX nY μ
hnX : AEMeasurable nX μ
hnY : AEMeasurable nY μ
hmul : ∫⁻ (a : Ω), ‖X a‖ₑ * ‖Y a‖ₑ ∂μ = (∫⁻ (a : Ω), ‖X a‖ₑ ∂μ) * ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ
⊢ HasFiniteIntegral (X * Y) μ
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.exists_of_disjoint_sets_of_equiv {s t : Set V} (h : Disjoint s t)
    (f : s ≃ t) (hadj : ∀ v : s, G.Adj v (f v)) :
    ∃ M : Subgraph G, M.verts = s ∪ t ∧ M.IsMatching

Proof state:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ ⦃v : V⦄, v ∈ s ∨ v ∈ t → ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
intro v hv

Result:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s ∨ v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Proof state:
case inl.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s
⊢ G.Adj v ↑(f ⟨v, hv⟩)

Tactic:
exact hadj ⟨v, _⟩

Result:
no goals

Proof state:
case inr.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w

Tactic:
exact (hadj ⟨w, _⟩).symm

Result:
no goals

Proof state:
case h.inl.intro
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ ↑(f ⟨v, hy⟩) = ↑(f.symm ⟨v, hr⟩)

Tactic:
exact (h.ne_of_mem hy hr rfl).elim

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem card_roots_le [IsDomain R] [DecidableEq R] : P.roots.toFinset.card ≤ 3

Proof state:
case neg
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : ¬P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3

Tactic:
exact WithBot.coe_le_coe.1 ((card_roots hP).trans degree_cubic_le)

Result:
no goals

Proof state:
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : P.toPoly = 0
⊢ P.toPoly.natDegree ≤ 3

Tactic:
rw [hP, natDegree_zero]

Result:
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : P.toPoly = 0
⊢ 0 ≤ 3

Proof state:
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ P.toPoly.roots.card ≤ 3

Tactic:
by_cases hP : P.toPoly = 0

Result:
case pos
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3

case neg
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : ¬P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3

Proof state:
case pos
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3

Tactic:
exact (card_roots' P.toPoly).trans (by rw [hP, natDegree_zero]; exact zero_le 3)

Result:
no goals

Proof state:
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : P.toPoly = 0
⊢ 0 ≤ 3

Tactic:
exact zero_le 3

Result:
no goals

Proof state:
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ P.roots.toFinset.card ≤ 3

Tactic:
apply (toFinset_card_le P.toPoly.roots).trans

Result:
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ P.toPoly.roots.card ≤ 3
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_fin_succ' {n} {v : Fin (n + 1) → V} : LinearIndependent K v ↔
    LinearIndependent K (Fin.init v) ∧ v (Fin.last _) ∉ Submodule.span K (range <| Fin.init v)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
v : Fin (n + 1) → V
⊢ LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ span K (range (Fin.init v))

Tactic:
rw [← linearIndependent_fin_snoc, Fin.snoc_init_self]

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
lemma Theory.IsUniversal.models_of_embedding {T : L.Theory} [hT : T.IsUniversal]
    {N : Type*} [L.Structure N] [N ⊨ T] (f : M ↪[L] N) : M ⊨ T

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
⊢ ∀ φ ∈ T, M ⊨ φ

Tactic:
refine fun φ hφ => (hT.isUniversal_of_mem hφ).realize_embedding f (?_)

Result:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize φ (⇑f ∘ default) (⇑f ∘ default)

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize φ (⇑f ∘ default) (⇑f ∘ default)

Tactic:
rw [Subsingleton.elim (f ∘ default) default, Subsingleton.elim (f ∘ default) default]

Result:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize φ default default

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
⊢ M ⊨ T

Tactic:
simp only [model_iff]

Result:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
⊢ ∀ φ ∈ T, M ⊨ φ

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize φ default default

Tactic:
exact Theory.realize_sentence_of_mem T hφ

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem clog_mono_right {b : ℕ} {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ ≤ r₂) :
    clog b r₁ ≤ clog b r₂

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹

Tactic:
exact log_mono_right (inv_pos.mpr <| h₀.trans_le h) (inv_anti₀ h₀ h)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ clog b r₁ ≤ clog b r₂

Tactic:
rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]

Result:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₂⁻¹ ≤ log b r₁⁻¹
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
theorem unitCompPartialBijective_natural [Reflective i] (A : C) {B B' : C} (h : B ⟶ B')
    (hB : i.essImage B) (hB' : i.essImage B') (f : A ⟶ B) :
    (unitCompPartialBijective A hB') (f ≫ h) = unitCompPartialBijective A hB f ≫ h

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
⊢ (unitCompPartialBijective A hB') (f ≫ h) = (unitCompPartialBijective A hB) f ≫ h

Tactic:
rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
lemma coe_killingCompl_top :
    killingCompl R L ⊤ = LinearMap.ker (killingForm R L)

Proof state:
case h
R : Type u_1
L : Type u_3
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ (toLieSubalgebra R L (killingCompl R L ⊤)).toSubmodule ↔ x ∈ LinearMap.ker (killingForm R L)

Tactic:
simp [LinearMap.ext_iff, LinearMap.BilinForm.IsOrtho, LieModule.traceForm_comm R L L x]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (toLieSubalgebra R L (killingCompl R L ⊤)).toSubmodule = LinearMap.ker (killingForm R L)

Tactic:
ext x

Result:
case h
R : Type u_1
L : Type u_3
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ (toLieSubalgebra R L (killingCompl R L ⊤)).toSubmodule ↔ x ∈ LinearMap.ker (killingForm R L)
-- Mathlib/Topology/UnitInterval.lean
theorem mul_pos_mem_iff {a t : ℝ} (ha : 0 < a) : a * t ∈ I ↔ t ∈ Set.Icc (0 : ℝ) (1 / a)

Proof state:
case mp.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a

Tactic:
rwa [le_div_iff₀ ha, mul_comm]

Result:
no goals

Proof state:
case mp.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t

Tactic:
exact nonneg_of_mul_nonneg_right h₁ ha

Result:
no goals

Proof state:
case mpr.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1

Tactic:
rwa [le_div_iff₀ ha, mul_comm] at h₂

Result:
no goals

Proof state:
a t : ℝ
ha : 0 < a
⊢ a * t ∈ I ↔ t ∈ Icc 0 (1 / a)

Tactic:
constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor

Result:
case mp.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ 0 ≤ t

case mp.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ a * t
h₂ : a * t ≤ 1
⊢ t ≤ 1 / a

case mpr.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t

case mpr.intro.right
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ a * t ≤ 1

Proof state:
case mpr.intro.left
a t : ℝ
ha : 0 < a
h₁ : 0 ≤ t
h₂ : t ≤ 1 / a
⊢ 0 ≤ a * t

Tactic:
exact mul_nonneg ha.le h₁

Result:
no goals
-- Mathlib/Topology/Homotopy/Contractible.lean
theorem Nullhomotopic.comp_left {f : C(Y, Z)} (hf : f.Nullhomotopic) (g : C(X, Y)) :
    (f.comp g).Nullhomotopic

Proof state:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
⊢ (f.comp g).Homotopic (const X y)

Tactic:
exact Homotopic.hcomp (Homotopic.refl g) hy

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
hf : f.Nullhomotopic
g : C(X, Y)
⊢ (f.comp g).Nullhomotopic

Tactic:
obtain ⟨y, hy⟩ := hf

Result:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
⊢ (f.comp g).Nullhomotopic

Proof state:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
⊢ (f.comp g).Nullhomotopic

Tactic:
use y

Result:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : f.Homotopic (const Y y)
⊢ (f.comp g).Homotopic (const X y)
-- Mathlib/Data/Stream/Init.lean
theorem take_succ' {s : Stream' α} : ∀ n, s.take (n+1) = s.take n ++ [s.get n]
  | 0 => rfl
  | n+1 => by rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]

Proof state:
α : Type u
s : Stream' α
n : ℕ
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_one {α : Fin (n + 1) → Sort*} (v : (i : Fin (n + 1)) → α i) :
    take 1 (Nat.le_add_left 1 n) v = (fun i => v (castLE (Nat.le_add_left 1 n) i))

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin 1
⊢ take 1 ⋯ v i = v (castLE ⋯ i)

Tactic:
simp only [take]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ take 1 ⋯ v = fun i => v (castLE ⋯ i)

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin 1
⊢ take 1 ⋯ v i = v (castLE ⋯ i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem_modify_eq (f : α → α) (n) (l : List α) (h) :
    (modify f n l)[n] = f (l[n]'(by simpa using h))

Proof state:
α : Type ?u.24626
f : α → α
n : Nat
l : List α
h : n < (modify f n l).length
⊢ n < l.length

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < (modify f n l).length
⊢ (modify f n l)[n] = f l[n]

Tactic:
simp [getElem_modify]

Result:
no goals
-- Mathlib/Control/Traversable/Lemmas.lean
theorem traverse_comp (g : α → F β) (h : β → G γ) :
    traverse (Comp.mk ∘ map h ∘ g) =
      (Comp.mk ∘ map (traverse h) ∘ traverse g : t α → Comp F G (t γ))

Proof state:
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
x✝ : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x✝ = (Comp.mk ∘ map (traverse h) ∘ traverse g) x✝

Tactic:
exact comp_traverse _ _ _

Result:
no goals

Proof state:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
⊢ traverse (Comp.mk ∘ map h ∘ g) = Comp.mk ∘ map (traverse h) ∘ traverse g

Tactic:
ext

Result:
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
x✝ : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x✝ = (Comp.mk ∘ map (traverse h) ∘ traverse g) x✝
-- Mathlib/RingTheory/FreeCommRing.lean
theorem lift_comp_of (f : FreeCommRing α →+* R) : lift (f ∘ of) = f :=
  RingHom.ext fun x =>
    FreeCommRing.induction_on x (by rw [RingHom.map_neg, RingHom.map_one, f.map_neg, f.map_one])
      (lift_of _) (fun x y ihx ihy => by rw [RingHom.map_add, f.map_add, ihx, ihy])
      fun x y ihx ihy => by rw [RingHom.map_mul, f.map_mul, ihx, ihy]

Proof state:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x : FreeCommRing α
⊢ (lift (⇑f ∘ of)) (-1) = f (-1)

Tactic:
rw [RingHom.map_neg, RingHom.map_one, f.map_neg, f.map_one]

Result:
no goals

Proof state:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) (x + y) = f (x + y)

Tactic:
rw [RingHom.map_add, f.map_add, ihx, ihy]

Result:
no goals

Proof state:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) (x * y) = f (x * y)

Tactic:
rw [RingHom.map_mul, f.map_mul, ihx, ihy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem toList_alter [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
    {l : AssocList α β} :
    Perm (l.alter a f).toList (alterKey a f l.toList)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : (alter a f tail✝).toList.Perm (alterKey a f tail✝.toList)
⊢ (if h : (key✝ == a) = true then
          let_fun h' := ⋯;
          match f (some (cast ⋯ value✝)) with
          | none => tail✝
          | some b => cons a b tail✝
        else
          let tail := alter a f tail✝;
          cons key✝ value✝ tail).toList.Perm
    (if hk : (key✝ == a) = true then
      match f (some (cast ⋯ value✝)) with
      | none => tail✝.toList
      | some v => ⟨a, v⟩ :: tail✝.toList
    else ⟨key✝, value✝⟩ :: alterKey a f tail✝.toList)

Tactic:
split <;> (try split) <;> simp_all

Result:
no goals