harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Quandle.lean
theorem ad_conj {R : Type*} [Rack R] (x y : R) : act' (x ◃ y) = act' x * act' y * (act' x)⁻¹

Proof state:
R : Type u_2
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) * act' x = act' x * act' y

Tactic:
ext z

Result:
case H
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (act' (x ◃ y) * act' x) z = (act' x * act' y) z

Proof state:
case H
R : Type u_2
inst✝ : Rack R
x y z : R
⊢ (act' (x ◃ y) * act' x) z = (act' x * act' y) z

Tactic:
apply self_distrib.symm

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) = act' x * act' y * (act' x)⁻¹

Tactic:
rw [eq_mul_inv_iff_mul_eq]

Result:
R : Type u_2
inst✝ : Rack R
x y : R
⊢ act' (x ◃ y) * act' x = act' x * act' y
-- Mathlib/SetTheory/Game/Basic.lean
/-- Any left option of `x * y` of the first kind is also a left option of `x * -(-y)` of
  the first kind. -/
lemma mulOption_neg_neg {x} (y) {i j} :
    mulOption x y i j = mulOption x (-(-y)) i (toLeftMovesNeg <| toRightMovesNeg j)

Proof state:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ x.mulOption y i j = x.mulOption (- -y) i (toLeftMovesNeg (toRightMovesNeg j))

Tactic:
simp [mulOption]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD k]) (L : List ℕ) :
    ofDigits b L ≡ ofDigits b' L [ZMOD k]

Proof state:
case cons
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d + b * ofDigits b L) % ↑k = (↑d + b' * ofDigits b' L) % ↑k

Tactic:
conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]

Result:
case cons
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d % ↑k + b' % ↑k * (ofDigits b' L % ↑k) % ↑k) % ↑k = (↑d + b' * ofDigits b' L) % ↑k

Proof state:
case cons
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD ↑k]

Tactic:
dsimp [ofDigits]

Result:
case cons
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ↑d + b * ofDigits b L ≡ ↑d + b' * ofDigits b' L [ZMOD ↑k]

Proof state:
case cons
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ↑d + b * ofDigits b L ≡ ↑d + b' * ofDigits b' L [ZMOD ↑k]

Tactic:
dsimp [Int.ModEq] at *

Result:
case cons
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d + b * ofDigits b L) % ↑k = (↑d + b' * ofDigits b' L) % ↑k

Proof state:
case nil
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD ↑k]

Tactic:
rfl

Result:
no goals

Proof state:
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]

Tactic:
induction' L with d L ih

Result:
case nil
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD ↑k]

case cons
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD ↑k]

Proof state:
case cons
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d % ↑k + b' % ↑k * (ofDigits b' L % ↑k) % ↑k) % ↑k = (↑d + b' * ofDigits b' L) % ↑k

Tactic:
conv_rhs => rw [Int.add_emod, Int.mul_emod]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma sub_apply' (ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a / χ a

Proof state:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ (ψ - χ) a = ψ a / χ a

Tactic:
rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem EqOnSource.source_inter_preimage_eq {e e' : PartialEquiv α β} (he : e ≈ e') (s : Set β) :
    e.source ∩ e ⁻¹' s = e'.source ∩ e' ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s

Tactic:
rw [he.eqOn.inter_preimage_eq, source_eq he]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem toZModPow_compat (m n : ℕ) (h : m ≤ n) :
    (ZMod.castHom (pow_dvd_pow p h) (ZMod (p ^ m))).comp (toZModPow p n) = toZModPow p m :=
  calc
    (ZMod.castHom _ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n))
    _ = ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp
          (truncate n)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)) =
    ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp (truncate n)

Tactic:
rw [commutes_symm, RingHom.comp_assoc]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp (truncate n) =
    (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m)

Tactic:
rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose [Fintype ι']
    (a : OrthonormalBasis ι 𝕜 E) (b : OrthonormalBasis ι' 𝕜 E) :
    a.toBasis.toMatrix b * (a.toBasis.toMatrix b)ᴴ = 1

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
⊢ a.toBasis.toMatrix ⇑b * (a.toBasis.toMatrix ⇑b)ᴴ = 1

Tactic:
rw [Matrix.mul_eq_one_comm_of_equiv (a.toBasis.indexEquiv b.toBasis),
  a.toMatrix_orthonormalBasis_conjTranspose_mul_self b]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
a : OrthonormalBasis ι 𝕜 E
b : OrthonormalBasis ι' 𝕜 E
⊢ a.toBasis.toMatrix ⇑b * (a.toBasis.toMatrix ⇑b)ᴴ = 1

Tactic:
classical
rw [Matrix.mul_eq_one_comm_of_equiv (a.toBasis.indexEquiv b.toBasis),
  a.toMatrix_orthonormalBasis_conjTranspose_mul_self b]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem measurableSet_sInf {ms : Set (MeasurableSpace α)} {s : Set α} :
    MeasurableSet[sInf ms] s ↔ ∀ m ∈ ms, MeasurableSet[m] s :=
  show s ∈ ⋂₀ _ ↔ _ by simp

Proof state:
α : Type u_1
ms : Set (MeasurableSpace α)
s : Set α
⊢ s ∈ ⋂₀ ((fun m => {t | MeasurableSet t}) '' ms) ↔ ∀ m ∈ ms, MeasurableSet s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
@[reassoc (attr := simp)]
lemma inv_hom_id_hom_app (e : F ≅ G) (n : A) (X : C) :
    (e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
X : C
⊢ (e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)

Tactic:
rw [← NatTrans.comp_app, inv_hom_id_hom, NatTrans.id_app]

Result:
no goals
-- Mathlib/Order/DirectedInverseSystem.lean
theorem piSplitLE_eq {f : piLT X i × X i} :
    piSplitLE f ⟨i, le_rfl⟩ = f.2

Proof state:
ι : Type u_6
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
⊢ piSplitLE f ⟨i, ⋯⟩ = f.2

Tactic:
simp [piSplitLE]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem le_ker_iff_map (M' : LieSubmodule R L M) : M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
M' : LieSubmodule R L M
⊢ M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥

Tactic:
rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem lexOrder_eq_top_iff_eq_zero (φ : MvPowerSeries σ R) :
    lexOrder φ = ⊤ ↔ φ = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
⊢ φ.lexOrder = ⊤ ↔ φ = 0

Tactic:
unfold lexOrder

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
⊢ (if h : φ = 0 then ⊤
      else
        let_fun ne := ⋯;
        ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
      ⊤ ↔
    φ = 0

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : φ = 0
⊢ ⊤ = ⊤ ↔ φ = 0

Tactic:
simp only [h]

Result:
no goals

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ (let_fun ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
      ⊤ ↔
    φ = 0

Tactic:
simp only [h, WithTop.coe_ne_top]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
⊢ (if h : φ = 0 then ⊤
      else
        let_fun ne := ⋯;
        ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
      ⊤ ↔
    φ = 0

Tactic:
split_ifs with h

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : φ = 0
⊢ ⊤ = ⊤ ↔ φ = 0

case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ (let_fun ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
      ⊤ ↔
    φ = 0
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem comp_dite {P : Prop} [Decidable P]
    {X Y Z : C} (f : X ⟶ Y) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) :
    (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem comapDomain_single [DecidableEq ι] [DecidableEq κ] [∀ i, Zero (β i)] (h : κ → ι)
    (hh : Function.Injective h) (k : κ) (x : β (h k)) :
    comapDomain h hh (single (h k) x) = single k x

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (comapDomain h hh (single (h k) x)) i = (single k x) i

Tactic:
rw [comapDomain_apply]

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (single (h k) x) (h i) = (single k x) i

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (single (h k) x) (h i) = (single k x) i

Tactic:
obtain rfl | hik := Decidable.eq_or_ne i k

Result:
case h.inl
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
x : β (h i)
⊢ (single (h i) x) (h i) = (single i x) i

case h.inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = (single k x) i

Proof state:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
⊢ comapDomain h hh (single (h k) x) = single k x

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (comapDomain h hh (single (h k) x)) i = (single k x) i

Proof state:
case h.inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = (single k x) i

Tactic:
rw [single_eq_of_ne hik.symm, single_eq_of_ne (hh.ne hik.symm)]

Result:
no goals

Proof state:
case h.inl
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
x : β (h i)
⊢ (single (h i) x) (h i) = (single i x) i

Tactic:
rw [single_eq_same, single_eq_same]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- If the (coproduct-like) biproduct comparison for `F`, `X` and `Y` is an epimorphism, then
    `F` preserves the biproduct of `X` and `Y`. For the converse, see `mapBiprod`. -/
lemma preservesBinaryBiproduct_of_epi_biprodComparison' {X Y : C} [HasBinaryBiproduct X Y]
    [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Epi (biprodComparison' F X Y)] :
    PreservesBinaryBiproduct X Y F

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
this✝ : Epi (F.splitEpiBiprodComparison X Y).section_
this : IsIso (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F

Tactic:
apply preservesBinaryBiproduct_of_mono_biprodComparison

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
⊢ Epi (F.splitEpiBiprodComparison X Y).section_

Tactic:
simpa

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
this : Epi (F.splitEpiBiprodComparison X Y).section_
⊢ PreservesBinaryBiproduct X Y F

Tactic:
haveI : IsIso (biprodComparison F X Y) :=
  IsIso.of_epi_section' (splitEpiBiprodComparison F X Y)

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
this✝ : Epi (F.splitEpiBiprodComparison X Y).section_
this : IsIso (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
⊢ PreservesBinaryBiproduct X Y F

Tactic:
haveI : Epi (splitEpiBiprodComparison F X Y).section_ := by simpa

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
this : Epi (F.splitEpiBiprodComparison X Y).section_
⊢ PreservesBinaryBiproduct X Y F
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_lt_div_of_neg (hb : b < 0) : 1 < a / b ↔ a < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ 1 < a / b ↔ a < b

Tactic:
rw [lt_div_iff_of_neg hb, one_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem of_subsingleton [Subsingleton M] (x y : M) : SameRay R x y

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R x y

Tactic:
rw [Subsingleton.elim x 0]

Result:
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y

Tactic:
exact zero_left _

Result:
no goals
-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem tensorObj_comul (K L : CoalgebraCat R) :
    Coalgebra.comul (R := R) (A := (K ⊗ L : CoalgebraCat R))
      = (TensorProduct.tensorTensorTensorComm R K K L L).toLinearMap
      ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul

Proof state:
R : Type u
inst✝ : CommRing R
K L : CoalgebraCat R
⊢ ModuleCat.Hom.hom ((comonEquivalence R).symm.inverse.obj K ⊗ (comonEquivalence R).symm.inverse.obj L).comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj]

Result:
R : Type u
inst✝ : CommRing R
K L : CoalgebraCat R
⊢ ModuleCat.Hom.hom (K.toComonObj ⊗ L.toComonObj).comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Proof state:
R : Type u
inst✝ : CommRing R
K L : CoalgebraCat R
⊢ CoalgebraStruct.comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
rw [ofComonObjCoalgebraStruct_comul]

Result:
R : Type u
inst✝ : CommRing R
K L : CoalgebraCat R
⊢ ModuleCat.Hom.hom ((comonEquivalence R).symm.inverse.obj K ⊗ (comonEquivalence R).symm.inverse.obj L).comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Proof state:
R : Type u
inst✝ : CommRing R
K L : CoalgebraCat R
⊢ ModuleCat.Hom.hom (K.toComonObj ⊗ L.toComonObj).comul =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
simp only [Comon_.monoidal_tensorObj_comul, toComonObj_X, ModuleCat.of_coe, toComonObj_comul,
  tensorμ_eq_tensorTensorTensorComm]

Result:
R : Type u
inst✝ : CommRing R
K L : CoalgebraCat R
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
        ModuleCat.ofHom
          ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat)) =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Proof state:
R : Type u
inst✝ : CommRing R
K L : CoalgebraCat R
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
        ModuleCat.ofHom
          ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat)) =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- Expectation over a product set equals the expectation of the fiberwise expectations.

For rewriting in the reverse direction, use `Finset.expect_product`. -/
lemma expect_product' (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
    𝔼 i ∈ s ×ˢ t, f i.1 i.2 = 𝔼 i ∈ s, 𝔼 j ∈ t, f i j

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ 𝔼 i ∈ s ×ˢ t, f i.1 i.2 = 𝔼 i ∈ s, 𝔼 j ∈ t, f i j

Tactic:
simp only [expect, card_product, sum_product', smul_sum, mul_inv, mul_smul, Nat.cast_mul]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBy_one : torsionBy R M 1 = ⊥ :=
  eq_bot_iff.mpr fun _ h => by
    rw [mem_torsionBy_iff, one_smul] at h
    exact h

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
h : x✝ ∈ torsionBy R M 1
⊢ x✝ ∈ ⊥

Tactic:
rw [mem_torsionBy_iff, one_smul] at h

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥

Tactic:
exact h

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem PairwiseDisjoint.range (g : s → ι) (hg : ∀ i : s, f (g i) ≤ f i)
    (ht : s.PairwiseDisjoint f) : (range g).PairwiseDisjoint f

Proof state:
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : s.PairwiseDisjoint f
⊢ (Set.range g).PairwiseDisjoint f

Tactic:
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy

Result:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : s.PairwiseDisjoint f
x y : ↑s
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)

Proof state:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : s.PairwiseDisjoint f
x y : ↑s
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)

Tactic:
exact ((ht x.2 y.2) fun h => hxy <| congr_arg g <| Subtype.ext h).mono (hg x) (hg y)

Result:
no goals
-- Mathlib/Algebra/Regular/SMul.lean
theorem not_zero_iff : ¬IsSMulRegular M (0 : R) ↔ Nontrivial M

Proof state:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ ¬IsSMulRegular M 0 ↔ Nontrivial M

Tactic:
rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]

Result:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y

Proof state:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y

Tactic:
push_neg

Result:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)] lemma w₁₃_τ₃ : S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0

Tactic:
rw [← comp_τ₃, S.w₁₃, zero_τ₃]

Result:
no goals