harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_triangle' (fin : hausdorffEdist t u ≠ ⊤) :
    hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist u t ≠ ⊤
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
simpa [add_comm, hausdorffDist_comm] using I

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist u t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s :=
  hausdorffDist_triangle fin

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist u t ≠ ⊤
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist t u ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
rw [hausdorffEdist_comm] at fin

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist u t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- The delta-generated topology is also coinduced by a single map out of a sigma type. -/
lemma deltaGenerated_eq_coinduced : deltaGenerated X = coinduced
    (fun x : (f : (n : ℕ) × C(Fin n → ℝ, X)) × (Fin f.1 → ℝ) ↦ x.1.2 x.2) inferInstance

Proof state:
X : Type u_1
tX : TopologicalSpace X
⊢ deltaGenerated X = coinduced (fun x => x.fst.snd x.snd) inferInstance

Tactic:
rw [deltaGenerated, instTopologicalSpaceSigma, coinduced_iSup]

Result:
X : Type u_1
tX : TopologicalSpace X
⊢ ⨆ f, coinduced (⇑f.snd) inferInstance =
    ⨆ i, coinduced (fun x => x.fst.snd x.snd) (coinduced (Sigma.mk i) Pi.topologicalSpace)

Proof state:
X : Type u_1
tX : TopologicalSpace X
⊢ ⨆ f, coinduced (⇑f.snd) inferInstance =
    ⨆ i, coinduced (fun x => x.fst.snd x.snd) (coinduced (Sigma.mk i) Pi.topologicalSpace)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/Basic.lean
@[simp] lemma lie_coe_lieDerivation_apply (x : L) (D : LieDerivation R L M) :
    ⁅x, (D : L →ₗ[R] M)⁆ = ⁅x, D⁆

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
D : LieDerivation R L M
x✝ : L
⊢ ⁅x, ↑D⁆ x✝ = ↑⁅x, D⁆ x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
D : LieDerivation R L M
⊢ ⁅x, ↑D⁆ = ↑⁅x, D⁆

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
D : LieDerivation R L M
x✝ : L
⊢ ⁅x, ↑D⁆ x✝ = ↑⁅x, D⁆ x✝
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_length (l : List α) : rotate' l l.length = l

Proof state:
α : Type u
l : List α
⊢ drop l.length l ++ take l.length l = l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ l.rotate' l.length = l

Tactic:
rw [rotate'_eq_drop_append_take le_rfl]

Result:
α : Type u
l : List α
⊢ drop l.length l ++ take l.length l = l
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_antiperiodic : Function.Antiperiodic sin π

Proof state:
⊢ Function.Antiperiodic sin ↑π

Tactic:
simp [sin_add]

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem strictAntiOn_natAbs : StrictAntiOn natAbs (Iic 0) := fun a _ b hb hab => by
  simpa [Int.natAbs_neg] using
    natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)

Proof state:
a : ℤ
x✝ : a ∈ Iic 0
b : ℤ
hb : b ∈ Iic 0
hab : a < b
⊢ b.natAbs < a.natAbs

Tactic:
simpa [Int.natAbs_neg] using
  natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem term_neg {α} [AddCommGroup α] (n x a n' a')
    (h₁ : -n = n') (h₂ : -a = a') : -@termg α _ n x a = termg n' x a'

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -termg n x a = termg n' x a'

Tactic:
simpa [h₂.symm, h₁.symm, termg] using add_comm _ _

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_iff_not_injective {x : A} :
    IsAlgebraic R x ↔ ¬Function.Injective (Polynomial.aeval x : R[X] →ₐ[R] A)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ IsAlgebraic R x ↔ ¬Function.Injective ⇑(aeval x)

Tactic:
simp only [IsAlgebraic, injective_iff_map_eq_zero, not_forall, and_comm, exists_prop]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
protected lemma Finset.sum_empty {β α : Type*} [CommSemiring β] (f : α → β) :
    IsNat (Finset.sum ∅ f) 0 :=
  ⟨by simp⟩

Proof state:
β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ ∅.sum f = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_target_mem_nhdsWithin_of_mem {x : M} {y : E} (hy : y ∈ (extChartAt I x).target) :
    (extChartAt I x).target ∈ 𝓝[range I] y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∈ 𝓝[range ↑I] ↑(extChartAt I x) (↑(extChartAt I x).symm y)

Tactic:
apply extChartAt_target_mem_nhdsWithin'

Result:
case hy
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ ↑(extChartAt I x).symm y ∈ (extChartAt I x).source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∈ 𝓝[range ↑I] y

Tactic:
rw [← (extChartAt I x).right_inv hy]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∈ 𝓝[range ↑I] ↑(extChartAt I x) (↑(extChartAt I x).symm y)

Proof state:
case hy
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ ↑(extChartAt I x).symm y ∈ (extChartAt I x).source

Tactic:
exact (extChartAt I x).map_target hy

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem Eventually.diag_of_prod {p : α × α → Prop} (h : ∀ᶠ i in f ×ˢ f, p i) :
    ∀ᶠ i in f, p (i, i)

Proof state:
α : Type u_1
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
⊢ ∀ᶠ (i : α) in f, p (i, i)

Tactic:
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h

Result:
case intro.intro.intro.intro
α : Type u_1
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : α → Prop
hs : ∀ᶠ (y : α) in f, s y
hst : ∀ {x : α}, t x → ∀ {y : α}, s y → p (x, y)
⊢ ∀ᶠ (i : α) in f, p (i, i)

Proof state:
case intro.intro.intro.intro
α : Type u_1
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : α → Prop
hs : ∀ᶠ (y : α) in f, s y
hst : ∀ {x : α}, t x → ∀ {y : α}, s y → p (x, y)
⊢ ∀ᶠ (i : α) in f, p (i, i)

Tactic:
apply (ht.and hs).mono fun x hx => hst hx.1 hx.2

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1

Proof state:
m : ℕ
⊢ (m + 1) % 2 + m % 2 = 1

Tactic:
rw [add_comm, mod_two_add_succ_mod_two]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma not_odd_iff : ¬Odd n ↔ n % 2 = 0

Proof state:
n : ℕ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
rw [odd_iff, mod_two_not_eq_one]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.WF.tail (hwf : (s : Heap α).WF le n) : (s.tail le).WF le 0

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
hwf : WF le n s
⊢ WF le 0 (Heap.tail le s)

Tactic:
simp only [Heap.tail]

Result:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
hwf : WF le n s
⊢ WF le 0 ((Heap.tail? le s).getD Heap.nil)

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
hwf : WF le n s
tl : Heap α
eq : Heap.tail? le s = some tl
⊢ WF le 0 ((some tl).getD Heap.nil)

Tactic:
exact hwf.tail? eq

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
hwf : WF le n s
⊢ WF le 0 ((Heap.tail? le s).getD Heap.nil)

Tactic:
match eq : s.tail? le with
| none => exact Heap.WF.nil
| some tl => exact hwf.tail? eq

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
hwf : WF le n s
eq : Heap.tail? le s = none
⊢ WF le 0 (none.getD Heap.nil)

Tactic:
exact Heap.WF.nil

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem smul_val (n x y : ℤ) : (n : ℤ√d) * ⟨x, y⟩ = ⟨n * x, n * y⟩

Proof state:
d n x y : ℤ
⊢ ↑n * { re := x, im := y } = { re := n * x, im := n * y }

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma condIndepFun_iff {β γ : Type*} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
    (f : Ω → β) (g : Ω → γ) (hf : Measurable f) (hg : Measurable g)
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndepFun m' hm' f g μ ↔ ∀ t1 t2, MeasurableSet[MeasurableSpace.comap f mβ] t1
      → MeasurableSet[MeasurableSpace.comap g mγ] t2
        → (μ⟦t1 ∩ t2 | m'⟧) =ᵐ[μ] (μ⟦t1 | m'⟧) * (μ⟦t2 | m'⟧)

Proof state:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']

Tactic:
rw [condIndepFun_iff_condIndep, condIndep_iff _ _ _ _ hf.comap_le hg.comap_le]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_coe_eq_self_iff_mem_Ioc {θ : ℝ} : (θ : Angle).toReal = θ ↔ θ ∈ Set.Ioc (-π) π

Proof state:
θ : ℝ
⊢ (↑θ).toReal = θ ↔ θ ∈ Set.Ioc (-π) π

Tactic:
rw [toReal_coe_eq_self_iff, ← Set.mem_Ioc]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
@[parity_simps] lemma even_add : Even (m + n) ↔ (Even m ↔ Even n)

Proof state:
m n : ℕ
⊢ Even (m + n) ↔ (Even m ↔ Even n)

Tactic:
rcases mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂ <;>
  simp [even_iff, h₁, h₂, Nat.add_mod]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma mem_range_root_of_mem_range_reflection_of_mem_range_root
    {r : M ≃ₗ[R] M} {α : M} (hr : r ∈ range P.reflection) (hα : α ∈ range P.root) :
    r • α ∈ range P.root

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
r : M ≃ₗ[R] M
α : M
hr : r ∈ range P.reflection
hα : α ∈ range ⇑P.root
⊢ r • α ∈ range ⇑P.root

Tactic:
obtain ⟨i, rfl⟩ := hr

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
α : M
hα : α ∈ range ⇑P.root
i : ι
⊢ P.reflection i • α ∈ range ⇑P.root

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
α : M
hα : α ∈ range ⇑P.root
i : ι
⊢ P.reflection i • α ∈ range ⇑P.root

Tactic:
obtain ⟨j, rfl⟩ := hα

Result:
case intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.reflection i • P.root j ∈ range ⇑P.root

Proof state:
case intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.reflection i • P.root j ∈ range ⇑P.root

Tactic:
exact ⟨P.reflection_perm i j, P.root_reflection_perm i j⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_set_eq {l : Vector α n} {i : Nat} {a : α} {h : i < n} :
    (l.set i a).eraseIdx i = l.eraseIdx i

Proof state:
case mk
α : Type u_1
i : Nat
a : α
l : Array α
h : i < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.set i a h).eraseIdx i h = { toArray := l, size_toArray := ⋯ }.eraseIdx i h

Tactic:
simp [Array.eraseIdx_set_eq, *]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
a : α
h : i < n
⊢ (l.set i a h).eraseIdx i h = l.eraseIdx i h

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
a : α
l : Array α
h : i < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.set i a h).eraseIdx i h = { toArray := l, size_toArray := ⋯ }.eraseIdx i h
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (m.get? k)).isNone)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).isEmpty = ((m.isEmpty || m.size == 1 && m.contains k) && (f (m.get? k)).isNone)

Tactic:
simp_to_raw using Raw₀.isEmpty_alter

Result:
no goals
-- Mathlib/Data/Matrix/Reflection.lean
theorem vecMulᵣ_eq [NonUnitalNonAssocSemiring α] (v : Fin l → α) (A : Matrix (Fin l) (Fin m) α) :
    vecMulᵣ v A = v ᵥ* A

Proof state:
l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ (fun a => v ⬝ᵥ a) ∘ Aᵀ = v ᵥ* A

Tactic:
rfl

Result:
no goals

Proof state:
l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ vecMulᵣ v A = v ᵥ* A

Tactic:
simp [vecMulᵣ, Function.comp]

Result:
l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ (fun a => v ⬝ᵥ a) ∘ Aᵀ = v ᵥ* A
-- Mathlib/Algebra/Lie/Basic.lean
theorem lie_neg : ⁅x, -m⁆ = -⁅x, m⁆

Proof state:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m⁆ = -⁅x, m⁆

Tactic:
rw [← sub_eq_zero, sub_neg_eq_add, ← lie_add]

Result:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m + m⁆ = 0

Proof state:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m + m⁆ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem mem_extChartAt_source (x : M) : x ∈ (extChartAt I x).source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ x ∈ (extChartAt I x).source

Tactic:
simp only [extChartAt_source, mem_chart_source]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_right_comm : a / b / c = a / c / b

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b / c = a / c / b

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem lift_comp_ι (g : CliffordAlgebra Q →ₐ[R] A) :
    lift Q ⟨g.toLinearMap.comp (ι Q), comp_ι_sq_scalar _⟩ = g

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
⊢ (lift Q) ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩ = g

Tactic:
exact (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_le_one_of_le (hμν : μ ≤ ν) [SigmaFinite ν] : μ.rnDeriv ν ≤ᵐ[ν] 1

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ν s

Tactic:
exact (Measure.setLIntegral_rnDeriv_le s).trans (hμν s)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
⊢ μ.rnDeriv ν ≤ᶠ[ae ν] 1

Tactic:
refine ae_le_of_forall_setLIntegral_le_of_sigmaFinite (μ.measurable_rnDeriv ν) fun s _ _ ↦ ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν

Tactic:
simp only [Pi.one_apply, MeasureTheory.setLIntegral_one]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ⊤
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ν s
-- Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
theorem restrict_top_presheaf (X : PresheafedSpace C) :
    (X.restrict (Opens.isOpenEmbedding ⊤)).presheaf =
      (Opens.inclusionTopIso X.carrier).inv _* X.presheaf

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (X.restrict ⋯).presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
dsimp

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ ⋯.functor.op ⋙ X.presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (Opens.map (Opens.inclusionTopIso ↑X).inv).op ⋙ X.presheaf =
    (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ ⋯.functor.op ⋙ X.presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
rw [Opens.inclusion'_top_functor X.carrier]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (Opens.map (Opens.inclusionTopIso ↑X).inv).op ⋙ X.presheaf =
    (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_right_square (f : X' ⟶ X) (g : X ⟶ G.obj Y')
    (h : X' ⟶ G.obj Y) (k : Y ⟶ Y') (w : f ≫ g = h ≫ G.map k) :
    F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
⊢ F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k

Tactic:
rw [← homEquiv_naturality_left_symm, ← homEquiv_naturality_right_symm, w]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
/-- Two linear maps on `⋀[R]^n M` that agree on the image of `exteriorPower.ιMulti`
are equal. -/
@[ext]
lemma linearMap_ext {f : ⋀[R]^n M →ₗ[R] N} {g : ⋀[R]^n M →ₗ[R] N}
    (heq : f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)) : f = g :=
  (presentation R n M).postcomp_injective (by ext f; apply DFunLike.congr_fun heq )

Proof state:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
⊢ (presentation R n M).postcomp f = (presentation R n M).postcomp g

Tactic:
ext f

Result:
case var.h
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f✝.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
f : (presentation R n M).G
⊢ ((presentation R n M).postcomp f✝).var f = ((presentation R n M).postcomp g).var f

Proof state:
case var.h
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f✝.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
f : (presentation R n M).G
⊢ ((presentation R n M).postcomp f✝).var f = ((presentation R n M).postcomp g).var f

Tactic:
apply DFunLike.congr_fun heq

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_add_self : IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [isVonNBounded_add_of_nonempty, *]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_fst_prod' {f' : α → E' × F'} : (fun x => (f' x).1) =O[l] f'

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f' : α → E' × F'
⊢ (fun x => (f' x).1) =O[l] f'

Tactic:
simpa [IsBigO_def, IsBigOWith_def] using isBigO_fst_prod (E' := E') (F' := F')

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray

Proof state:
α : Type u_1
l : List α
as : Array α
⊢ foldr (fun a b => b.push a) as l = as ++ l.reverse.toArray

Tactic:
rw [foldr_eq_foldl_reverse, foldl_push]

Result:
no goals