harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma degree_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) : (C a * p).degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a * p).degree = p.degree

Tactic:
rw [degree_mul', degree_C ha.ne_zero]

Result:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ 0 + p.degree = p.degree

R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0

Proof state:
case inl
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
⊢ (C a * 0).degree = degree 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (C a * p).degree = p.degree

Tactic:
nontriviality R

Result:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a * p).degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ (C a).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
simpa [ha.mul_right_eq_zero]

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).degree = p.degree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Result:
case inl
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
⊢ (C a * 0).degree = degree 0

case inr
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (C a * p).degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
a✝ : Nontrivial R
⊢ 0 + p.degree = p.degree

Tactic:
simp

Result:
no goals
-- Mathlib/Control/Bitraversable/Lemmas.lean
theorem tsnd_tfst {α₀ α₁ β₀ β₁} (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀) :
    Comp.mk (tsnd f' <$> tfst f x)
      = bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x =
    bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x

Tactic:
simp only [Function.comp_def, map_pure]

Result:
no goals

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ Comp.mk (tsnd f' <$> tfst f x) = bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x

Tactic:
rw [← comp_bitraverse]

Result:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ β₀ β₁ : Type u
f : α₀ → F α₁
f' : β₀ → G β₁
x : t α₀ β₀
⊢ bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x =
    bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma posSemidef_add [AddLeftMono R]
    {A : Matrix m m R} {B : Matrix m m R}
    (hA : A.PosSemidef) (hB : B.PosDef) : (A + B).PosDef :=
  ⟨hA.isHermitian.add hB.isHermitian, fun x hx => by
    rw [add_mulVec, dotProduct_add]
    exact add_pos_of_nonneg_of_pos (hA.2 x) (hB.2 x hx)⟩

Proof state:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosDef
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x

Tactic:
exact add_pos_of_nonneg_of_pos (hA.2 x) (hB.2 x hx)

Result:
no goals

Proof state:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosDef
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (A + B) *ᵥ x

Tactic:
rw [add_mulVec, dotProduct_add]

Result:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosSemidef
hB : B.PosDef
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x
-- Mathlib/Data/Matroid/Circuit.lean
lemma Dep.exists_isCircuit_subset (hX : M.Dep X) : ∃ C, C ⊆ X ∧ M.IsCircuit C

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
⊢ ∃ C ⊆ X, M.IsCircuit C

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis X

Result:
case intro
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
⊢ ∃ C ⊆ X, M.IsCircuit C

Proof state:
case intro.intro.intro
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
e : α
heX : e ∈ X
heI : e ∉ I
⊢ ∃ C ⊆ X, M.IsCircuit C

Tactic:
exact ⟨M.fundCircuit e I, (M.fundCircuit_subset_insert e I).trans (insert_subset heX hI.subset),
  hI.indep.fundCircuit_isCircuit (hI.subset_closure heX) heI⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
⊢ I ≠ X

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
I : Set α
hX : M.Dep I
hI : M.IsBasis I I
⊢ False

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hX : M.Dep I
hI : M.IsBasis I I
⊢ False

Tactic:
exact hI.indep.not_dep hX

Result:
no goals

Proof state:
case intro
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
⊢ ∃ C ⊆ X, M.IsCircuit C

Tactic:
obtain ⟨e, heX, heI⟩ := exists_of_ssubset
  (hI.subset.ssubset_of_ne (by rintro rfl; exact hI.indep.not_dep hX))

Result:
case intro.intro.intro
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
e : α
heX : e ∈ X
heI : e ∉ I
⊢ ∃ C ⊆ X, M.IsCircuit C
-- Mathlib/Data/Fin/Parity.lean
lemma odd_of_odd {n : ℕ} [NeZero n] (hn : Odd n) (k : Fin n) : Odd k

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
⊢ Odd k

Tactic:
rcases k.val.even_or_odd with hk | hk

Result:
case inl
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Even ↑k
⊢ Odd k

case inr
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Odd ↑k
⊢ Odd k

Proof state:
case inl
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Even ↑k
⊢ Odd k

Tactic:
simpa using (Even.add_odd hk hn).natCast (R := Fin n)

Result:
no goals

Proof state:
case inr
n : ℕ
inst✝ : NeZero n
hn : Odd n
k : Fin n
hk : Odd ↑k
⊢ Odd k

Tactic:
exact odd_of_val hk

Result:
no goals
-- Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
theorem succNthVal_spec' (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0)
    (ha₂ : a₂.coeff 0 ≠ 0) :
    succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
          a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) =
      succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)

Proof state:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this :
  succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
        nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
      (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
        nthRemainder p n bs (truncateFun (n + 1) a₂)) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) -
        succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
      (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) -
          a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) -
        nthRemainder p n bs (truncateFun (n + 1) a₂))

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/Convex/Quasiconvex.lean
theorem quasilinearOn_iff_mem_uIcc : QuasilinearOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄,
    y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ QuasilinearOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Tactic:
rw [QuasilinearOn, quasiconvexOn_iff_le_max, quasiconcaveOn_iff_min_le, and_and_and_comm,
  and_self_iff]

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ (Convex 𝕜 s ∧
      (∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ f x ⊔ f y) ∧
        ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ⊓ f y ≤ f (a • x + b • y)) ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ (Convex 𝕜 s ∧
      (∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ f x ⊔ f y) ∧
        ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ⊓ f y ≤ f (a • x + b • y)) ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Tactic:
apply and_congr_right'

Result:
case h
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ ((∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ f x ⊔ f y) ∧
      ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ⊓ f y ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ ((∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ f x ⊔ f y) ∧
      ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ⊓ f y ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Tactic:
simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :
    (insertIdx.loop i as j).size = as.size

Proof state:
case isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
h✝ : i < ↑j
⊢ (let j' := ⟨↑j - 1, ⋯⟩;
      let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
      insertIdx.loop i as_1 ⟨↑j', ⋯⟩).size =
    as.size

Tactic:
rw [size_insertIdx_loop, size_swap]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
h✝ : ¬i < ↑j
⊢ as.size = as.size

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
⊢ (insertIdx.loop i as j).size = as.size

Tactic:
unfold insertIdx.loop

Result:
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
⊢ (if i < ↑j then
        let j' := ⟨↑j - 1, ⋯⟩;
        let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
        insertIdx.loop i as_1 ⟨↑j', ⋯⟩
      else as).size =
    as.size

Proof state:
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
⊢ (if i < ↑j then
        let j' := ⟨↑j - 1, ⋯⟩;
        let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
        insertIdx.loop i as_1 ⟨↑j', ⋯⟩
      else as).size =
    as.size

Tactic:
split

Result:
case isTrue
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
h✝ : i < ↑j
⊢ (let j' := ⟨↑j - 1, ⋯⟩;
      let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
      insertIdx.loop i as_1 ⟨↑j', ⋯⟩).size =
    as.size

case isFalse
α : Type u_1
as : Array α
i : Nat
j : Fin as.size
h✝ : ¬i < ↑j
⊢ as.size = as.size
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem ext_threefold {g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q}
    (H : ∀ x y z, g (x ⊗ₜ y ⊗ₜ z) = h (x ⊗ₜ y ⊗ₜ z)) : g = h

Proof state:
case H.H.h.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q
H : ∀ (x : M) (y : N) (z : P), g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
x : M
y : N
z : P
⊢ ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ g)) x) y) z =
    ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ h)) x) y) z

Tactic:
exact H x y z

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q
H : ∀ (x : M) (y : N) (z : P), g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
⊢ g = h

Tactic:
ext x y z

Result:
case H.H.h.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q
H : ∀ (x : M) (y : N) (z : P), g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
x : M
y : N
z : P
⊢ ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ g)) x) y) z =
    ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) P).compr₂ h)) x) y) z
-- Mathlib/Analysis/Convex/Between.lean
theorem affineSegment_same (x : P) : affineSegment R x x = {x}

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 : P
⊢ affineSegment R x x = {x}

Tactic:
simp_rw [affineSegment, lineMap_same, AffineMap.coe_const, Function.const,
  (Set.nonempty_Icc.mpr zero_le_one).image_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_shrink (a : Array α) (n : Nat) (i : Nat) (h : i < (a.shrink n).size) :
    (a.shrink n)[i] = a[i]'(by simp at h; omega)

Proof state:
α : Type ?u.488907
a : Array α
n i : Nat
h : i < min n a.size
⊢ i < a.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.488907
a : Array α
n i : Nat
h : i < (a.shrink n).size
⊢ i < a.size

Tactic:
simp at h

Result:
α : Type ?u.488907
a : Array α
n i : Nat
h : i < min n a.size
⊢ i < a.size

Proof state:
α : Type u_1
a : Array α
n i : Nat
h : i < (a.shrink n).size
⊢ (a.shrink n)[i] = a[i]

Tactic:
simp [shrink]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem isLittleO_cpow_mul_exp {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (a₁ a₂ : ℂ) :
    (fun z => z ^ a₁ * exp (b₁ * z)) =o[l] fun z => z ^ a₂ * exp (b₂ * z) :=
  calc
    (fun z => z ^ a₁ * exp (b₁ * z)) =ᶠ[l] fun z => z ^ a₂ * exp (b₁ * z) * z ^ (a₁ - a₂) :=
      hl.eventually_ne.mono fun z hz => by
        simp only
        rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]
    _ =o[l] fun z => z ^ a₂ * exp (b₁ * z) * exp (↑(b₂ - b₁) * z) :=
      ((isBigO_refl (fun z => z ^ a₂ * exp (b₁ * z)) l).mul_isLittleO <|
        hl.isLittleO_cpow_exp _ (sub_pos.2 hb))
    _ =ᶠ[l] fun z => z ^ a₂ * exp (b₂ * z)

Proof state:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z => z ^ a₁ * cexp (↑b₁ * z)) z = (fun z => z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)) z

Tactic:
simp only

Result:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * cexp (↑b₁ * z) = z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)

Proof state:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * cexp (↑b₂ * z)) =ᶠ[l] fun z => z ^ a₂ * cexp (↑b₂ * z)

Tactic:
norm_cast

Result:
no goals

Proof state:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * cexp (↑b₁ * z) = z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)

Tactic:
rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]

Result:
no goals

Proof state:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * cexp (↑b₁ * z) * cexp (↑(b₂ - b₁) * z)) =ᶠ[l] fun z => z ^ a₂ * cexp (↑b₂ * z)

Tactic:
simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel]

Result:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * cexp (↑b₂ * z)) =ᶠ[l] fun z => z ^ a₂ * cexp (↑b₂ * z)
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_insert [DecidableEq α] (a : α) (s : Finset α) :
    (insert a s).sym2 = ((insert a s).image fun b => s(a, b)) ∪ s.sym2

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
⊢ (insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2

Tactic:
simp only [insert_eq_of_mem ha, right_eq_union, image_subset_iff]

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
⊢ ∀ x ∈ s, s(a, x) ∈ s.sym2

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
⊢ (insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2

Tactic:
simpa [map_eq_image] using sym2_cons a s ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2

Tactic:
obtain ha | ha := Decidable.em (a ∈ s)

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
⊢ (insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2

case inr
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
⊢ (insert a s).sym2 = image (fun b => s(a, b)) (insert a s) ∪ s.sym2

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
⊢ ∀ x ∈ s, s(a, x) ∈ s.sym2

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem of_eq_eq_false {a b : Prop} (h : (a = b) = False) : (¬a ∨ ¬b) ∧ (b ∨ a)

Proof state:
a b : Prop
h : (a = b) = False
⊢ (¬a ∨ ¬b) ∧ (b ∨ a)

Tactic:
by_cases a <;> by_cases b <;> simp_all

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma add_sub_cancel_left {a : EReal} {b : Real} : b + a - b = a

Proof state:
a : EReal
b : ℝ
⊢ ↑b + a - ↑b = a

Tactic:
rw [add_comm, EReal.add_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma quasispectrum_eq_spectrum_union (R : Type*) {A : Type*} [CommSemiring R]
    [Ring A] [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {r : R | ¬ IsUnit r}

Proof state:
case h
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ r ∈ {r | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))} ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_union, ← imp_iff_or_not, spectrum.mem_iff]

Result:
case h
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ IsUnit r → ¬IsUnit ((algebraMap R A) r - a)

Proof state:
case h
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}

Tactic:
rw [quasispectrum]

Result:
case h
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ r ∈ {r | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))} ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}

Proof state:
case h.a.h.a
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit ((algebraMap R A) r - a)

Tactic:
rw [not_iff_not, isQuasiregular_iff_isUnit, ← sub_eq_add_neg, Algebra.algebraMap_eq_smul_one]

Result:
case h.a.h.a
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (r • 1 - a)

Proof state:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ quasispectrum R a = spectrum R a ∪ {r | ¬IsUnit r}

Tactic:
ext r

Result:
case h
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}

Proof state:
case h.a.h.a
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (r • 1 - a)

Tactic:
exact (IsUnit.smul_sub_iff_sub_inv_smul hr.unit a).symm

Result:
no goals

Proof state:
case h
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ IsUnit r → ¬IsUnit ((algebraMap R A) r - a)

Tactic:
congr! 1 with hr

Result:
case h.a.h.a
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit ((algebraMap R A) r - a)
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_pos_of_pos (hq : 0 < q) : (0 : K) < q

Proof state:
q : ℚ
K : Type u_5
inst✝ : LinearOrderedField K
hq : 0 < q
⊢ 0 < ↑q.num / ↑q.den

Tactic:
exact div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)

Result:
no goals

Proof state:
q : ℚ
K : Type u_5
inst✝ : LinearOrderedField K
hq : 0 < q
⊢ 0 < ↑q

Tactic:
rw [Rat.cast_def]

Result:
q : ℚ
K : Type u_5
inst✝ : LinearOrderedField K
hq : 0 < q
⊢ 0 < ↑q.num / ↑q.den
-- Mathlib/LinearAlgebra/FreeProduct/Basic.lean
theorem mul_injections (a₁ a₂ : A i) :
    ι' R A (DirectSum.lof R I A i a₁) * ι' R A (DirectSum.lof R I A i a₂)
      = ι' R A (DirectSum.lof R I A i (a₁ * a₂))

Proof state:
case h.e'_2
I : Type u
inst✝³ : DecidableEq I
i : I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
a₁ a₂ : A i
⊢ (ι' R A) ((lof R I A i) a₁) * (ι' R A) ((lof R I A i) a₂) =
    (RingQuot.mkAlgHom R (rel R A))
      ((tprod R (⨁ (i : I), A i) 2) fun x =>
        match x with
        | 0 => (lof R I A i) a₁
        | 1 => (lof R I A i) a₂)

Tactic:
simp

Result:
no goals

Proof state:
I : Type u
inst✝³ : DecidableEq I
i : I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
a₁ a₂ : A i
⊢ (ι' R A) ((lof R I A i) a₁) * (ι' R A) ((lof R I A i) a₂) = (ι' R A) ((lof R I A i) (a₁ * a₂))

Tactic:
convert RingQuot.mkAlgHom_rel R <| rel.prod

Result:
case h.e'_2
I : Type u
inst✝³ : DecidableEq I
i : I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
a₁ a₂ : A i
⊢ (ι' R A) ((lof R I A i) a₁) * (ι' R A) ((lof R I A i) a₂) =
    (RingQuot.mkAlgHom R (rel R A))
      ((tprod R (⨁ (i : I), A i) 2) fun x =>
        match x with
        | 0 => (lof R I A i) a₁
        | 1 => (lof R I A i) a₂)