harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toLeft_cons_inr (hb) :
    (cons (inr b) u hb).toLeft = u.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
hb : inr b ∉ u
y : α
⊢ y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toLeft = u.toLeft

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
hb : inr b ∉ u
y : α
⊢ y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft
-- Mathlib/Data/List/Pi.lean
lemma mem_pi {l : List ι} (fs : ∀ i, List (α i)) :
    ∀ f : ∀ i ∈ l, α i, (f ∈ pi l fs) ↔ (∀ i (hi : i ∈ l), f i hi ∈ fs i)

Proof state:
case h.e'_1.a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
f : (i : ι) → i ∈ l → α i
⊢ f ∈ l.pi fs ↔ f ∈ ↑(l.pi fs)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_1.a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
f : (i : ι) → i ∈ l → α i
⊢ f ∈ l.pi fs ↔ f ∈ (↑l).pi fun x => ↑(fs x)

Tactic:
rw [Multiset.pi_coe]

Result:
case h.e'_1.a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
f : (i : ι) → i ∈ l → α i
⊢ f ∈ l.pi fs ↔ f ∈ ↑(l.pi fs)

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
⊢ ∀ (f : (i : ι) → i ∈ l → α i), f ∈ l.pi fs ↔ ∀ (i : ι) (hi : i ∈ l), f i hi ∈ fs i

Tactic:
intros f

Result:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
f : (i : ι) → i ∈ l → α i
⊢ f ∈ l.pi fs ↔ ∀ (i : ι) (hi : i ∈ l), f i hi ∈ fs i
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[simp]
lemma mem_genEigenspace_one {f : End R M} {μ : R} {x : M} :
    x ∈ f.genEigenspace μ 1 ↔ f x = μ • x

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ (f.genEigenspace μ) 1 ↔ f x = μ • x

Tactic:
rw [genEigenspace_one, LinearMap.mem_ker, LinearMap.sub_apply,
  sub_eq_zero, LinearMap.smul_apply, LinearMap.one_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma add_comp (α₁ α₂ : Ext X Y n) {m : ℕ} (β : Ext Y Z m) {p : ℕ} (h : n + m = p) :
    (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((α₁ + α₂).comp β h).hom = (α₁.comp β h + α₂.comp β h).hom

Tactic:
simp [this, add_hom']

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((α₁ + α₂).comp β h).hom = (α₁.comp β h + α₂.comp β h).hom
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivWithinAt.scomp_hasDerivAt_of_eq (hg : HasDerivWithinAt g₁ g₁' s' y)
    (hh : HasDerivAt h h' x) (hs : ∀ x, h x ∈ s') (hy : y = h x) :
    HasDerivAt (g₁ ∘ h) (h' • g₁') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
exact hg.scomp_hasDerivAt x hh hs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' y
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ico_succ_left_eq_Ioo (a b : α) : Ico (succ a) b = Ioo a b :=
  coe_injective <| by simpa using Set.Ico_succ_left_eq_Ioo _ _

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

Tactic:
simpa using Set.Ico_succ_left_eq_Ioo _ _

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem dpow_sum' {M : Type*} [AddCommMonoid M] {I : AddSubmonoid M} (dpow : ℕ → M → A)
    (dpow_zero : ∀ {x} (_ : x ∈ I), dpow 0 x = 1)
    (dpow_add : ∀ {n x y} (_ : x ∈ I) (_ : y ∈ I),
      dpow n (x + y) = (antidiagonal n).sum fun k ↦ dpow k.1 x * dpow k.2 y)
    (dpow_eval_zero : ∀ {n : ℕ} (_ : n ≠ 0), dpow n 0 = 0)
    {ι : Type*} [DecidableEq ι] {s : Finset ι} {x : ι → M} (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ} :
    dpow n (s.sum x) = (s.sym n).sum fun k ↦ s.prod fun i ↦ dpow (Multiset.count i k) (x i)

Proof state:
case empty
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
⊢ dpow n (∅.sum x) = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dpow (Multiset.count i ↑k) (x i)

Tactic:
simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]

Result:
case empty
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
⊢ dpow n 0 = ↑(#(∅.sym n))
-- Mathlib/GroupTheory/Nilpotent.lean
theorem CommGroup.nilpotencyClass_le_one {G : Type*} [CommGroup G] :
    Group.nilpotencyClass G ≤ 1

Proof state:
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
apply CommGroup.center_eq_top

Result:
no goals

Proof state:
G : Type u_2
inst✝ : CommGroup G
⊢ nilpotencyClass G ≤ 1

Tactic:
rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_one]

Result:
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤
-- Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean
theorem isIso_iff_bijective [(forget C).ReflectsIsomorphisms]
    {X Y : C} (f : X ⟶ Y) : IsIso f ↔ Function.Bijective f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ IsIso ⇑(hom f)

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ isIso_of_reflects_iso f (forget C)⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ Function.Bijective ⇑(hom f)

Tactic:
rw [← CategoryTheory.isIso_iff_bijective]

Result:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ IsIso ⇑(hom f)
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
  { epi := epi_of_epi f g
    llp := fun {X Y} z _ => by
      constructor
      intro u v sq
      have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v

Proof state:
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ ∀ {f : Q ⟶ X} {g_1 : R ⟶ Y} (sq : CommSq f g z g_1), sq.HasLift

Tactic:
intro u v sq

Result:
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ sq.HasLift

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ ⋯.lift ≫ z = v

Tactic:
simp

Result:
no goals

Proof state:
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ sq.HasLift

Tactic:
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]

Result:
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ sq.HasLift

Proof state:
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ sq.HasLift

Tactic:
exact
  CommSq.HasLift.mk'
    ⟨(CommSq.mk h₀).lift, by
      simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ HasLiftingProperty g z

Tactic:
constructor

Result:
case sq_hasLift
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ ∀ {f : Q ⟶ X} {g_1 : R ⟶ Y} (sq : CommSq f g z g_1), sq.HasLift

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ (f ≫ u) ≫ z = (f ≫ g) ≫ v

Tactic:
simp only [Category.assoc, sq.w]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ g ≫ ⋯.lift = u

Tactic:
simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem take_take {s : Stream' α} : ∀ {m n}, (s.take n).take m = s.take (min n m)
  | 0, n => by rw [Nat.min_zero, List.take_zero, take_zero]
  | m, 0 => by rw [Nat.zero_min, take_zero, List.take_nil]
  | m+1, n+1 => by rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]

Proof state:
α : Type u
s : Stream' α
m n : ℕ
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s

Tactic:
rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]

Result:
no goals

Proof state:
α : Type u
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take (min n 0) s

Tactic:
rw [Nat.min_zero, List.take_zero, take_zero]

Result:
no goals

Proof state:
α : Type u
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take (min 0 m) s

Tactic:
rw [Nat.zero_min, take_zero, List.take_nil]

Result:
no goals
-- Mathlib/Algebra/QuaternionBasis.lean
theorem lift_mul (x y : ℍ[R,c₁,c₂,c₃]) : q.lift (x * y) = q.lift x * q.lift y

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * y.imJ * c₃) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -((x.imK * y.imK * (c₁ * c₃)) • 1)

Tactic:
simp only [mul_right_comm _ _ (c₁ * c₃), mul_comm _ (c₁ * c₃)]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * y.imJ * c₃) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem lt_add_of_tsub_lt_right (hc : AddLECancellable c) (h : a - c < b) :
    a < b + c

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a < b + c

Tactic:
rw [lt_iff_le_and_ne, ← tsub_le_iff_right]

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a - c ≤ b ∧ a ≠ b + c

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a ≠ b + c

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b + c - c < b
⊢ False

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b + c - c < b
⊢ False

Tactic:
simp [hc] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a - c ≤ b ∧ a ≠ b + c

Tactic:
refine ⟨h.le, ?_⟩

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a ≠ b + c
-- Mathlib/Data/Sign.lean
theorem Left.sign_neg [AddLeftStrictMono α] (a : α) : sign (-a) = -sign a

Proof state:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
simp_rw [sign_apply, Left.neg_pos_iff, Left.neg_neg_iff]

Result:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Proof state:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

Tactic:
exact False.elim (lt_asymm h h')

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Tactic:
split_ifs with h h'

Result:
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x1 x2 => x1 < x2
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem IsUnit.mem_submonoid_iff {M : Type*} [Monoid M] (a : M) :
    a ∈ IsUnit.submonoid M ↔ IsUnit a

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a

Tactic:
change a ∈ setOf IsUnit ↔ IsUnit a

Result:
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ setOf IsUnit ↔ IsUnit a

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ setOf IsUnit ↔ IsUnit a

Tactic:
rw [Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem lookup_insert_eq_none {l : AList β} {k k' : α} {v : β k} :
    (l.insert k v).lookup k' = none ↔ (k' ≠ k) ∧ l.lookup k' = none

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Tactic:
by_cases h : k' = k

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
h : k' = k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
h : ¬k' = k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
h : k' = k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Tactic:
subst h

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k' : α
v : β k'
⊢ lookup k' (insert k' v l) = none ↔ k' ≠ k' ∧ lookup k' l = none

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
h : ¬k' = k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Tactic:
simp_all [lookup_insert_ne h]

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k' : α
v : β k'
⊢ lookup k' (insert k' v l) = none ↔ k' ≠ k' ∧ lookup k' l = none

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_eq_inv_mul : a / b = b⁻¹ * a

Proof state:
a b : ℝ≥0∞
⊢ a / b = b⁻¹ * a

Tactic:
rw [div_eq_mul_inv, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
theorem delete_iff (c : DefaultClause n) (l l' : Literal (PosFin n)) :
    l' ∈ toList (delete c l) ↔ l' ≠ l ∧ l' ∈ toList c

Proof state:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ List.erase c.clause l ↔ ¬l' = l ∧ l' ∈ c.clause

Tactic:
by_cases hl : l' = l

Result:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ List.erase c.clause l ↔ ¬l' = l ∧ l' ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ List.erase c.clause l ↔ ¬l' = l ∧ l' ∈ c.clause

Proof state:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ List.erase c.clause l ↔ ¬l' = l ∧ l' ∈ c.clause

Tactic:
simp only [hl, not_false_eq_true, true_and]

Result:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ List.erase c.clause l ↔ l' ∈ c.clause

Proof state:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ ¬l ∈ List.erase c.clause l

Tactic:
exact List.Nodup.not_mem_erase c.nodup

Result:
no goals

Proof state:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ (c.delete l).toList ↔ l' ≠ l ∧ l' ∈ c.toList

Tactic:
simp only [toList, delete, ne_eq]

Result:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ List.erase c.clause l ↔ ¬l' = l ∧ l' ∈ c.clause

Proof state:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ List.erase c.clause l ↔ ¬l' = l ∧ l' ∈ c.clause

Tactic:
simp only [hl, not_true, false_and, iff_false]

Result:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ ¬l ∈ List.erase c.clause l

Proof state:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ List.erase c.clause l ↔ l' ∈ c.clause

Tactic:
exact List.mem_erase_of_ne hl

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toENNReal_le_toENNReal {x y : EReal} (h : x ≤ y) : x.toENNReal ≤ y.toENNReal

Proof state:
x y : EReal
h : x ≤ y
⊢ x.toENNReal ≤ y.toENNReal

Tactic:
induction x

Result:
case h_bot
y : EReal
h : ⊥ ≤ y
⊢ ⊥.toENNReal ≤ y.toENNReal

case h_real
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

case h_top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Proof state:
case h_real
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

Tactic:
by_cases hy_top : y = ⊤

Result:
case pos
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

Proof state:
case h_bot
y : EReal
h : ⊥ ≤ y
⊢ ⊥.toENNReal ≤ y.toENNReal

Tactic:
simp

Result:
no goals

Proof state:
case pos
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

Tactic:
simp [hy_top]

Result:
no goals

Proof state:
case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ (↑a✝).toENNReal ≤ y.toENNReal

Tactic:
simp only [toENNReal, coe_ne_top, ↓reduceIte, toReal_coe, hy_top]

Result:
case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ ENNReal.ofReal a✝ ≤ ENNReal.ofReal y.toReal

Proof state:
case h_top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Tactic:
simp_all

Result:
no goals

Proof state:
case neg
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
hy_top : ¬y = ⊤
⊢ ENNReal.ofReal a✝ ≤ ENNReal.ofReal y.toReal

Tactic:
exact ENNReal.ofReal_le_ofReal <| EReal.toReal_le_toReal h (coe_ne_bot _) hy_top

Result:
no goals