harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/PartrecCode.lean
theorem eval_prec_zero (cf cg : Code) (a : ℕ) : eval (prec cf cg) (Nat.pair a 0) = eval cf a

Proof state:
cf cg : Code
a : ℕ
⊢ Nat.rec (cf.eval (a, 0).1)
      (fun y IH => do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a

Tactic:
simp (config := { Lean.Meta.Simp.neutralConfig with proj := true }) only []

Result:
cf cg : Code
a : ℕ
⊢ Nat.rec (cf.eval a)
      (fun y IH => do
        let i ← IH
        cg.eval (Nat.pair a (Nat.pair y i)))
      0 =
    cf.eval a

Proof state:
cf cg : Code
a : ℕ
⊢ (cf.prec cg).eval (Nat.pair a 0) = cf.eval a

Tactic:
rw [eval, Nat.unpaired, Nat.unpair_pair]

Result:
cf cg : Code
a : ℕ
⊢ Nat.rec (cf.eval (a, 0).1)
      (fun y IH => do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a

Proof state:
cf cg : Code
a : ℕ
⊢ Nat.rec (cf.eval a)
      (fun y IH => do
        let i ← IH
        cg.eval (Nat.pair a (Nat.pair y i)))
      0 =
    cf.eval a

Tactic:
rw [Nat.rec_zero]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem mul_moveRight_inr {x y : PGame} {i j} :
    (x * y).moveRight (toRightMovesMul (Sum.inr (i, j))) =
      x.moveRight i * y + x * y.moveLeft j - x.moveRight i * y.moveLeft j

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesMul (Sum.inr (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveLeft j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * (mk α✝ β✝ a✝¹ a✝).moveLeft j

Tactic:
rfl

Result:
no goals

Proof state:
case mk
y : PGame
j : y.LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveRight (toRightMovesMul (Sum.inr (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveRight i * y + mk α✝ β✝ a✝¹ a✝ * y.moveLeft j - (mk α✝ β✝ a✝¹ a✝).moveRight i * y.moveLeft j

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesMul (Sum.inr (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveLeft j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i * (mk α✝ β✝ a✝¹ a✝).moveLeft j

Proof state:
x y : PGame
i : x.RightMoves
j : y.LeftMoves
⊢ (x * y).moveRight (toRightMovesMul (Sum.inr (i, j))) =
    x.moveRight i * y + x * y.moveLeft j - x.moveRight i * y.moveLeft j

Tactic:
cases x

Result:
case mk
y : PGame
j : y.LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveRight (toRightMovesMul (Sum.inr (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveRight i * y + mk α✝ β✝ a✝¹ a✝ * y.moveLeft j - (mk α✝ β✝ a✝¹ a✝).moveRight i * y.moveLeft j
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_interval {a b : ℝ} : volume (uIcc a b) = ofReal |b - a|

Proof state:
a b : ℝ
⊢ volume (uIcc a b) = ofReal |b - a|

Tactic:
rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem udiv_eq_and {x y : BitVec 1} :
    x / y = (x &&& y)

Proof state:
x y : BitVec 1
⊢ x / y = x &&& y

Tactic:
have hx : x = 0#1 ∨ x = 1#1 := by bv_omega

Result:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ x / y = x &&& y

Proof state:
x y : BitVec 1
⊢ x = 0#1 ∨ x = 1#1

Tactic:
bv_omega

Result:
no goals

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ x / y = x &&& y

Tactic:
have hy : y = 0#1 ∨ y = 1#1 := by bv_omega

Result:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
hy : y = 0#1 ∨ y = 1#1
⊢ x / y = x &&& y

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
hy : y = 0#1 ∨ y = 1#1
⊢ x / y = x &&& y

Tactic:
rcases hx with rfl | rfl <;>
  rcases hy with rfl | rfl <;>
    rfl

Result:
no goals

Proof state:
x y : BitVec 1
hx : x = 0#1 ∨ x = 1#1
⊢ y = 0#1 ∨ y = 1#1

Tactic:
bv_omega

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma cross_self (v : ℙ F (Fin 3 → F)) : cross v v = v

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : ℙ F (Fin 3 → F)
⊢ v.cross v = v

Tactic:
induction v with | h v hv =>
rw [cross_mk_of_cross_eq_zero]
rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]

Result:
no goals

Proof state:
case h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
⊢ (crossProduct v) v = 0

Tactic:
rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]

Result:
no goals

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
⊢ (mk F v hv).cross (mk F v hv) = mk F v hv

Tactic:
rw [cross_mk_of_cross_eq_zero]

Result:
case h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
⊢ (crossProduct v) v = 0
-- Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean
theorem measurableEquiv_range_coe_nat_of_infinite_of_countable [Infinite α] [Countable α] :
    Nonempty (α ≃ᵐ range ((↑) : ℕ → ℝ))

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ α ≃ ↑(range Nat.cast)

Tactic:
refine (nonempty_equiv_of_countable.some : α ≃ ℕ).trans ?_

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ ℕ ≃ ↑(range Nat.cast)

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))

Tactic:
have : PolishSpace (range ((↑) : ℕ → ℝ)) :=
  Nat.isClosedEmbedding_coe_real.isClosedMap.isClosed_range.polishSpace

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ Nonempty (α ≃ᵐ ↑(range Nat.cast))

Tactic:
refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ α ≃ ↑(range Nat.cast)

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : StandardBorelSpace α
inst✝¹ : Infinite α
inst✝ : Countable α
this : PolishSpace ↑(range Nat.cast)
⊢ ℕ ≃ ↑(range Nat.cast)

Tactic:
exact Equiv.ofInjective ((↑) : ℕ → ℝ) Nat.cast_injective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_xor (x y : BitVec v) :
    BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y

Proof state:
v : Nat
x y : BitVec v
⊢ (x ^^^ y).toFin = x.toFin ^^^ y.toFin

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
v : Nat
x y : BitVec v
⊢ ↑(x ^^^ y).toFin = ↑(x.toFin ^^^ y.toFin)

Proof state:
case a
v : Nat
x y : BitVec v
⊢ ↑(x ^^^ y).toFin = ↑(x.toFin ^^^ y.toFin)

Tactic:
exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_lt_smul_of_neg_left (hb : b₁ < b₂) (ha : a < 0) : a • b₂ < a • b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ -a • b₁ < -a • b₂

Tactic:
exact smul_lt_smul_of_pos_left hb (neg_pos_of_neg ha)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ a • b₂ < a • b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff]

Result:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ -a • b₁ < -a • b₂
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem left_nonuniformWitnesses_card (h : ¬G.IsUniform ε s t) :
    #s * ε ≤ #(G.nonuniformWitnesses ε s t).1

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(⋯.choose, ⋯.choose).1)

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.1

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).1)

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(⋯.choose, ⋯.choose).1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_eq_foldr_reverse (l : Vector α n) (f : β → α → β) (b) :
    l.foldl f b = l.reverse.foldr (fun x y => f y x) b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : β → α → β
b : β
⊢ foldl f b l = foldr (fun x y => f y x) b l.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem dist_eq_re_im (z w : ℂ) : dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)

Proof state:
z w : ℂ
⊢ dist z w = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))

Tactic:
rfl

Result:
no goals

Proof state:
z w : ℂ
⊢ dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)

Tactic:
rw [sq, sq]

Result:
z w : ℂ
⊢ dist z w = √((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem transpose_adjMatrix [Zero α] [One α] : (G.adjMatrix α)ᵀ = G.adjMatrix α

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G)ᵀ = adjMatrix α G

Tactic:
ext

Result:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : V
⊢ (adjMatrix α G)ᵀ i✝ j✝ = adjMatrix α G i✝ j✝

Proof state:
case a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : V
⊢ (adjMatrix α G)ᵀ i✝ j✝ = adjMatrix α G i✝ j✝

Tactic:
simp [adj_comm]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem prod_singleton : s ×ˢ ({b} : Set β) = (fun a => (a, b)) '' s

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s : Set α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ (fun a => (a, b)) '' s

Tactic:
simp [and_left_comm, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ s ×ˢ {b} = (fun a => (a, b)) '' s

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s : Set α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ (fun a => (a, b)) '' s
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem transpose {M : Matrix n n R} (hM : M.PosSemidef) : Mᵀ.PosSemidef

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
x : n → R
⊢ 0 ≤ star x ⬝ᵥ Mᵀ *ᵥ x

Tactic:
convert hM.2 (star x) using 1

Result:
case h.e'_4
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
x : n → R
⊢ star x ⬝ᵥ Mᵀ *ᵥ x = star (star x) ⬝ᵥ M *ᵥ star x

Proof state:
case h.e'_4
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
x : n → R
⊢ star x ⬝ᵥ Mᵀ *ᵥ x = star (star x) ⬝ᵥ M *ᵥ star x

Tactic:
rw [mulVec_transpose, dotProduct_mulVec, star_star, dotProduct_comm]

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
⊢ Mᵀ.PosSemidef

Tactic:
refine ⟨IsHermitian.transpose hM.1, fun x => ?_⟩

Result:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
x : n → R
⊢ 0 ≤ star x ⬝ᵥ Mᵀ *ᵥ x
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
/-- Reorder a product.

The difference with `Finset.prod_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.prod_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the product. -/
@[to_additive "Reorder a sum.

The difference with `Finset.sum_nbij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.sum_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the sum."]
lemma prod_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set ι).InjOn i)
    (i_surj : (s : Set ι).SurjOn i t) (h : ∀ a ∈ s, f a = g (i a)) :
    ∏ x ∈ s, f x = ∏ x ∈ t, g x :=
  prod_bij (fun a _ ↦ i a) hi i_inj (by simpa using i_surj) h

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
h : ∀ a ∈ s, f a = g (i a)
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), (fun a x => i a) a ha = b

Tactic:
simpa using i_surj

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
theorem Functor.rightDerived_map_eq (F : C ⥤ D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y)
    {P : InjectiveResolution X} {Q : InjectiveResolution Y} (g : P.cocomplex ⟶ Q.cocomplex)
    (w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι) :
    (F.rightDerived n).map f =
      (P.isoRightDerivedObj F n).hom ≫
        (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map g ≫
          (Q.isoRightDerivedObj F n).inv

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ P.ι.f 0 ≫ g.f 0 = f ≫ Q.ι.f 0

Tactic:
rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
  CochainComplex.single₀_map_f_zero]

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (F.rightDerived n).map f =
    (P.isoRightDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map g ≫
        (Q.isoRightDerivedObj F n).inv

Tactic:
rw [← cancel_mono (Q.isoRightDerivedObj F n).hom,
  InjectiveResolution.isoRightDerivedObj_hom_naturality f P Q g _ F n,
  assoc, assoc, Iso.inv_hom_id, comp_id]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ P.ι.f 0 ≫ g.f 0 = f ≫ Q.ι.f 0
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem zero_le (I : FractionalIdeal S P) : 0 ≤ I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ 0 ∈ I

Tactic:
exact zero_mem I

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ x ∈ I

Tactic:
rw [(mem_zero_iff _).mp hx]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ 0 ∈ I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ 0 ≤ I

Tactic:
intro x hx

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
x : P
hx : x ∈ 0
⊢ x ∈ I
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_right_Ico (a b c : α) : ((Ico a b).map fun x => x + c) = Ico (a + c) (b + c)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Result:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
exact map_add_left_Ico _ _ _

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Right.inv_lt_one_iff : a⁻¹ < 1 ↔ 1 < a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a : α
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nndist_eq_sup [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp ∞ (α × β)) :
    nndist x y = nndist x.fst y.fst ⊔ nndist x.snd y.snd :=
  NNReal.eq <| by
    push_cast
    exact prod_dist_eq_sup _ _

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x y : WithLp ⊤ (α × β)
⊢ ↑(nndist x y) = ↑(nndist x.1 y.1 ⊔ nndist x.2 y.2)

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x y : WithLp ⊤ (α × β)
⊢ dist x y = dist x.1 y.1 ⊔ dist x.2 y.2

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x y : WithLp ⊤ (α × β)
⊢ dist x y = dist x.1 y.1 ⊔ dist x.2 y.2

Tactic:
exact prod_dist_eq_sup _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Reindex.lean
theorem reindexLinearEquiv_comp (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
    reindexLinearEquiv R A e₁' e₂' ∘ reindexLinearEquiv R A e₁ e₂ =
      reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')

Proof state:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ ⇑(reindexLinearEquiv R A e₁' e₂') ∘ ⇑(reindexLinearEquiv R A e₁ e₂) =
    ⇑(reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂')

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ ⇑(reindexLinearEquiv R A e₁' e₂') ∘ ⇑(reindexLinearEquiv R A e₁ e₂) =
    ⇑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))

Tactic:
rw [← reindexLinearEquiv_trans]

Result:
m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ ⇑(reindexLinearEquiv R A e₁' e₂') ∘ ⇑(reindexLinearEquiv R A e₁ e₂) =
    ⇑(reindexLinearEquiv R A e₁ e₂ ≪≫ₗ reindexLinearEquiv R A e₁' e₂')
-- Mathlib/ModelTheory/Semantics.lean
theorem boundedFormula_realize_eq_realize (φ : L.Formula α) (x : α → M) (y : Fin 0 → M) :
    BoundedFormula.Realize φ x y ↔ φ.Realize x

Proof state:
case e__xs.h
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
i : Fin 0
⊢ y i = default i

Tactic:
exact Fin.elim0 i

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ BoundedFormula.Realize φ x y ↔ φ.Realize x

Tactic:
rw [Formula.Realize, iff_iff_eq]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ BoundedFormula.Realize φ x y = BoundedFormula.Realize φ x default

Proof state:
case e__xs
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ y = default

Tactic:
ext i

Result:
case e__xs.h
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
i : Fin 0
⊢ y i = default i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ BoundedFormula.Realize φ x y = BoundedFormula.Realize φ x default

Tactic:
congr

Result:
case e__xs
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ y = default
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addXYZ_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) : W.addXYZ P Q = addU P Q • ![0, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.addXYZ P Q = addU P Q • ![0, 1, 0]

Tactic:
erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
  addZ_of_X_eq hP hQ hPz hQz hx, smul_fin3, mul_zero, mul_one]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[simp]
lemma preimage_image_eq (U : X.Opens) : f ⁻¹ᵁ f ''ᵁ U = U

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
⊢ f ⁻¹ᵁ f ''ᵁ U = U

Tactic:
apply Opens.ext

Result:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
⊢ ↑(f ⁻¹ᵁ f ''ᵁ U) = ↑U

Proof state:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
⊢ ↑(f ⁻¹ᵁ f ''ᵁ U) = ↑U

Tactic:
simp [Set.preimage_image_eq _ f.isOpenEmbedding.injective]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_neg : normSq (-a) = normSq a

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ normSq (-a) = normSq a

Tactic:
simp only [normSq_def, star_neg, neg_mul_neg]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
/-- An open ball in a product space is a product of open balls. See also `ball_pi`
for a version assuming `0 < r` instead of `Nonempty β`. -/
lemma ball_pi' [Nonempty β] (x : ∀ b, π b) (r : ℝ) :
    ball x r = Set.pi univ fun b => ball (x b) r :=
  (lt_or_le 0 r).elim (ball_pi x) fun hr => by simp [ball_eq_empty.2 hr]

Proof state:
β : Type u_2
π : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
x : (b : β) → π b
r : ℝ
hr : r ≤ 0
⊢ ball x r = Set.univ.pi fun b => ball (x b) r

Tactic:
simp [ball_eq_empty.2 hr]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
@[simp] lemma sdiff_eq_right : x \ y = y ↔ x = ⊥ ∧ y = ⊥

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = y ↔ x = ⊥ ∧ y = ⊥

Tactic:
rw [disjoint_sdiff_self_left.eq_iff]

Result:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥