harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorZero_inv_app_shift (n : A) :
    (shiftFunctorZero C A).inv.app (X⟦n⟧) =
  ((shiftFunctorZero C A).inv.app X)⟦n⟧' ≫ (shiftFunctorComm C n 0).inv.app X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X) =
    (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫ (shiftFunctorComm C n 0).inv.app X

Tactic:
rw [← cancel_mono ((shiftFunctorZero C A).hom.app (X⟦n⟧)), Category.assoc, Iso.inv_hom_id_app,
  shiftFunctorZero_hom_app_shift, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
  Iso.inv_hom_id_app]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) = (shiftFunctor C n).map (𝟙 ((𝟭 C).obj X))

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((shiftFunctor C n).obj X) = (shiftFunctor C n).map (𝟙 X)

Tactic:
rw [Functor.map_id]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) = (shiftFunctor C n).map (𝟙 ((𝟭 C).obj X))

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((shiftFunctor C n).obj X) = (shiftFunctor C n).map (𝟙 X)
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem HasProd.mul_disjoint {s t : Set β} (hs : Disjoint s t) (ha : HasProd (f ∘ (↑) : s → α) a)
    (hb : HasProd (f ∘ (↑) : t → α) b) : HasProd (f ∘ (↑) : (s ∪ t : Set β) → α) (a * b)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd (fun a => s.mulIndicator f a * t.mulIndicator f a) (a * b)

Tactic:
exact ha.mul hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd ((s ∪ t).mulIndicator f) (a * b)

Tactic:
rw [Set.mulIndicator_union_of_disjoint hs]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd (fun a => s.mulIndicator f a * t.mulIndicator f a) (a * b)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (f ∘ Subtype.val) a
hb : HasProd (f ∘ Subtype.val) b
⊢ HasProd (f ∘ Subtype.val) (a * b)

Tactic:
rw [hasProd_subtype_iff_mulIndicator] at *

Result:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd ((s ∪ t).mulIndicator f) (a * b)
-- Mathlib/Data/Set/Lattice.lean
theorem bijective_iff_bijective_of_iUnion_eq_univ :
    Bijective f ↔ ∀ i, Bijective ((U i).restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Bijective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU,
  surjective_iff_surjective_of_iUnion_eq_univ hU]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔
    ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔
    ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
simp [Bijective, forall_and]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma pred_eq_self_iff : n.pred = n ↔ n = 0

Proof state:
n : ℕ
⊢ n.pred = n ↔ n = 0

Tactic:
cases n <;> simp [(Nat.succ_ne_self _).symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n

Proof state:
n : Nat
x : BitVec n
⊢ (-x).toNat = (2 ^ n - x.toNat) % 2 ^ n

Tactic:
simp [Neg.neg, BitVec.neg]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_of_retract {f : K ⟶ L} {f' : K' ⟶ L'}
    (h : RetractArrow f f') (i : ι) [K.HasHomology i] [L.HasHomology i]
    [K'.HasHomology i] [L'.HasHomology i] [hf' : QuasiIsoAt f' i] :
    QuasiIsoAt f i

Proof state:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst✝³ : K.HasHomology i
inst✝² : L.HasHomology i
inst✝¹ : K'.HasHomology i
inst✝ : L'.HasHomology i
hf' : ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f')
this : RetractArrow ((shortComplexFunctor C c i).map f) ((shortComplexFunctor C c i).map f')
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
exact ShortComplex.quasiIso_of_retract this

Result:
no goals

Proof state:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst✝³ : K.HasHomology i
inst✝² : L.HasHomology i
inst✝¹ : K'.HasHomology i
inst✝ : L'.HasHomology i
hf' : ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f')
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
have : RetractArrow ((shortComplexFunctor C c i).map f)
  ((shortComplexFunctor C c i).map f') := h.map (shortComplexFunctor C c i).mapArrow

Result:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst✝³ : K.HasHomology i
inst✝² : L.HasHomology i
inst✝¹ : K'.HasHomology i
inst✝ : L'.HasHomology i
hf' : ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f')
this : RetractArrow ((shortComplexFunctor C c i).map f) ((shortComplexFunctor C c i).map f')
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Proof state:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst✝³ : K.HasHomology i
inst✝² : L.HasHomology i
inst✝¹ : K'.HasHomology i
inst✝ : L'.HasHomology i
hf' : QuasiIsoAt f' i
⊢ QuasiIsoAt f i

Tactic:
rw [quasiIsoAt_iff] at hf' ⊢

Result:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst✝³ : K.HasHomology i
inst✝² : L.HasHomology i
inst✝¹ : K'.HasHomology i
inst✝ : L'.HasHomology i
hf' : ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f')
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
    (id_map : ∀ {α} (x : m α), id <$> x = x)
    (pure_bind : ∀ {α β} (x : α) (f : α → m β), pure x >>= f = f x)
    (bind_assoc : ∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ),
      x >>= f >>= g = x >>= fun x => f x >>= g)
    (map_const : ∀ {α β} (x : α) (y : m β),
      Functor.mapConst x y = Function.const β x <$> y

Proof state:
m : Type u → Type v
inst✝ : Monad m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝
seqLeft_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = do
        let a ← x
        let _ ← y
        pure a)
    _auto✝
seqRight_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y)
    _auto✝
bind_pure_comp :
  autoParam
    (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x)
    _auto✝
bind_map :
  autoParam
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x)
    _auto✝
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
α✝ β✝ : Type u
x : m α✝
y : m β✝
⊢ x *> y = const α✝ id <$> x <*> y

Tactic:
rw [seqRight_eq, ← bind_map, ← bind_pure_comp, bind_assoc]

Result:
m : Type u → Type v
inst✝ : Monad m
id_map : ∀ {α : Type u} (x : m α), id <$> x = x
pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝
seqLeft_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x <* y = do
        let a ← x
        let _ ← y
        pure a)
    _auto✝
seqRight_eq :
  autoParam
    (∀ {α β : Type u} (x : m α) (y : m β),
      x *> y = do
        let _ ← x
        y)
    _auto✝
bind_pure_comp :
  autoParam
    (∀ {α β : Type u} (f : α → β) (x : m α),
      (do
          let y ← x
          pure (f y)) =
        f <$> x)
    _auto✝
bind_map :
  autoParam
    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
      (do
          let x_1 ← f
          x_1 <$> x) =
        f <*> x)
    _auto✝
map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
α✝ β✝ : Type u
x : m α✝
y : m β✝
⊢ (do
      let _ ← x
      y) =
    do
    let x ← x
    let x ← pure (const α✝ id x)
    x <$> y
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem DvdNotUnit.ne [CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) : p ≠ q

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
h : DvdNotUnit p q
⊢ p ≠ q

Tactic:
by_contra hcontra

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
h : DvdNotUnit p q
hcontra : p = q
⊢ False

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
h : DvdNotUnit p q
hcontra : p = q
⊢ False

Tactic:
obtain ⟨hp, x, hx', hx''⟩ := h

Result:
case intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit x
hx'' : q = p * x
⊢ False

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit 1
hx'' : p * 1 = p * x
⊢ False

Tactic:
exact hx' isUnit_one

Result:
no goals

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit x
hx'' : p * 1 = p * x
⊢ False

Tactic:
rw [(mul_left_cancel₀ hp hx'').symm] at hx'

Result:
case intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit 1
hx'' : p * 1 = p * x
⊢ False

Proof state:
case intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit x
hx'' : q = p * x
⊢ False

Tactic:
conv_lhs at hx'' => rw [← hcontra, ← mul_one p]

Result:
case intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit x
hx'' : p * 1 = p * x
⊢ False
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_singleton_eq_top {x} : span ({x} : Set α) = ⊤ ↔ IsUnit x

Proof state:
α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ IsUnit x

Tactic:
rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v'

Proof state:
α : Type u_1
γ : Sort u_2
β : Type u_3
u u' : α → γ
v v' : β → γ
⊢ Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v'

Tactic:
simp [funext_iff, Sum.forall]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem le_minFac' {m n : ℕ} : n = 1 ∨ m ≤ minFac n ↔ ∀ p, 2 ≤ p → p ∣ n → m ≤ p :=
  ⟨fun h p (pp : 1 < p) d =>
    h.elim (by rintro rfl; cases not_le_of_lt pp (le_of_dvd (by decide) d)) fun h =>
      le_trans h <| minFac_le_of_dvd pp d,
    fun H => le_minFac.2 fun p pp d => H p pp.two_le d⟩

Proof state:
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p

Tactic:
cases not_le_of_lt pp (le_of_dvd (by decide) d)

Result:
no goals

Proof state:
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
m n : ℕ
h : n = 1 ∨ m ≤ n.minFac
p : ℕ
pp : 1 < p
d : p ∣ n
⊢ n = 1 → m ≤ p

Tactic:
rintro rfl

Result:
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
-- Mathlib/Data/Vector/Mem.lean
theorem not_mem_map_zero (b : β) (v : Vector α 0) (f : α → β) : b ∉ (v.map f).toList

Proof state:
α : Type u_1
β : Type u_2
b : β
v : Vector α 0
f : α → β
⊢ b ∉ (map f v).toList

Tactic:
simpa only [Vector.eq_nil v, Vector.map_nil, Vector.toList_nil] using List.not_mem_nil b

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_vecMul_cons (x : α) (v : Fin n → α) (w : o' → α) (B : Fin n → o' → α) :
    vecCons x v ᵥ* of (vecCons w B) = x • w + v ᵥ* of B

Proof state:
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
w : o' → α
B : Fin n → o' → α
⊢ vecCons x v ᵥ* of (vecCons w B) = x • w + v ᵥ* of B

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem eq_iff_le_and_ge {x y : Int} : x = y ↔ x ≤ y ∧ y ≤ x

Proof state:
case mpr
x y : Int
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x = y

Tactic:
exact Int.le_antisymm h₁ h₂

Result:
no goals

Proof state:
x y : Int
⊢ x = y ↔ x ≤ y ∧ y ≤ x

Tactic:
constructor

Result:
case mp
x y : Int
⊢ x = y → x ≤ y ∧ y ≤ x

case mpr
x y : Int
⊢ x ≤ y ∧ y ≤ x → x = y

Proof state:
case mp
x y : Int
⊢ x = y → x ≤ y ∧ y ≤ x

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr
x y : Int
⊢ x ≤ y ∧ y ≤ x → x = y

Tactic:
intro ⟨h₁, h₂⟩

Result:
case mpr
x y : Int
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x = y
-- Mathlib/Algebra/Lie/Basic.lean
theorem neg_lie : ⁅-x, m⁆ = -⁅x, m⁆

Proof state:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x + x, m⁆ = 0

Tactic:
simp

Result:
no goals

Proof state:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x, m⁆ = -⁅x, m⁆

Tactic:
rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]

Result:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x + x, m⁆ = 0
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.sub (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) :
    StarConvex 𝕜 (x - y) (s - t)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x - y) (s - t)

Tactic:
simp_rw [sub_eq_add_neg]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + -y) (s + -t)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + -y) (s + -t)

Tactic:
exact hs.add ht.neg

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem ge_trans (h₁ : cmp x y ≠ .lt) (h₂ : cmp y z ≠ .lt) : cmp x z ≠ .lt

Proof state:
cmp✝ : ?m.1056 → ?m.1056 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1054
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y ≠ Ordering.lt
h₂ : cmp y z ≠ Ordering.lt
⊢ cmp x z ≠ Ordering.lt

Tactic:
have := @TransCmp.le_trans _ cmp _ z y x

Result:
cmp✝ : ?m.1056 → ?m.1056 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1054
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y ≠ Ordering.lt
h₂ : cmp y z ≠ Ordering.lt
this : cmp z y ≠ Ordering.gt → cmp y x ≠ Ordering.gt → cmp z x ≠ Ordering.gt
⊢ cmp x z ≠ Ordering.lt

Proof state:
cmp✝ : ?m.1056 → ?m.1056 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1054
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y ≠ Ordering.lt
h₂ : cmp y z ≠ Ordering.lt
this : cmp z y ≠ Ordering.gt → cmp y x ≠ Ordering.gt → cmp z x ≠ Ordering.gt
⊢ cmp x z ≠ Ordering.lt

Tactic:
simp [cmp_eq_gt] at *

Result:
cmp✝ : ?m.1056 → ?m.1056 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1054
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : ¬cmp x y = Ordering.lt
h₂ : ¬cmp y z = Ordering.lt
this : ¬cmp y z = Ordering.lt → ¬cmp x y = Ordering.lt → ¬cmp x z = Ordering.lt
⊢ ¬cmp x z = Ordering.lt

Proof state:
cmp✝ : ?m.1056 → ?m.1056 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1054
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : ¬cmp x y = Ordering.lt
h₂ : ¬cmp y z = Ordering.lt
this : ¬cmp y z = Ordering.lt → ¬cmp x y = Ordering.lt → ¬cmp x z = Ordering.lt
⊢ ¬cmp x z = Ordering.lt

Tactic:
exact this h₂ h₁

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toSignedMeasure_toMeasureOfZeroLE :
    μ.toSignedMeasure.toMeasureOfZeroLE Set.univ MeasurableSet.univ
      ((le_restrict_univ_iff_le _ _).2 (zero_le_toSignedMeasure μ)) = μ

Proof state:
case intro
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ ⟨↑μ.toSignedMeasure (univ ∩ i), ⋯⟩ = m

Tactic:
congr

Result:
case intro.e_val
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ ↑μ.toSignedMeasure (univ ∩ i) = ↑m

Proof state:
case intro.e_val
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ ↑μ.toSignedMeasure (univ ∩ i) = ↑m

Tactic:
simp [hi, ← hm]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯) i = μ i

Tactic:
lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm

Result:
case intro
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯) i = ↑m

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ = μ

Tactic:
refine Measure.ext fun i hi => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯) i = μ i

Proof state:
case intro
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯) i = ↑m

Tactic:
rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, ENNReal.coe_inj]

Result:
case intro
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : ↑m = μ i
⊢ ⟨↑μ.toSignedMeasure (univ ∩ i), ⋯⟩ = m
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem localization_toBasicOpen (f : R) :
    RingHom.comp (toBasicOpen R f) (algebraMap R (Localization.Away f)) =
    (toOpen R (PrimeSpectrum.basicOpen f)).hom :=
  RingHom.ext fun g => by
    rw [toBasicOpen, IsLocalization.Away.lift, RingHom.comp_apply, IsLocalization.lift_eq]

Proof state:
R : Type u
inst✝ : CommRing R
f g : R
⊢ ((toBasicOpen R f).comp (algebraMap R (Localization.Away f))) g =
    (CommRingCat.Hom.hom (toOpen R (PrimeSpectrum.basicOpen f))) g

Tactic:
rw [toBasicOpen, IsLocalization.Away.lift, RingHom.comp_apply, IsLocalization.lift_eq]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mkOfAlgebra {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S]
    [Algebra R S'] (M : Submonoid R) (f : S →ₐ[R] S') (h₁ : ∀ x ∈ M, IsUnit (algebraMap R S' x))
    (h₂ : ∀ y, ∃ x : S × M, x.2 • y = f x.1) (h₃ : ∀ x, f x = 0 → ∃ m : M, m • x = 0) :
    IsLocalizedModule M f.toLinearMap

Proof state:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ m • f x = (algebraMap R S') m * 0

Tactic:
simpa [Submonoid.smul_def] using f.congr_arg e

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem mul_val_inv (h : IsUnit a) : a * ↑h.unit⁻¹ = 1

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹

Tactic:
congr

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = 1

Tactic:
rw [← h.unit.mul_inv]

Result:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
⊢ a * ↑h.unit⁻¹ = ↑h.unit * ↑h.unit⁻¹
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem codisjoint_left : Codisjoint s t ↔ ∀ ⦃a⦄, a ∉ s → a ∈ t

Proof state:
α : Type u_1
s t : Finset α
inst✝ : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

Tactic:
classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
inst✝ : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

Tactic:
simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]

Result:
no goals