harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_apply (M : ∀ i, Matrix (m' i) (n' i) α) (ik jk) :
    blockDiagonal' M ik jk =
      if h : ik.1 = jk.1 then M ik.1 ik.2 (cast (congr_arg n' h.symm) jk.2) else 0

Proof state:
case mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
jk : (i : o) × n' i
fst✝ : o
snd✝ : m' fst✝
⊢ blockDiagonal' M ⟨fst✝, snd✝⟩ jk =
    if h : ⟨fst✝, snd✝⟩.fst = jk.fst then M ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd (cast ⋯ jk.snd) else 0

Tactic:
cases jk

Result:
case mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
fst✝¹ : o
snd✝¹ : m' fst✝¹
fst✝ : o
snd✝ : n' fst✝
⊢ blockDiagonal' M ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩ =
    if h : ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst then M ⟨fst✝¹, snd✝¹⟩.fst ⟨fst✝¹, snd✝¹⟩.snd (cast ⋯ ⟨fst✝, snd✝⟩.snd)
    else 0

Proof state:
case mk.mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
fst✝¹ : o
snd✝¹ : m' fst✝¹
fst✝ : o
snd✝ : n' fst✝
⊢ blockDiagonal' M ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩ =
    if h : ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst then M ⟨fst✝¹, snd✝¹⟩.fst ⟨fst✝¹, snd✝¹⟩.snd (cast ⋯ ⟨fst✝, snd✝⟩.snd)
    else 0

Tactic:
rfl

Result:
no goals

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ik : (i : o) × m' i
jk : (i : o) × n' i
⊢ blockDiagonal' M ik jk = if h : ik.fst = jk.fst then M ik.fst ik.snd (cast ⋯ jk.snd) else 0

Tactic:
cases ik

Result:
case mk
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
jk : (i : o) × n' i
fst✝ : o
snd✝ : m' fst✝
⊢ blockDiagonal' M ⟨fst✝, snd✝⟩ jk =
    if h : ⟨fst✝, snd✝⟩.fst = jk.fst then M ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd (cast ⋯ jk.snd) else 0
-- Mathlib/Order/Atoms.lean
theorem IsStronglyAtomic.of_wellFounded_lt (h : WellFounded ((· < ·) : α → α → Prop)) :
    IsStronglyAtomic α where
  exists_covBy_le_of_lt a b hab

Proof state:
α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 => x1 < x2
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
refine ⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab,rfl.le⟩, ?_⟩

Result:
α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 => x1 < x2
a b : α
hab : a < b
⊢ a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b

Proof state:
α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 => x1 < x2
a b : α
hab : a < b
⊢ a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b

Tactic:
have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab,rfl.le⟩)

Result:
α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 => x1 < x2
a b : α
hab : a < b
hmem : h.min (Set.Ioc a b) ⋯ ∈ Set.Ioc a b
⊢ a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b

Proof state:
α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 => x1 < x2
a b : α
hab : a < b
hmem : h.min (Set.Ioc a b) ⋯ ∈ Set.Ioc a b
⊢ a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b

Tactic:
exact ⟨⟨hmem.1,fun c hac hlt ↦ WellFounded.not_lt_min h
  (Set.Ioc a b) ⟨b, hab,rfl.le⟩ ⟨hac, hlt.le.trans hmem.2⟩ hlt ⟩, hmem.2⟩

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_insert_of_not_mem {a : α} (h : a ∉ s) (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : autoParam s.Finite _auto✝
⊢ (insert a s).ncard = s.ncard + 1

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
  hs.cast_ncard_eq, encard_insert_of_not_mem h]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Ico [NoMinOrder α] {a b : α} (h : a < b) : frontier (Ico a b) = {a, b}

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
h : a < b
⊢ frontier (Ico a b) = {a, b}

Tactic:
rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]

Result:
no goals
-- Mathlib/RingTheory/Derivation/Basic.lean
lemma liftOfSurjective_apply {f : F} (hf : Function.Surjective f)
    {d : Derivation R A A} (hd : ∀ x, f x = 0 → f (d x) = 0) (x : A) :
    Derivation.liftOfSurjective hf hd (f x) = f (d x)

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
hf : Function.Surjective ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ (liftOfSurjective hf hd) (f x) = f (d x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem self_distrib_inv {x y z : R} : x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z

Proof state:
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ y ◃ y ◃⁻¹ z = z

Tactic:
rw [right_inv]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z

Tactic:
rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]

Result:
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z

Proof state:
R : Type u_1
inst✝ : Rack R
x y z : R
⊢ (x ◃ x ◃⁻¹ y) ◃ x ◃ x ◃⁻¹ y ◃⁻¹ z = z

Tactic:
repeat' rw [right_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α} {k : α} :
    get? (insertManyIfNewUnit m l) k =
      if k ∈ m ∨ l.contains k then some () else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ get? (insertManyIfNewUnit m l) k = if m.contains k = true ∨ l.contains k = true then some () else none

Tactic:
simp_to_raw using Raw₀.Const.get?_insertManyIfNewUnit_list

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ get? (insertManyIfNewUnit m l) k = if k ∈ m ∨ l.contains k = true then some () else none

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k : α
⊢ get? (insertManyIfNewUnit m l) k = if m.contains k = true ∨ l.contains k = true then some () else none
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_real (w : InfinitePlace K) (c : ℝ) :
    normAtPlace w ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = |c|

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
⊢ (normAtPlace w) (fun x => c, fun x => ↑c) = |c|

Tactic:
rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul,
  map_one, mul_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
⊢ (fun x => c, fun x => ↑c) = c • 1

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem diag_σ {X : C} : diag X ≫ σ = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ diag X ≫ σ = 0

Tactic:
rw [cokernel.condition_assoc, zero_comp]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma AbsolutelyContinuous.compProd_right [SFinite μ] [IsSFiniteKernel η]
    (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) :
    μ ⊗ₘ κ ≪ μ ⊗ₘ η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
by_cases hκ : IsSFiniteKernel κ

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (μ ⊗ₘ η) s = 0
⊢ (μ ⊗ₘ κ) s = 0

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
simp [compProd_of_not_isSFiniteKernel _ _ hκ]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a => (η a) (Prod.mk a ⁻¹' s)) =ᶠ[ae μ] 0
⊢ (fun a => (κ a) (Prod.mk a ⁻¹' s)) =ᶠ[ae μ] 0

Tactic:
filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (μ ⊗ₘ η) s = 0
⊢ (μ ⊗ₘ κ) s = 0

Tactic:
rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prod_mk_left hs)]
  at hs_zero ⊢

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a => (η a) (Prod.mk a ⁻¹' s)) =ᶠ[ae μ] 0
⊢ (fun a => (κ a) (Prod.mk a ⁻¹' s)) =ᶠ[ae μ] 0
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
lemma coeff_map_eq_comp (p : R[X]) (f : R →+* S) : (p.map f).coeff = f ∘ p.coeff

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ
⊢ (map f p).coeff n = (⇑f ∘ p.coeff) n

Tactic:
exact coeff_map ..

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).coeff = ⇑f ∘ p.coeff

Tactic:
ext n

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ
⊢ (map f p).coeff n = (⇑f ∘ p.coeff) n
-- Mathlib/Data/List/Nodup.lean
theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length)
    (h : xs.get n = xs.get m) (hne : n ≠ m) : ¬Nodup xs

Proof state:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬Injective xs.get

Tactic:
exact fun hinj => hne (hinj h)

Result:
no goals

Proof state:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬xs.Nodup

Tactic:
rw [nodup_iff_injective_get]

Result:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬Injective xs.get
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_lt_mul_of_pos_right {a b c : Int}
  (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c

Proof state:
a b c : Int
h₁ : a < b
h₂ : 0 < c
⊢ a * c < b * c

Tactic:
have : 0 < b - a := Int.sub_pos_of_lt h₁

Result:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < b - a
⊢ a * c < b * c

Proof state:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this✝ : 0 < b - a
this : 0 < (b - a) * c
⊢ a * c < b * c

Tactic:
rw [Int.sub_mul] at this

Result:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this✝ : 0 < b - a
this : 0 < b * c - a * c
⊢ a * c < b * c

Proof state:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this✝ : 0 < b - a
this : 0 < b * c - a * c
⊢ a * c < b * c

Tactic:
exact Int.lt_of_sub_pos this

Result:
no goals

Proof state:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this : 0 < b - a
⊢ a * c < b * c

Tactic:
have : 0 < (b - a) * c := Int.mul_pos this h₂

Result:
a b c : Int
h₁ : a < b
h₂ : 0 < c
this✝ : 0 < b - a
this : 0 < (b - a) * c
⊢ a * c < b * c
-- Mathlib/Control/Fold.lean
theorem foldlm_toList {f : α → β → m α} {x : α} {xs : t β} :
    foldlm f x xs = List.foldlM f x (toList xs) :=
  calc foldlm f x xs
    _ = unop (foldlM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs)) x

Proof state:
α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ foldlm f x xs = unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x

Tactic:
simp only [foldlm, toList_spec, foldMap_hom_free (foldlM.ofFreeMonoid f),
  foldlm.ofFreeMonoid_comp_of, foldlM.get, FreeMonoid.ofList_toList]

Result:
no goals

Proof state:
α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x = List.foldlM f x (toList xs)

Tactic:
simp [foldlM.ofFreeMonoid, unop_op, flip]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem X_pow_card_sub_X_natDegree_eq (hp : 1 < p) : (X ^ p - X : K'[X]).natDegree = p

Proof state:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ X.degree < (X ^ p).degree

Tactic:
rw [degree_X_pow, degree_X]

Result:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ 1 < ↑p

Proof state:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
h1 : X.degree < (X ^ p).degree
⊢ (X ^ p - X).natDegree = p

Tactic:
rw [natDegree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt h1), natDegree_X_pow]

Result:
no goals

Proof state:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ (X ^ p - X).natDegree = p

Tactic:
have h1 : (X : K'[X]).degree < (X ^ p : K'[X]).degree := by
  rw [degree_X_pow, degree_X]
  exact mod_cast hp

Result:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
h1 : X.degree < (X ^ p).degree
⊢ (X ^ p - X).natDegree = p

Proof state:
K' : Type u_3
inst✝ : Field K'
p : ℕ
hp : 1 < p
⊢ 1 < ↑p

Tactic:
exact mod_cast hp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_pair (hxy : x ≠ y) : ({x, y} : Set α).einfsep = edist x y

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep = edist x y ⊓ edist x y

Tactic:
convert einfsep_pair_eq_inf hxy using 2

Result:
case h.e'_3.h.e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ edist x y = edist y x

Proof state:
case h.e'_3.h.e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ edist x y = edist y x

Tactic:
rw [edist_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep = edist x y

Tactic:
nth_rw 1 [← min_self (edist x y)]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep = edist x y ⊓ edist x y
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem IsNormal.le_iff_deriv (H : IsNormal f) {a} : f a ≤ a ↔ ∃ o, deriv f o = a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, derivFamily (fun x => f) o = a

Tactic:
rw [← le_iff_derivFamily fun _ : Unit => H]

Result:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ Unit → f a ≤ a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ Unit → f a ≤ a

Tactic:
exact ⟨fun h _ => h, fun h => h Unit.unit⟩

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, deriv f o = a

Tactic:
unfold deriv

Result:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, derivFamily (fun x => f) o = a
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_natDegree_lt_or_eraseLead_eq_zero (f : R[X]) :
    (eraseLead f).natDegree < f.natDegree ∨ f.eraseLead = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
by_cases h : #f.support ≤ 1

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : ¬#f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Proof state:
case pos.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).eraseLead = 0

Tactic:
simp

Result:
no goals

Proof state:
case neg.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : ¬#f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree

Tactic:
apply eraseLead_natDegree_lt (lt_of_not_ge h)

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
right

Result:
case pos.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : ¬#f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
left

Result:
case neg.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : ¬#f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree

Proof state:
case pos.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead = 0

Tactic:
rw [← C_mul_X_pow_eq_self h]

Result:
case pos.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).eraseLead = 0
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.algHom (f : A →ₐ[R] B) {a : A}
    (h : IsAlgebraic R a) : IsAlgebraic R (f a) :=
  let ⟨p, hp, ha⟩ := h
  ⟨p, hp, by rw [aeval_algHom, f.comp_apply, ha, map_zero]⟩

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : (aeval a) p = 0
⊢ (aeval (f a)) p = 0

Tactic:
rw [aeval_algHom, f.comp_apply, ha, map_zero]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_eq' (s : Multiset α) (b : α) : s.filter (· = b) = replicate (count b s) b :=
  Quotient.inductionOn s fun l => by
    simp only [quot_mk_to_coe, filter_coe, mem_coe, coe_count]
    rw [List.filter_eq l b, coe_replicate]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ filter (fun x => x = b) ⟦l⟧ = replicate (count b ⟦l⟧) b

Tactic:
simp only [quot_mk_to_coe, filter_coe, mem_coe, coe_count]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 => decide (b_1 = b)) l) = replicate (List.count b l) b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 => decide (b_1 = b)) l) = replicate (List.count b l) b

Tactic:
rw [List.filter_eq l b, coe_replicate]

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getD_append_right (l l' : List α) (d : α) (n : ℕ) (h : l.length ≤ n) :
    (l ++ l').getD n d = l'.getD (n - l.length) d

Proof state:
case inr.hn
α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
h' : n ≥ (l ++ l').length
⊢ l'.length ≤ n - l.length

Tactic:
rwa [Nat.le_sub_iff_add_le' h, ← length_append]

Result:
no goals

Proof state:
case inr
α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
h' : n ≥ (l ++ l').length
⊢ (l ++ l').getD n d = l'.getD (n - l.length) d

Tactic:
rw [getD_eq_default _ _ h', getD_eq_default]

Result:
case inr.hn
α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
h' : n ≥ (l ++ l').length
⊢ l'.length ≤ n - l.length

Proof state:
α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
⊢ (l ++ l').getD n d = l'.getD (n - l.length) d

Tactic:
cases Nat.lt_or_ge n (l ++ l').length with
| inl h' =>
  rw [getD_eq_getElem (l ++ l') d h', getElem_append_right h, getD_eq_getElem]
| inr h' =>
  rw [getD_eq_default _ _ h', getD_eq_default]
  rwa [Nat.le_sub_iff_add_le' h, ← length_append]

Result:
no goals

Proof state:
case inl
α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
h' : n < (l ++ l').length
⊢ (l ++ l').getD n d = l'.getD (n - l.length) d

Tactic:
rw [getD_eq_getElem (l ++ l') d h', getElem_append_right h, getD_eq_getElem]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Prod.tendsto_iff {X} (seq : X → Y × Z) {f : Filter X} (p : Y × Z) :
    Tendsto seq f (𝓝 p) ↔
      Tendsto (fun n => (seq n).fst) f (𝓝 p.fst) ∧ Tendsto (fun n => (seq n).snd) f (𝓝 p.snd)

Proof state:
Y : Type v
Z : Type u_1
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
X : Type u_5
seq : X → Y × Z
f : Filter X
p : Y × Z
⊢ Tendsto seq f (𝓝 p) ↔ Tendsto (fun n => (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun n => (seq n).2) f (𝓝 p.2)

Tactic:
rw [nhds_prod_eq, Filter.tendsto_prod_iff']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_replicate (w : replicate n a ≠ []) : (replicate n a).getLast w = a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
w : replicate n a ≠ []
⊢ (replicate n a).getLast w = a

Tactic:
simp [getLast_eq_head_reverse]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive]
lemma oneLePart_leOnePart_injective : Injective fun a : α ↦ (a⁺ᵐ, a⁻ᵐ)

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a = b

Tactic:
rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ Injective fun a => (a⁺ᵐ , a⁻ᵐ)

Tactic:
simp only [Injective, Prod.mk.injEq, and_imp]

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ ∀ ⦃a₁ a₂ : α⦄, a₁⁺ᵐ = a₂⁺ᵐ → a₁⁻ᵐ = a₂⁻ᵐ → a₁ = a₂

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ ∀ ⦃a₁ a₂ : α⦄, a₁⁺ᵐ = a₂⁺ᵐ → a₁⁻ᵐ = a₂⁻ᵐ → a₁ = a₂

Tactic:
rintro a b hpos hneg

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a = b
-- Mathlib/Analysis/Convex/Side.lean
theorem sOppSide_vadd_left_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y

Tactic:
rw [SOppSide, SOppSide, wOppSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]

Result:
no goals