harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
    (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)

Tactic:
simp only [homEquiv_naturality_right, eq_self_iff_true, Equiv.apply_symm_apply]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g

Tactic:
rw [Equiv.symm_apply_eq]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_mul_ofReal (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) :
    log (x * r) = Real.log r + log x

Proof state:
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (x * ↑r) = ↑(Real.log r) + log x

Tactic:
rw [mul_comm, log_ofReal_mul hr hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem all_takeWhile {l : List α} : (l.takeWhile p).all p = true

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (takeWhile p l).all p = true

Tactic:
induction l with
| nil => rfl
| cons h t ih => by_cases p h <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
h : α
t : List α
ih : (takeWhile p t).all p = true
⊢ (takeWhile p (h :: t)).all p = true

Tactic:
by_cases p h <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ (takeWhile p []).all p = true

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Int/LeastGreatest.lean
theorem exists_least_of_bdd
    {P : ℤ → Prop}
    (Hbdd : ∃ b : ℤ , ∀ z : ℤ , P z → b ≤ z)
    (Hinh : ∃ z : ℤ , P z) : ∃ lb : ℤ , P lb ∧ ∀ z : ℤ , P z → lb ≤ z

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
let ⟨b , Hb⟩ := Hbdd

Result:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
exact ⟨lb , H⟩

Result:
no goals

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
classical
let ⟨b , Hb⟩ := Hbdd
let ⟨lb , H⟩ := leastOfBdd b Hb Hinh
exact ⟨lb , H⟩

Result:
no goals

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

Tactic:
let ⟨lb , H⟩ := leastOfBdd b Hb Hinh

Result:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
-- Mathlib/NumberTheory/KummerDedekind.lean
theorem Ideal.irreducible_map_of_irreducible_minpoly (hI : IsMaximal I) (hI' : I ≠ ⊥)
    (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x)
    (hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) :
    Irreducible (I.map (algebraMap R S))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : y = Ideal.map (algebraMap R S) I
⊢ y ∈ normalizedFactors (Ideal.map (algebraMap R S) I)

Tactic:
simp [hy]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem Intersecting.isUpperSet (hs : s.Intersecting)
    (h : ∀ t : Set α, t.Intersecting → s ⊆ t → s = t) : IsUpperSet s

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s

Tactic:
rw [h (Insert.insert b s) _ (subset_insert _ _)]

Result:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s

α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ (insert b s).Intersecting

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s

Tactic:
exact mem_insert _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
⊢ IsUpperSet s

Tactic:
rintro a b hab ha

Result:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ (insert b s).Intersecting

Tactic:
exact
  hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
@[to_additive] lemma threeGPFree_insert :
    ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧
      (∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → b * c = a * a → b = a

Proof state:
case intro.intro.inl.inr
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hd : d = b ∨ d ∈ s
hc : c ∈ s
⊢ b = c

case intro.intro.inr.inl
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d = c ∨ d ∈ s
⊢ b = c

case intro.intro.inr.inr
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
⊢ b = c

Tactic:
all_goals obtain rfl | hd := hd

Result:
case intro.intro.inl.inr.inl
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
c d : α
hc : c ∈ s
h : d * d = c * c
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ d = c

case intro.intro.inl.inr.inr
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
ha : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = b_1 * b_1 → b = b_1
ha' : ∀ ⦃b_1 : α⦄, b_1 ∈ s → ∀ ⦃c : α⦄, c ∈ s → b_1 * c = b * b → b_1 = b
hc : c ∈ s
hd : d ∈ s
⊢ b = c

case intro.intro.inr.inl.inl
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
b d : α
hb : b ∈ s
h : b * d = d * d
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = d

case intro.intro.inr.inl.inr
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d ∈ s
⊢ b = c

case intro.intro.inr.inr.inl
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → d * c = b * b → d = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = d * d → b = d
⊢ b = c

case intro.intro.inr.inr.inr
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c d : α
h : b * d = c * c
hb : b ∈ s
hc : c ∈ s
hd : d ∈ s
⊢ b = c
-- Mathlib/CategoryTheory/Subterminal.lean
theorem isSubterminal_of_isIso_diag [HasBinaryProduct A A] [IsIso (diag A)] : IsSubterminal A :=
  fun Z f g => by
  have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ prod.fst = prod.snd

Tactic:
simp [← cancel_epi (diag A)]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ f = g

Tactic:
rw [← prod.lift_fst f g, this, prod.lift_snd]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ f = g
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem pointReflection_involutive (x : P) : Involutive (pointReflection x : P → P) := fun y =>
  (Equiv.apply_eq_iff_eq_symm_apply _).2 <| by rw [pointReflection_symm]

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ (pointReflection x) y = (Equiv.symm (pointReflection x)) y

Tactic:
rw [pointReflection_symm]

Result:
no goals
-- Mathlib/Algebra/Ring/NonZeroDivisors.lean
/-- In a finite ring, an element is a unit iff it is a non-zero-divisor. -/
lemma isUnit_iff_mem_nonZeroDivisors_of_finite [Finite R] : IsUnit a ↔ a ∈ nonZeroDivisors R

Proof state:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
⊢ IsUnit a ↔ a ∈ R⁰

Tactic:
refine ⟨IsUnit.mem_nonZeroDivisors, fun ha ↦ ?_⟩

Result:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
⊢ IsUnit a

Proof state:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
⊢ IsUnit a

Tactic:
rw [IsUnit.isUnit_iff_mulRight_bijective, ← Finite.injective_iff_bijective]

Result:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
⊢ Function.Injective fun x => x * a

Proof state:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
b c : R
hbc : (fun x => x * a) b = (fun x => x * a) c
⊢ b = c

Tactic:
rw [← sub_eq_zero, ← sub_mul] at hbc

Result:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
b c : R
hbc : (b - c) * a = 0
⊢ b = c

Proof state:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
b c : R
hbc : (b - c) * a = 0
⊢ b = c

Tactic:
exact sub_eq_zero.mp (ha _ hbc)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
⊢ Function.Injective fun x => x * a

Tactic:
intro b c hbc

Result:
R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
ha : a ∈ R⁰
b c : R
hbc : (fun x => x * a) b = (fun x => x * a) c
⊢ b = c
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem lt_one (a : R) : a ≺ (1 : R) → a = 0 :=
  haveI := Classical.dec
  not_imp_not.1 fun h => by simpa only [one_mul] using mul_left_not_lt 1 h

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a : R
this : (p : Prop) → Decidable p
h : ¬a = 0
⊢ ¬a ≺ 1

Tactic:
simpa only [one_mul] using mul_left_not_lt 1 h

Result:
no goals
-- Mathlib/Algebra/QuadraticDiscriminant.lean
@[simp] lemma discrim_neg [Ring R] (a b c : R) : discrim (-a) (-b) (-c) = discrim a b c

Proof state:
R : Type u_1
inst✝ : Ring R
a b c : R
⊢ discrim (-a) (-b) (-c) = discrim a b c

Tactic:
simp [discrim]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Lattice.lean
theorem dual_solid (a b : α) (h : b ⊓ -b ≤ a ⊓ -a) : ‖a‖ ≤ ‖b‖

Proof state:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ b ⊔ -b

Tactic:
nth_rw 1 [← neg_neg b]

Result:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ ‖a‖ ≤ ‖b‖

Tactic:
apply solid

Result:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ |a| ≤ |b|

Proof state:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ - -a ⊔ -a ≤ |b|

Tactic:
rw [← neg_inf]

Result:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ |b|

Proof state:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ |b|

Tactic:
rw [abs]

Result:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ b ⊔ -b

Proof state:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b

Tactic:
rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ |a| ≤ |b|

Tactic:
rw [abs]

Result:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ a ⊔ -a ≤ |b|

Proof state:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ a ⊔ -a ≤ |b|

Tactic:
nth_rw 1 [← neg_neg a]

Result:
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ - -a ⊔ -a ≤ |b|
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_one (x : Nat) : x % 1 = 0

Proof state:
x : Nat
h : x % 1 < 1
this : ∀ (y : Nat), y < 1 → y = 0
⊢ x % 1 = 0

Tactic:
exact this _ h

Result:
no goals

Proof state:
x : Nat
h : x % 1 < 1
⊢ ∀ (y : Nat), y < 1 → y = 0

Tactic:
intro y

Result:
x : Nat
h : x % 1 < 1
y : Nat
⊢ y < 1 → y = 0

Proof state:
x : Nat
h : x % 1 < 1
y : Nat
⊢ y < 1 → y = 0

Tactic:
cases y with
| zero   => intro _; rfl
| succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)

Result:
no goals

Proof state:
case succ
x : Nat
h : x % 1 < 1
y : Nat
⊢ y + 1 < 1 → y + 1 = 0

Tactic:
intro h

Result:
case succ
x : Nat
h✝ : x % 1 < 1
y : Nat
h : y + 1 < 1
⊢ y + 1 = 0

Proof state:
case zero
x : Nat
h : x % 1 < 1
⊢ 0 < 1 → 0 = 0

Tactic:
intro _

Result:
case zero
x : Nat
h : x % 1 < 1
a✝ : 0 < 1
⊢ 0 = 0

Proof state:
x : Nat
⊢ 1 > 0

Tactic:
decide

Result:
no goals

Proof state:
x : Nat
h : x % 1 < 1
⊢ x % 1 = 0

Tactic:
have : (y : Nat) → y < 1 → y = 0 := by
  intro y
  cases y with
  | zero   => intro _; rfl
  | succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)

Result:
x : Nat
h : x % 1 < 1
this : ∀ (y : Nat), y < 1 → y = 0
⊢ x % 1 = 0

Proof state:
x : Nat
⊢ x % 1 = 0

Tactic:
have h : x % 1 < 1 := mod_lt x (by decide)

Result:
x : Nat
h : x % 1 < 1
⊢ x % 1 = 0

Proof state:
case succ
x : Nat
h✝ : x % 1 < 1
y : Nat
h : y + 1 < 1
⊢ y + 1 = 0

Tactic:
apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)

Result:
no goals

Proof state:
case zero
x : Nat
h : x % 1 < 1
a✝ : 0 < 1
⊢ 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type*} {mα : MeasurableSpace α}
    (μ : Measure α) {f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s)
    {t : ℝ≥0} (ht : 1 < t) :
    μ s =
      μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) +
      ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1)))

Proof state:
case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
hx : x ∈ s ∩ f ⁻¹' {⊤}
h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ⊤
⊢ False

Tactic:
have : f x < ∞ := h'x.2.2

Result:
case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
hx : x ∈ s ∩ f ⁻¹' {⊤}
h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ⊤
this : f x < ⊤
⊢ False
-- Mathlib/Topology/FiberBundle/Constructions.lean
theorem inducing_pullbackTotalSpaceEmbedding (f : B' → B) :
    IsInducing (@pullbackTotalSpaceEmbedding B F E B' f)

Proof state:
case eq_induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ =
    induced (Prod.fst ∘ pullbackTotalSpaceEmbedding f) inst✝¹ ⊓ induced (Prod.snd ∘ pullbackTotalSpaceEmbedding f) inst✝

Tactic:
rfl

Result:
no goals

Proof state:
case eq_induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding f) instTopologicalSpaceProd

Tactic:
simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose,
  Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]

Result:
case eq_induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ =
    induced (Prod.fst ∘ pullbackTotalSpaceEmbedding f) inst✝¹ ⊓ induced (Prod.snd ∘ pullbackTotalSpaceEmbedding f) inst✝

Proof state:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ IsInducing (pullbackTotalSpaceEmbedding f)

Tactic:
constructor

Result:
case eq_induced
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Pullback.TotalSpace.topologicalSpace F E f = induced (pullbackTotalSpaceEmbedding f) instTopologicalSpaceProd
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.symm {m n : ℕ+} : m.Coprime n → n.Coprime m

Proof state:
m n : ℕ+
⊢ m.Coprime n → n.Coprime m

Tactic:
unfold Coprime

Result:
m n : ℕ+
⊢ m.gcd n = 1 → n.gcd m = 1

Proof state:
m n : ℕ+
⊢ m.gcd n = 1 → n.gcd m = 1

Tactic:
rw [gcd_comm]

Result:
m n : ℕ+
⊢ n.gcd m = 1 → n.gcd m = 1

Proof state:
m n : ℕ+
⊢ n.gcd m = 1 → n.gcd m = 1

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basisDivisor_inj (hxy : basisDivisor x y = 0) : x = y

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x = y
⊢ x = y

Tactic:
exact hxy

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
hxy : basisDivisor x y = 0
⊢ x = y

Tactic:
simp_rw [basisDivisor, mul_eq_zero, X_sub_C_ne_zero, or_false, C_eq_zero, inv_eq_zero,
  sub_eq_zero] at hxy

Result:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x = y
⊢ x = y
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma map_add (f₁ f₂ : X ⟶ Y) :
    letI := addCommGroup L W (L.obj X) (L.obj Y)
    L.map (f₁ + f₂) = L.map f₁ + L.map f₂

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
⊢ L.map (f₁ + f₂) = L.map f₁ + L.map f₂

Tactic:
rw [add_eq W (Iso.refl _) (Iso.refl _) (L.map f₁) (L.map f₂)]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
⊢ L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
⊢ L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)

Tactic:
simp [add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_eq_nat {x : BitVec w} {y : Nat}
  : (x.toNat = y) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y))

Proof state:
case mpr
w : Nat
x : BitVec w
y : Nat
⊢ y < 2 ^ w ∧ x = BitVec.ofNat w y → x.toNat = y

Tactic:
intro eq

Result:
case mpr
w : Nat
x : BitVec w
y : Nat
eq : y < 2 ^ w ∧ x = BitVec.ofNat w y
⊢ x.toNat = y

Proof state:
case mpr
w : Nat
x : BitVec w
y : Nat
eq : y < 2 ^ w ∧ x = BitVec.ofNat w y
⊢ x.toNat = y

Tactic:
simp [Nat.mod_eq_of_lt, eq]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
y : Nat
⊢ x.toNat = y ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y

Tactic:
apply Iff.intro

Result:
case mp
w : Nat
x : BitVec w
y : Nat
⊢ x.toNat = y → y < 2 ^ w ∧ x = BitVec.ofNat w y

case mpr
w : Nat
x : BitVec w
y : Nat
⊢ y < 2 ^ w ∧ x = BitVec.ofNat w y → x.toNat = y

Proof state:
case mp
w : Nat
x : BitVec w
y : Nat
eq : x.toNat = y
⊢ y < 2 ^ w ∧ x = BitVec.ofNat w y

Tactic:
simp [←eq, x.isLt]

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
y : Nat
⊢ x.toNat = y → y < 2 ^ w ∧ x = BitVec.ofNat w y

Tactic:
intro eq

Result:
case mp
w : Nat
x : BitVec w
y : Nat
eq : x.toNat = y
⊢ y < 2 ^ w ∧ x = BitVec.ofNat w y
-- Mathlib/Order/RelSeries.lean
@[simp] lemma head_reverse (p : RelSeries r) : p.reverse.head = p.last

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
⊢ p.reverse.head = p.last

Tactic:
simp [RelSeries.last, RelSeries.head]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem ι_range_map_reverse :
    (ι Q).range.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
      = LinearMap.range (ι Q)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.map reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)

Tactic:
rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp,
  ← Submodule.map_comp]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ ↑(MulOpposite.opLinearEquiv R)) (LinearMap.range (ι Q)) =
    LinearMap.range (ι Q)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ ↑(MulOpposite.opLinearEquiv R)) (LinearMap.range (ι Q)) =
    LinearMap.range (ι Q)

Tactic:
exact Submodule.map_id _

Result:
no goals