harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateRow_transpose [DecidableEq n] : updateRow Mᵀ j c = (updateCol M j c)ᵀ

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ Mᵀ.updateRow j c i✝ j✝ = (M.updateCol j c)ᵀ i✝ j✝

Tactic:
rw [transpose_apply, updateRow_apply, updateCol_apply]

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ (if i✝ = j then c j✝ else Mᵀ i✝ j✝) = if i✝ = j then c j✝ else M j✝ i✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ (if i✝ = j then c j✝ else Mᵀ i✝ j✝) = if i✝ = j then c j✝ else M j✝ i✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
⊢ Mᵀ.updateRow j c = (M.updateCol j c)ᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ Mᵀ.updateRow j c i✝ j✝ = (M.updateCol j c)ᵀ i✝ j✝
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_subtype_lt [Fintype α] {p : α → Prop} [DecidablePred p] {x : α} (hx : ¬p x) :
    Fintype.card { x // p x } < Fintype.card α :=
  Fintype.card_lt_of_injective_of_not_mem (b := x) (↑) Subtype.coe_injective <| by
    rwa [Subtype.range_coe_subtype]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ x ∉ Set.range Subtype.val

Tactic:
rwa [Subtype.range_coe_subtype]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem not_principal_iff : ¬ Principal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

Proof state:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ ¬Principal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

Tactic:
simp [Principal]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem symm_map (f : α ≃o β) : (map f).symm = map f.symm :=
  DFunLike.ext _ _ fun s => ext <| by convert Set.preimage_equiv_eq_image_symm s f.toEquiv

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : LowerSet β
⊢ ↑((map f).symm s) = ↑((map f.symm) s)

Tactic:
convert Set.preimage_equiv_eq_image_symm s f.toEquiv

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem smul_apply [IsScalarTower R ℝ≥0 ℝ≥0] (c : R) (μ : FiniteMeasure Ω) (s : Set Ω) :
    (c • μ) s = c • μ s

Proof state:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
s : Set Ω
⊢ (c • μ) s = c • μ s

Tactic:
rw [coeFn_smul, Pi.smul_apply]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem not_bddBelow_coe : ¬ (BddBelow <| range (fun (x : ℚ) ↦ (x : ℝ)))

Proof state:
⊢ ¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a}.Nonempty

Tactic:
rw [Set.not_nonempty_iff_eq_empty]

Result:
⊢ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a} = ∅

Proof state:
case h
x✝ : ℝ
⊢ x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a} ↔ x✝ ∈ ∅

Tactic:
simpa using exists_rat_lt _

Result:
no goals

Proof state:
⊢ ¬BddBelow (range fun x => ↑x)

Tactic:
dsimp only [BddBelow, lowerBounds]

Result:
⊢ ¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a}.Nonempty

Proof state:
⊢ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a} = ∅

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a} ↔ x✝ ∈ ∅
-- Mathlib/Data/ENNReal/Inv.lean
lemma iSup_add_iSup_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → ℝ≥0∞}
    (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ a, f a + g a :=
  iSup_add_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ ↦ by gcongr <;> apply_rules

Proof state:
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
gcongr <;> apply_rules

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem continuous_preStoneCechUnit : Continuous (preStoneCechUnit : α → PreStoneCech α) :=
  continuous_iff_ultrafilter.mpr fun x g gx ↦ by
    have : (g.map pure).toFilter ≤ 𝓝 g

Proof state:
case h.e'_1.h.e'_3.h
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : map preStoneCechUnit ↑g ≤ 𝓝 (Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g)
e_1✝ : PreStoneCech α = Quot fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x
⊢ preStoneCechUnit x = Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g

Tactic:
exact Quot.sound ⟨x, pure_le_nhds x, gx⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Tactic:
have : (g.map pure).toFilter ≤ 𝓝 g := by
  rw [ultrafilter_converges_iff, ← bind_pure g]
  rfl

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Tactic:
have : (map preStoneCechUnit g : Filter (PreStoneCech α)) ≤ 𝓝 (Quot.mk _ g) :=
  (map_mono this).trans (continuous_quot_mk.tendsto _)

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : map preStoneCechUnit ↑g ≤ 𝓝 (Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g)
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map pure g) ≤ 𝓝 g

Tactic:
rw [ultrafilter_converges_iff, ← bind_pure g]

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : map preStoneCechUnit ↑g ≤ 𝓝 (Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g)
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Tactic:
convert this

Result:
case h.e'_1.h.e'_3.h
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : map preStoneCechUnit ↑g ≤ 𝓝 (Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g)
e_1✝ : PreStoneCech α = Quot fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x
⊢ preStoneCechUnit x = Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g
-- Mathlib/Analysis/Convex/Between.lean
theorem affineSegment_comm (x y : P) : affineSegment R x y = affineSegment R y x

Proof state:
case mpr.intro.intro.refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
t : R
ht : t ∈ Set.Icc 0 1
hxy : (lineMap y x) t = z
⊢ 1 - t ∈ Set.Icc 0 1

Tactic:
rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]

Result:
no goals

Proof state:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ z ∈ affineSegment R y x → z ∈ affineSegment R x y

Tactic:
rintro ⟨t, ht, hxy⟩

Result:
case mpr.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
t : R
ht : t ∈ Set.Icc 0 1
hxy : (lineMap y x) t = z
⊢ z ∈ affineSegment R x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ affineSegment R x y = affineSegment R y x

Tactic:
refine Set.ext fun z => ?_

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x

Proof state:
case mpr.intro.intro.refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
t : R
ht : t ∈ Set.Icc 0 1
hxy : (lineMap y x) t = z
⊢ (lineMap x y) (1 - t) = z

Tactic:
rwa [lineMap_apply_one_sub]

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
t : R
ht : t ∈ Set.Icc 0 1
hxy : (lineMap y x) t = z
⊢ z ∈ affineSegment R x y

Tactic:
refine ⟨1 - t, ?_, ?_⟩

Result:
case mpr.intro.intro.refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
t : R
ht : t ∈ Set.Icc 0 1
hxy : (lineMap y x) t = z
⊢ 1 - t ∈ Set.Icc 0 1

case mpr.intro.intro.refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
t : R
ht : t ∈ Set.Icc 0 1
hxy : (lineMap y x) t = z
⊢ (lineMap x y) (1 - t) = z
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_comp_add_const {a b : 𝕜} :
    DifferentiableAt 𝕜 (fun x ↦ f (x + b)) a ↔ DifferentiableAt 𝕜 f (a + b)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 (fun x => f (x + b)) a ↔ DifferentiableAt 𝕜 f (a + b)

Tactic:
simpa [add_comm b] using differentiableAt_comp_const_add (f := f) (b := b)

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Finite.preimage' (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite) :
    (f ⁻¹' s).Finite

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (f ⁻¹' s).Finite

Tactic:
rw [← Set.biUnion_preimage_singleton]

Result:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (⋃ y ∈ s, f ⁻¹' {y}).Finite

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (⋃ y ∈ s, f ⁻¹' {y}).Finite

Tactic:
exact Set.Finite.biUnion h hf

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem natDegree_eq_zero_iff_eq_one (hp : p.Monic) : p.natDegree = 0 ↔ p = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
⊢ p.degree ≤ 0

Tactic:
rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
⊢ p = C (p.coeff 0)

Tactic:
rw [← Polynomial.degree_le_zero_iff]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
⊢ p.degree ≤ 0

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
⊢ p = 1

Tactic:
have : p = C (p.coeff 0) := by
  rw [← Polynomial.degree_le_zero_iff]
  rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
this : p = C (p.coeff 0)
⊢ p = 1

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
this : p = C (p.coeff 0)
⊢ p = 1

Tactic:
rw [this]

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
this : p = C (p.coeff 0)
⊢ C (p.coeff 0) = 1

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
⊢ p = 1

case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p = 1
⊢ p.natDegree = 0

Tactic:
swap

Result:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p = 1
⊢ p.natDegree = 0

case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
⊢ p = 1

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
this : p = C (p.coeff 0)
⊢ C (p.coeff 0) = 1

Tactic:
rw [← h, ← Polynomial.leadingCoeff, Monic.def.1 hp, C_1]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ p.natDegree = 0 ↔ p = 1

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p.natDegree = 0
⊢ p = 1

case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p = 1
⊢ p.natDegree = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p = 1
⊢ p.natDegree = 0

Tactic:
rw [h]

Result:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p = 1
⊢ natDegree 1 = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
h : p = 1
⊢ natDegree 1 = 0

Tactic:
exact natDegree_one

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_inter_inter (t s₁ s₂ s₁' s₂' : Set α) :
    t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Proof state:
case h
α : Type u
t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ x ∈ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') ↔ x ∈ t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Tactic:
simp only [Set.ite, Set.mem_inter_iff, Set.mem_diff, Set.mem_union]

Result:
case h
α : Type u
t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ x ∉ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ x ∉ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ x ∉ t)

Proof state:
α : Type u
t s₁ s₂ s₁' s₂' : Set α
⊢ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Tactic:
ext x

Result:
case h
α : Type u
t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ x ∈ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') ↔ x ∈ t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Proof state:
case h
α : Type u
t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ x ∉ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ x ∉ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ x ∉ t)

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem mem_keys_kerase_of_ne {a₁ a₂} {l : List (Sigma β)} (h : a₁ ≠ a₂) :
    a₁ ∈ (kerase a₂ l).keys ↔ a₁ ∈ l.keys :=
  (Iff.intro mem_keys_of_mem_keys_kerase) fun p =>
    if q : a₂ ∈ l.keys then
      match l, kerase a₂ l, exists_of_kerase q, p with
      | _, _, ⟨_, _, _, _, rfl, rfl⟩, p => by simpa [keys, h] using p
    else by simp [q, p]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p✝ : a₁ ∈ l.keys
w✝² : β a₂
w✝¹ w✝ : List (Sigma β)
left✝ : a₂ ∉ w✝¹.keys
p : a₁ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
q : a₂ ∈ (w✝¹ ++ ⟨a₂, w✝²⟩ :: w✝).keys
⊢ a₁ ∈ (w✝¹ ++ w✝).keys

Tactic:
simpa [keys, h] using p

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p : a₁ ∈ l.keys
q : a₂ ∉ l.keys
⊢ a₁ ∈ (kerase a₂ l).keys

Tactic:
simp [q, p]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem eqToIso_refl {n : ℕ} (h : n = n) : X.eqToIso h = Iso.refl _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ X.eqToIso h = Iso.refl (X ^⦋n⦌)

Tactic:
ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ (X.eqToIso h).hom = (Iso.refl (X ^⦋n⦌)).hom

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ (X.eqToIso h).hom = (Iso.refl (X ^⦋n⦌)).hom

Tactic:
simp [eqToIso]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
lemma maxTrivSubmodule_eq_bot_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
    LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : D x = 0
⊢ D x = 0 x

Tactic:
simp [this]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
⊢ (ad R L) (D x) = 0

Tactic:
rw [LieModule.mem_maxTrivSubmodule] at hD

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : ∀ (x : L), ⁅x, D⁆ = 0
x : L
⊢ (ad R L) (D x) = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
⊢ LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥

Tactic:
refine (LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
⊢ D x = 0 x

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : (ad R L) (D x) = 0
⊢ D x = 0 x

Tactic:
rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : D x = 0
⊢ D x = 0 x

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : ∀ (x : L), ⁅x, D⁆ = 0
x : L
⊢ (ad R L) (D x) = 0

Tactic:
simp [ad_apply_lieDerivation, hD]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
⊢ D x = 0 x

Tactic:
have : ad R L (D x) = 0 := by
  rw [LieModule.mem_maxTrivSubmodule] at hD
  simp [ad_apply_lieDerivation, hD]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : (ad R L) (D x) = 0
⊢ D x = 0 x
-- Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean
/--
The kernel of the ring homomorphism `R → R⧸I` is `I`.
-/
@[simp]
lemma ker_ringCon_mk' (I : TwoSidedIdeal R) : ker I.ringCon.mk' = I :=
  le_antisymm
    (fun _ h => by simpa using I.rel_iff _ _ |>.1 (Quotient.eq'.1 h))
    (fun _ h => Quotient.sound' <| I.rel_iff _ _ |>.2 (by simpa using h))

Proof state:
R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ ker I.ringCon.mk'
⊢ x✝ ∈ I

Tactic:
simpa using I.rel_iff _ _ |>.1 (Quotient.eq'.1 h)

Result:
no goals

Proof state:
R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ I
⊢ x✝ - 0 ∈ I

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ico_succ_left_eq_Ioo (a b : α) : Ico (succ a) b = Ioo a b

Proof state:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
ext x

Result:
case neg.h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b

Proof state:
case neg.h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b

Tactic:
rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
⊢ Ico (succ a) b = Ioo a b

Tactic:
by_cases ha : IsMax a

Result:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b

case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Proof state:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem map_eq_sum [Countable β] [MeasurableSingletonClass β] (μ : Measure α) (f : α → β)
    (hf : Measurable f) : μ.map f = sum fun b : β => μ (f ⁻¹' {b}) • dirac b

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
⊢ map f μ = sum fun b => μ (f ⁻¹' {b}) • dirac b

Tactic:
ext s

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
a✝ : MeasurableSet s
⊢ (map f μ) s = (sum fun b => μ (f ⁻¹' {b}) • dirac b) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
a✝ : MeasurableSet s
this : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ (map f μ) s = (sum fun b => μ (f ⁻¹' {b}) • dirac b) s

Tactic:
simp [← tsum_measure_preimage_singleton (to_countable s) this, *,
  tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
a✝ : MeasurableSet s
⊢ (map f μ) s = (sum fun b => μ (f ⁻¹' {b}) • dirac b) s

Tactic:
have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _)

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
a✝ : MeasurableSet s
this : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ (map f μ) s = (sum fun b => μ (f ⁻¹' {b}) • dirac b) s
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem one_le_zpow {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n

Proof state:
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ x ^ n

Tactic:
lift n to ℕ using hn

Result:
case intro
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ ↑n

Proof state:
case intro
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ ↑n

Tactic:
rw [zpow_natCast]

Result:
case intro
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n

Proof state:
case intro
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
H : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n

Tactic:
apply one_le_pow_of_one_le' H

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem aestronglyMeasurable_uIoc_iff [LinearOrder α] [PseudoMetrizableSpace β] {f : α → β}
    {a b : α} :
    AEStronglyMeasurable f (μ.restrict <| uIoc a b) ↔
      AEStronglyMeasurable f (μ.restrict <| Ioc a b) ∧
        AEStronglyMeasurable f (μ.restrict <| Ioc b a)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : LinearOrder α
inst✝ : PseudoMetrizableSpace β
f : α → β
a b : α
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b)) ↔
    AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))

Tactic:
rw [uIoc_eq_union, aestronglyMeasurable_union_iff]

Result:
no goals