harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Lemmas.lean
theorem dite_dite_distrib_right {a : p → q → α} {b : p → ¬q → α} {c : ¬p → α} :
    dite p (fun hp ↦ dite q (a hp) (b hp)) c =
      dite q (fun hq ↦ dite p (fun hp ↦ a hp hq) c) fun hq ↦ dite p (fun hp ↦ b hp hq) c

Proof state:
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun hp => dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
lemma stalkToFiberRingHom_homogeneousLocalizationToStalk (x z) :
    stalkToFiberRingHom 𝒜 x (homogeneousLocalizationToStalk 𝒜 x z) = z

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z : at x
⊢ (ConcreteCategory.hom (stalkToFiberRingHom 𝒜 x)) (homogeneousLocalizationToStalk 𝒜 x z) = z

Tactic:
obtain ⟨z, rfl⟩ := Quotient.mk''_surjective z

Result:
case intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ (ConcreteCategory.hom (stalkToFiberRingHom 𝒜 x)) (homogeneousLocalizationToStalk 𝒜 x (Quotient.mk'' z)) =
    Quotient.mk'' z

Proof state:
case intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ (ConcreteCategory.hom (stalkToFiberRingHom 𝒜 x)) (homogeneousLocalizationToStalk 𝒜 x (Quotient.mk'' z)) =
    Quotient.mk'' z

Tactic:
rw [homogeneousLocalizationToStalk, Quotient.liftOn'_mk'',
  stalkToFiberRingHom_germ, sectionInBasicOpen]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem eraseIdx_idxOf_eq_erase [BEq α] (a : α) (l : List α) :
    l.eraseIdx (l.idxOf a) = l.erase a

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a : α
⊢ [].eraseIdx (idxOf a []) = [].erase a

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih : xs.eraseIdx (idxOf a xs) = xs.erase a
⊢ (x :: xs).eraseIdx (idxOf a (x :: xs)) = (x :: xs).erase a

Tactic:
rw [List.erase, idxOf_cons]

Result:
case cons
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih : xs.eraseIdx (idxOf a xs) = xs.erase a
⊢ (x :: xs).eraseIdx (bif x == a then 0 else idxOf a xs + 1) =
    match x == a with
    | true => xs
    | false => x :: xs.erase a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ l.eraseIdx (idxOf a l) = l.erase a

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  rw [List.erase, idxOf_cons]
  cases x == a <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih : xs.eraseIdx (idxOf a xs) = xs.erase a
⊢ (x :: xs).eraseIdx (bif x == a then 0 else idxOf a xs + 1) =
    match x == a with
    | true => xs
    | false => x :: xs.erase a

Tactic:
cases x == a <;> simp [ih]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_nonneg_left (h : SameRay R x y) (hx : x ≠ 0) : ∃ r : R, 0 ≤ r ∧ r • x = y

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Result:
case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ r, 0 ≤ r ∧ r • x = 0

case inr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y

Proof state:
case inl
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
h : SameRay R x 0
⊢ ∃ r, 0 ≤ r ∧ r • x = 0

Tactic:
exact ⟨0, le_rfl, zero_smul _ _⟩

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y

Tactic:
exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.mul_left_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : q * p ≠ 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ⊥ < 0

Tactic:
simp

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0

Tactic:
rw [Ne, ← degree_eq_bot, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬p.degree = ⊥

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
⊢ q * p ≠ 0

Tactic:
by_cases h : p = 1

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0

Tactic:
simpa [h]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬p.degree = ⊥

Tactic:
refine ⟨hq, ?_⟩

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬p.degree = ⊥

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬p.degree = ⊥

Tactic:
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ¬p.degree = ⊥

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ¬p.degree = ⊥

Tactic:
refine (lt_trans ?_ h).ne'

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : 0 < p.degree
⊢ ⊥ < 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k

Proof state:
n m k : Nat
h : n + m = k + m
⊢ n = k

Tactic:
rw [Nat.add_comm n m, Nat.add_comm k m] at h

Result:
n m k : Nat
h : m + n = m + k
⊢ n = k

Proof state:
n m k : Nat
h : m + n = m + k
⊢ n = k

Tactic:
apply Nat.add_left_cancel h

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem comap_le_comap_smul (fₗ : N →ₗ[R] N₂) (c : R) : comap fₗ qₗ ≤ comap (c • fₗ) qₗ

Proof state:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
m : N
h : fₗ m ∈ qₗ
⊢ c • fₗ m ∈ qₗ

Tactic:
apply qₗ.smul_mem _ h

Result:
no goals

Proof state:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
m : N
h : m ∈ comap fₗ qₗ
⊢ m ∈ comap (c • fₗ) qₗ

Tactic:
change c • fₗ m ∈ qₗ

Result:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
m : N
h : m ∈ comap fₗ qₗ
⊢ c • fₗ m ∈ qₗ

Proof state:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
m : N
h : m ∈ comap fₗ qₗ
⊢ c • fₗ m ∈ qₗ

Tactic:
change fₗ m ∈ qₗ at h

Result:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
m : N
h : fₗ m ∈ qₗ
⊢ c • fₗ m ∈ qₗ

Proof state:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
⊢ comap fₗ qₗ ≤ comap (c • fₗ) qₗ

Tactic:
rw [SetLike.le_def]

Result:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
⊢ ∀ ⦃x : N⦄, x ∈ comap fₗ qₗ → x ∈ comap (c • fₗ) qₗ

Proof state:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
⊢ ∀ ⦃x : N⦄, x ∈ comap fₗ qₗ → x ∈ comap (c • fₗ) qₗ

Tactic:
intro m h

Result:
R : Type u_1
N : Type u_9
N₂ : Type u_10
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N
inst✝ : Module R N₂
qₗ : Submodule R N₂
fₗ : N →ₗ[R] N₂
c : R
m : N
h : m ∈ comap fₗ qₗ
⊢ m ∈ comap (c • fₗ) qₗ
-- Mathlib/Analysis/Calculus/Deriv/Inverse.lean
theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜}
    (hf : HasDerivAt f 0 (g a)) (hfg : f ∘ g =ᶠ[𝓝 a] id) : ¬DifferentiableAt 𝕜 g a

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
hg : DifferentiableAt 𝕜 g a
this : HasDerivAt id (0 * deriv g a) a
⊢ False

Tactic:
simpa using this.unique (hasDerivAt_id a)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
hg : DifferentiableAt 𝕜 g a
⊢ False

Tactic:
have := (hf.comp a hg.hasDerivAt).congr_of_eventuallyEq hfg.symm

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
hg : DifferentiableAt 𝕜 g a
this : HasDerivAt id (0 * deriv g a) a
⊢ False

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
⊢ ¬DifferentiableAt 𝕜 g a

Tactic:
intro hg

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
hg : DifferentiableAt 𝕜 g a
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.findSome? f = some b) :
    ∃ a, a ∈ l ∧ f a = b

Proof state:
case cons
α : Type u_1
β : Type u_2
b : β
f : α → Option β
h : α
l : List α
ih : findSome? f l = some b → ∃ a, a ∈ l ∧ f a = some b
w :
  (match f h with
    | some b => some b
    | none => findSome? f l) =
    some b
⊢ f h = some b ∨ ∃ a, a ∈ l ∧ f a = some b

Tactic:
split at w <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
b : β
f : α → Option β
w : findSome? f [] = some b
⊢ ∃ a, a ∈ [] ∧ f a = some b

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
l : List α
f : α → Option β
w : findSome? f l = some b
⊢ ∃ a, a ∈ l ∧ f a = some b

Tactic:
induction l with
| nil => simp_all
| cons h l ih =>
  simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
  split at w <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
b : β
f : α → Option β
h : α
l : List α
ih : findSome? f l = some b → ∃ a, a ∈ l ∧ f a = some b
w : findSome? f (h :: l) = some b
⊢ ∃ a, a ∈ h :: l ∧ f a = some b

Tactic:
simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]

Result:
case cons
α : Type u_1
β : Type u_2
b : β
f : α → Option β
h : α
l : List α
ih : findSome? f l = some b → ∃ a, a ∈ l ∧ f a = some b
w :
  (match f h with
    | some b => some b
    | none => findSome? f l) =
    some b
⊢ f h = some b ∨ ∃ a, a ∈ l ∧ f a = some b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.mul.go_denote (ctx : Context) (k : Nat) (p : Poly) : (Poly.mul.go k p).denote ctx = k * p.denote ctx

Proof state:
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (go k []) = k * denote ctx []

Tactic:
rfl

Result:
no goals

Proof state:
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (go k p) = k * denote ctx p

Tactic:
match p with
| [] => rfl
| (k', v) :: p => simp [Poly.mul.go, go_denote]

Result:
no goals

Proof state:
ctx : Context
k : Nat
p✝ : Poly
k' : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx (go k ((k', v) :: p)) = k * denote ctx ((k', v) :: p)

Tactic:
simp [Poly.mul.go, go_denote]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
lemma autMulEquivAutGalois_π (f : Aut F) (A : C) [IsGalois A] (a : F.obj A) :
    F.map (AutGalois.π F { obj := A, pt := a } (autMulEquivAutGalois F f).unop).hom a =
      f.hom.app A a

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop ((autMulEquivAutGalois F) f))).hom a =
    f.hom.app A a

Tactic:
dsimp [autMulEquivAutGalois, endMulEquivAutGalois]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ F.map
      ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ })
          ((endEquivAutGalois F) ↑((Aut.unitsEndEquivAut F).symm f))).hom
      a =
    f.hom.app A a

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ F.map
      ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ })
          ((endEquivAutGalois F) ↑((Aut.unitsEndEquivAut F).symm f))).hom
      a =
    f.hom.app A a

Tactic:
rw [endEquivAutGalois_π]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ (↑((Aut.unitsEndEquivAut F).symm f)).app { obj := A, pt := a, isGalois := ⋯ }.obj
      { obj := A, pt := a, isGalois := ⋯ }.pt =
    f.hom.app A a

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ (↑((Aut.unitsEndEquivAut F).symm f)).app { obj := A, pt := a, isGalois := ⋯ }.obj
      { obj := A, pt := a, isGalois := ⋯ }.pt =
    f.hom.app A a

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem rightInv_coeff_zero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

Tactic:
rw [rightInv]

Result:
no goals
-- Mathlib/Algebra/Field/Power.lean
theorem Odd.neg_zpow (h : Odd n) (a : α) : (-a) ^ n = -a ^ n

Proof state:
α : Type u_1
inst✝ : DivisionRing α
a : α
h : Odd 0
⊢ False

Tactic:
exact Int.not_even_iff_odd.2 h .zero

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n

Tactic:
have hn : n ≠ 0 := by rintro rfl; exact Int.not_even_iff_odd.2 h .zero

Result:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
a : α
hn : n ≠ 0
⊢ (-a) ^ n = -a ^ n

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
a : α
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DivisionRing α
a : α
h : Odd 0
⊢ False

Proof state:
case intro
α : Type u_1
inst✝ : DivisionRing α
a : α
k : ℤ
hn : 2 * k + 1 ≠ 0
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)

Tactic:
simp_rw [zpow_add' (.inr (.inl hn)), zpow_one, zpow_mul, zpow_two, neg_mul_neg,
  neg_mul_eq_mul_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
a : α
hn : n ≠ 0
⊢ (-a) ^ n = -a ^ n

Tactic:
obtain ⟨k, rfl⟩ := h

Result:
case intro
α : Type u_1
inst✝ : DivisionRing α
a : α
k : ℤ
hn : 2 * k + 1 ≠ 0
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_D₁ [HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] :
    ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
      d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{u_13, u_1} C₁
inst✝¹⁹ : Category.{u_14, u_2} C₂
inst✝¹⁸ : Category.{u_15, u_5} C₃
inst✝¹⁷ : Category.{u_16, u_6} C₄
inst✝¹⁶ : Category.{u_17, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
⊢ ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
simp [D₁]

Result:
no goals
-- Mathlib/Probability/Process/HittingTime.lean
theorem stoppedValue_hitting_mem [ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι]
    {u : ι → Ω → β} {s : Set β} {n m : ι} {ω : Ω} (h : ∃ j ∈ Set.Icc n m, u j ω ∈ s) :
    stoppedValue u (hitting u s n m) ω ∈ s

Proof state:
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
this : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Tactic:
exact this.2

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h

Result:
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Proof state:
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Tactic:
have : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s} :=
  csInf_mem (Set.nonempty_of_mem ⟨hj₁, hj₂⟩)

Result:
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
this : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ stoppedValue u (hitting u s n m) ω ∈ s

Tactic:
simp only [stoppedValue, hitting, if_pos h]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
inst✝ : WellFoundedLT ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic.irreducible_rat {n : ℕ} (hpos : 0 < n) : Irreducible (cyclotomic n ℚ)

Proof state:
n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℚ)

Tactic:
rw [← map_cyclotomic_int]

Result:
n : ℕ
hpos : 0 < n
⊢ Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))

Proof state:
n : ℕ
hpos : 0 < n
⊢ Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))

Tactic:
exact (IsPrimitive.irreducible_iff_irreducible_map_fraction_map (cyclotomic.isPrimitive n ℤ)).1
  (cyclotomic.irreducible hpos)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getLast?_attachWith {P : α → Prop} {xs : List α}
    {H : ∀ (a : α), a ∈ xs → P a} :
    (xs.attachWith P H).getLast? = xs.getLast?.pbind (fun a h => some ⟨a, H _ (mem_of_getLast? h)⟩)

Proof state:
α : Type u_1
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.attachWith P H).getLast? = xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
rw [getLast?_eq_head?_reverse, reverse_attachWith, head?_attachWith]

Result:
α : Type u_1
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.reverse.head?.pbind fun a h => some ⟨a, ⋯⟩) = xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩

Proof state:
α : Type u_1
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.reverse.head?.pbind fun a h => some ⟨a, ⋯⟩) = xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Homotopy/Product.lean
theorem projLeft_prod : projLeft (prod q₁ q₂) = q₁

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projLeft (prod q₁ q₂) = q₁

Tactic:
induction q₁, q₂ using Quotient.inductionOn₂

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ projLeft (prod ⟦a✝⟧ ⟦b✝⟧) = ⟦a✝⟧

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ projLeft (prod ⟦a✝⟧ ⟦b✝⟧) = ⟦a✝⟧

Tactic:
rw [projLeft, prod_lift, ← Path.Homotopic.map_lift]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ ⟦(a✝.prod b✝).map ⋯⟧ = ⟦a✝⟧

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ ⟦(a✝.prod b✝).map ⋯⟧ = ⟦a✝⟧

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.and_contra' (a : BitVec w) : ~~~a &&& a = 0#w

Proof state:
w : Nat
a : BitVec w
⊢ ~~~a &&& a = 0#w

Tactic:
ext i h

Result:
case pred
w : Nat
a : BitVec w
i : Nat
h : i < w
⊢ (~~~a &&& a).getLsbD i = (0#w).getLsbD i

Proof state:
case pred
w : Nat
a : BitVec w
i : Nat
h : i < w
⊢ (~~~a &&& a).getLsbD i = (0#w).getLsbD i

Tactic:
simp [h]

Result:
no goals