harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem _root_.LinearMap.compQuadraticMap_polarBilin (f : N →ₗ[R] N') (Q : QuadraticMap R M N) :
    (f.compQuadraticMap' Q).polarBilin = Q.polarBilin.compr₂ f

Proof state:
case h.h
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((f.compQuadraticMap' Q).polarBilin x✝¹) x✝ = ((compr₂ Q.polarBilin f) x✝¹) x✝

Tactic:
rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply,
  LinearMap.compQuadraticMap_polar]

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
⊢ (f.compQuadraticMap' Q).polarBilin = compr₂ Q.polarBilin f

Tactic:
ext

Result:
case h.h
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((f.compQuadraticMap' Q).polarBilin x✝¹) x✝ = ((compr₂ Q.polarBilin f) x✝¹) x✝
-- Mathlib/NumberTheory/Divisors.lean
theorem cons_self_properDivisors (h : n ≠ 0) :
    cons n (properDivisors n) properDivisors.not_self_mem = divisors n

Proof state:
n : ℕ
h : n ≠ 0
⊢ cons n n.properDivisors ⋯ = n.divisors

Tactic:
rw [cons_eq_insert, insert_self_properDivisors h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A B)]
    [IsIso (prodComparison F A' B')] :
    inv (prodComparison F A B) ≫ F.map (prod.map f g) =
      prod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B')

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryProduct A B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝² : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (prodComparison F A B)
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B')

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma mul_nonpos_iff [MulPosStrictMono α] [PosMulStrictMono α]
    [AddLeftReflectLE α] [AddLeftMono α] :
    a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : MulPosStrictMono α
inst✝² : PosMulStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (α := α), neg_nonneg, neg_nonpos]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma sqrt_eq_one : sqrt x = 1 ↔ x = 1

Proof state:
x : ℝ≥0
⊢ sqrt x = 1 ↔ x = 1

Tactic:
simp [sqrt_eq_iff_eq_sq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.false_and (b : Bool) : (false && b) = false

Proof state:
b : Bool
⊢ (false && b) = false

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem land_bit (a m b n) : land (bit a m) (bit b n) = bit (a && b) (land m n)

Proof state:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).land (bit b n) = bit (a && b) (m.land n)

Tactic:
rw [← bitwise_and, bitwise_bit]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_inv (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    (cycleOf f x)⁻¹ = cycleOf f⁻¹ x :=
  Equiv.ext fun y => by
    rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
    split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (f.cycleOf x)⁻¹ y = (f⁻¹.cycleOf x) y

Tactic:
rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]

Result:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then f⁻¹ y else y) then f (if f⁻¹.SameCycle x y then f⁻¹ y else y)
    else if f⁻¹.SameCycle x y then f⁻¹ y else y

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ y =
    if f.SameCycle x (if f⁻¹.SameCycle x y then f⁻¹ y else y) then f (if f⁻¹.SameCycle x y then f⁻¹ y else y)
    else if f⁻¹.SameCycle x y then f⁻¹ y else y

Tactic:
split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_mul_le {p q : MvPolynomial σ R} : (p * q).degrees ≤ p.degrees + q.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ (p * q).degrees ≤ p.degrees + q.degrees

Tactic:
classical
simp_rw [degrees_def]
exact supDegree_mul_le (map_add _)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ ((p * q).support.sup fun s => toMultiset s) ≤
    (p.support.sup fun s => toMultiset s) + q.support.sup fun s => toMultiset s

Tactic:
exact supDegree_mul_le (map_add _)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ (p * q).degrees ≤ p.degrees + q.degrees

Tactic:
simp_rw [degrees_def]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ ((p * q).support.sup fun s => toMultiset s) ≤
    (p.support.sup fun s => toMultiset s) + q.support.sup fun s => toMultiset s
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma zeta_mul_kappa [Semiring 𝕜] [Preorder α] [LocallyFiniteOrder α]
    [DecidableRel (α := α) (· ≤ ·)] (a b : α) :
    (zeta 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) a b = (Icc a b).card

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1

Tactic:
refine sum_congr rfl fun x hx ↦ ?_

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Tactic:
rw [mem_Icc] at hx

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(#(Icc a b))

Tactic:
rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]

Result:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Tactic:
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem le_inv_iff_mul_le {r p : ℝ≥0} (h : p ≠ 0) : r ≤ p⁻¹ ↔ r * p ≤ 1

Proof state:
r p : ℝ≥0
h : p ≠ 0
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1

Tactic:
rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem Integrable.ae_eq_of_withDensityᵥ_eq [CompleteSpace E] {f g : α → E} (hf : Integrable f μ)
    (hg : Integrable g μ) (hfg : μ.withDensityᵥ f = μ.withDensityᵥ g) : f =ᵐ[μ] g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : μ.withDensityᵥ f = μ.withDensityᵥ g
i : Set α
hi : MeasurableSet i
x✝ : μ i < ⊤
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ

Tactic:
rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : μ.withDensityᵥ f = μ.withDensityᵥ g
⊢ f =ᶠ[ae μ] g

Tactic:
refine hf.ae_eq_of_forall_setIntegral_eq f g hg fun i hi _ => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : μ.withDensityᵥ f = μ.withDensityᵥ g
i : Set α
hi : MeasurableSet i
x✝ : μ i < ⊤
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
theorem monomorphisms.iff : (monomorphisms C) f ↔ Mono f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ monomorphisms C f ↔ Mono f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem chain_map {β : Type*} {r : α → α → Prop} (f : β → α) {s : Cycle β} :
    Chain r (s.map f) ↔ Chain (fun a b => r (f a) (f b)) s :=
  Quotient.inductionOn s fun l => by
    rcases l with - | ⟨a, l⟩
    · rfl
    · simp [← concat_eq_append, ← List.map_concat, List.chain_map f]

Proof state:
case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun a b => r (f a) (f b)) ⟦[]⟧

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
⊢ Chain r (map f ⟦l⟧) ↔ Chain (fun a b => r (f a) (f b)) ⟦l⟧

Tactic:
rcases l with - | ⟨a, l⟩

Result:
case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun a b => r (f a) (f b)) ⟦[]⟧

case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b => r (f a) (f b)) ⟦a :: l⟧

Proof state:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b => r (f a) (f b)) ⟦a :: l⟧

Tactic:
simp [← concat_eq_append, ← List.map_concat, List.chain_map f]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_zero : intDegree (0 : RatFunc K) = 0

Proof state:
K : Type u
inst✝ : Field K
⊢ intDegree 0 = 0

Tactic:
rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem prime_def_le_sqrt {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬m ∣ p :=
  prime_def_lt'.trans <|
    and_congr_right fun p2 =>
      ⟨fun a m m2 l => a m m2 <| lt_of_le_of_lt l <| sqrt_lt_self p2, fun a =>
        have : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k := fun {m k} mk m1 e =>
          a m m1 (le_sqrt.2 (e.symm ▸ Nat.mul_le_mul_left m mk)) ⟨k, e⟩
        fun m m2 l ⟨k, e⟩ => by
        rcases le_total m k with mk | km
        · exact this mk m2 e
        · rw [mul_comm] at e
          refine this km (Nat.lt_of_mul_lt_mul_right (a := m) ?_) e
          rwa [one_mul, ← e]⟩

Proof state:
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
km : k ≤ m
⊢ False

Tactic:
rw [mul_comm] at e

Result:
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ False

Proof state:
case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
mk : m ≤ k
⊢ False

Tactic:
exact this mk m2 e

Result:
no goals

Proof state:
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ False

Tactic:
refine this km (Nat.lt_of_mul_lt_mul_right (a := m) ?_) e

Result:
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ 1 * m < k * m

Proof state:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
⊢ False

Tactic:
rcases le_total m k with mk | km

Result:
case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
mk : m ≤ k
⊢ False

case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
km : k ≤ m
⊢ False

Proof state:
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ 1 * m < k * m

Tactic:
rwa [one_mul, ← e]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/NatCast.lean
lemma zero_le_three [Preorder α] [ZeroLEOneClass α] [AddLeftMono α] :
    (0 : α) ≤ 3

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2 + 1

Tactic:
exact add_nonneg zero_le_two zero_le_one

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 3

Tactic:
rw [← two_add_one_eq_three]

Result:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2 + 1
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_sub_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a - n * c ≡ b [ZMOD n]

Proof state:
case h.e'_2
a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ a - n * c = a + n * -c

Tactic:
rw [Int.mul_neg, sub_eq_add_neg]

Result:
no goals

Proof state:
a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ a - n * c ≡ b [ZMOD n]

Tactic:
convert Int.modEq_add_fac (-c) ha using 1

Result:
case h.e'_2
a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ a - n * c = a + n * -c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem log2_lt (h : n ≠ 0) : n.log2 < k ↔ n < 2 ^ k

Proof state:
n k : Nat
h : n ≠ 0
⊢ n.log2 < k ↔ n < 2 ^ k

Tactic:
rw [← Nat.not_le, ← Nat.not_le, le_log2 h]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem exists_pos_sum_of_countable {ε : ℝ≥0} (hε : ε ≠ 0) (ι) [Countable ι] :
    ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Proof state:
case intro.intro.intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι

Result:
case intro.intro.intro.mk.intro.intro.intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ (fun a => ↑a) a
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Proof state:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
cases nonempty_encodable ι

Result:
case intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Proof state:
case intro.intro.intro.mk.intro.intro.intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ (fun a => ↑a) a
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
exact
  ⟨fun i ↦ ⟨ε' i, (hε' i).le⟩, fun i ↦ NNReal.coe_lt_coe.1 <| hε' i,
    ⟨c, hasSum_le (fun i ↦ (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
    aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩

Result:
no goals

Proof state:
case intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Tactic:
obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)

Result:
case intro.intro.intro
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem eq_zero_iff {I : FractionalIdeal S P} : I = 0 ↔ ∀ x ∈ I, x = (0 : P) :=
  ⟨fun h x hx => by simpa [h, mem_zero_iff] using hx, fun h =>
    le_bot_iff.mp fun x hx => (mem_zero_iff S).mpr (h x hx)⟩

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
h : I = 0
x : P
hx : x ∈ I
⊢ x = 0

Tactic:
simpa [h, mem_zero_iff] using hx

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem IsMultiplicative.ppow [CommSemiring R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative)
    {k : ℕ} : IsMultiplicative (f.ppow k)

Proof state:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hi : (f.ppow k).IsMultiplicative
⊢ (f.pmul (f.ppow k)).IsMultiplicative

Tactic:
apply hf.pmul hi

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hi : (f.ppow k).IsMultiplicative
⊢ (f.ppow (k + 1)).IsMultiplicative

Tactic:
rw [ppow_succ']

Result:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hi : (f.ppow k).IsMultiplicative
⊢ (f.pmul (f.ppow k)).IsMultiplicative

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
⊢ (f.ppow k).IsMultiplicative

Tactic:
induction k with
| zero => exact isMultiplicative_zeta.natCast
| succ k hi => rw [ppow_succ']; apply hf.pmul hi

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
⊢ (f.ppow 0).IsMultiplicative

Tactic:
exact isMultiplicative_zeta.natCast

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem xor_not_left : Xor' (¬a) b ↔ (a ↔ b)

Proof state:
a b : Prop
⊢ Xor' (¬a) b ↔ (a ↔ b)

Tactic:
by_cases a <;> simp [*]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk_left_injective (b : s) : Injective fun a => mk a b := fun c d h => by
  simpa [mk_eq_mk_iff, r_iff_exists] using h

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
s : Submonoid α
b : ↥s
c d : α
h : (fun a => mk a b) c = (fun a => mk a b) d
⊢ c = d

Tactic:
simpa [mk_eq_mk_iff, r_iff_exists] using h

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_mul (h : IsUnit A.det) : A⁻¹ * A = 1

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹ * A = 1

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible

Result:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ * A = 1

Proof state:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ * A = 1

Tactic:
rw [← invOf_eq_nonsing_inv, invOf_mul_self]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma φ_neg (n : ℤ) : W.φ (-n) = W.φ n

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ W.φ (-n) = W.φ n

Tactic:
rw [φ, ψ_neg, neg_sq (R := R[X][Y]), neg_add_eq_sub, ← neg_sub n, ψ_neg, ← neg_add', ψ_neg,
  neg_mul_neg (α := R[X][Y]), mul_comm <| W.ψ _, φ]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem sup_eq_range (s t : Submonoid N) : s ⊔ t = mrange (s.subtype.coprod t.subtype)

Proof state:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)

Tactic:
rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
  coprod_comp_inr, mrange_subtype, mrange_subtype]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma graphOn_prod_prodMap (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
    (s ×ˢ t).graphOn (Prod.map f g) = Equiv.prodProdProdComm .. ⁻¹' s.graphOn f ×ˢ t.graphOn g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → γ
g : β → δ
⊢ graphOn (Prod.map f g) (s ×ˢ t) = ⇑(prodProdProdComm α β γ δ) ⁻¹' graphOn f s ×ˢ graphOn g t

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
/-- Finite product of finite sets is finite. Note this is a variant of `Set.Finite.pi` without the
extra `i ∈ univ` binder. -/
lemma Finite.pi' (ht : ∀ i, (t i).Finite) : {f : ∀ i, κ i | ∀ i, f i ∈ t i}.Finite

Proof state:
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ {f | ∀ (i : ι), f i ∈ t i}.Finite

Tactic:
simpa [Set.pi] using Finite.pi ht

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂Hom_monomial (f : R →+* S₁) (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :
    eval₂Hom f g (monomial d r) = f r * d.prod fun i k => g i ^ k

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
d : σ →₀ ℕ
r : R
⊢ (eval₂Hom f g) ((monomial d) r) = f r * d.prod fun i k => g i ^ k

Tactic:
simp only [monomial_eq, RingHom.map_mul, eval₂Hom_C, Finsupp.prod, map_prod,
  RingHom.map_pow, eval₂Hom_X']

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSub_eq_linear_combination {ι} (s : Finset ι) {w : ι → k} {p : ι → V}
    (hw : s.sum w = 0) : s.weightedVSub p w = ∑ i ∈ s, w i • p i

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_6
s : Finset ι
w : ι → k
p : ι → V
hw : s.sum w = 0
⊢ (s.weightedVSub p) w = ∑ i ∈ s, w i • p i

Tactic:
simp [s.weightedVSub_apply, vsub_eq_sub, smul_sub, ← Finset.sum_smul, hw]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_sub_self (a b : α) : toIcoMod hp a b - b = -toIcoDiv hp a b • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b - b = -toIcoDiv hp a b • p

Tactic:
rw [toIcoMod, sub_sub_cancel_left, neg_smul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_dblY (P : Fin 3 → R) : (W'.map f).toJacobian.dblY (f ∘ P) = f (W'.dblY P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.dblY (⇑f ∘ P) = f (W'.dblY P)

Tactic:
simp only [dblY, negY_eq, map_negDblY, map_dblX, map_dblZ]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.negDblY P) - (map W' f).toJacobian.a₁ * f (W'.dblX P) * f (W'.dblZ P) -
      (map W' f).toJacobian.a₃ * f (W'.dblZ P) ^ 3 =
    f (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.negDblY P) - (map W' f).toJacobian.a₁ * f (W'.dblX P) * f (W'.dblZ P) -
      (map W' f).toJacobian.a₃ * f (W'.dblZ P) ^ 3 =
    f (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)

Tactic:
map_simp

Result:
no goals