harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inl_snd_assoc {K : CochainComplex C ℤ} {d e f : ℤ} (γ : Cochain G K d)
    (he : 0 + d = e) (hf : -1 + e = f) :
    (inl φ).comp ((snd φ).comp γ he) hf = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e f : ℤ
γ : Cochain G K d
he : 0 + d = e
hf : -1 + e = f
⊢ (inl φ).comp ((snd φ).comp γ he) hf = 0

Tactic:
obtain rfl : e = d := by omega

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
⊢ (inl φ).comp ((snd φ).comp γ he) hf = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e f : ℤ
γ : Cochain G K d
he : 0 + d = e
hf : -1 + e = f
⊢ e = d

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
⊢ (inl φ).comp ((snd φ).comp γ he) hf = 0

Tactic:
rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_diagonal (i : m) : v ⬝ᵥ diagonal w i = v i * w i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i j : m
hij : j ≠ i
⊢ v j * diagonal w i j = 0

Tactic:
simp [diagonal_apply_ne' _ hij]

Result:
no goals

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ v ⬝ᵥ diagonal w i = v i * w i

Tactic:
have : ∀ j ≠ i, v j * diagonal w i j = 0 := fun j hij => by
  simp [diagonal_apply_ne' _ hij]

Result:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v ⬝ᵥ diagonal w i = v i * w i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v ⬝ᵥ diagonal w i = v i * w i

Tactic:
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem MonotoneOn.memLp_of_measure_ne_top (hmono : MonotoneOn f s) {a b : X}
    (ha : IsLeast s a) (hb : IsGreatest s b) (hs : μ s ≠ ∞) (h's : MeasurableSet s) :
    MemLp f p (μ.restrict s) :=
  (hmono.memLp_top ha hb h's).mono_exponent_of_measure_support_ne_top (s := univ)
    (by simp) (by simpa using hs) le_top

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : μ s ≠ ⊤
h's : MeasurableSet s
⊢ (μ.restrict s) univ ≠ ⊤

Tactic:
simpa using hs

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : μ s ≠ ⊤
h's : MeasurableSet s
⊢ ∀ x ∉ univ, f x = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α)

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : (Matrix n n α)ˣ
⊢ ↑A⁻¹ = (↑A)⁻¹

Tactic:
letI := A.invertible

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : (Matrix n n α)ˣ
this : Invertible ↑A := A.invertible
⊢ ↑A⁻¹ = (↑A)⁻¹

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : (Matrix n n α)ˣ
this : Invertible ↑A := A.invertible
⊢ ↑A⁻¹ = (↑A)⁻¹

Tactic:
rw [← invOf_eq_nonsing_inv, invOf_units]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem isClassified_of_normalize_isPrimitiveClassified (hc : h.normalize.IsPrimitiveClassified) :
    h.IsClassified

Proof state:
case h.e'_1
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ x

Tactic:
exact Int.gcd_dvd_left

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ h.IsClassified

Tactic:
convert h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc) <;>
  rw [Int.mul_ediv_cancel']

Result:
case h.e'_1
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ x

case h.e'_2
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ y

case h.e'_3
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ z

Proof state:
case h.e'_2
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ y

Tactic:
exact Int.gcd_dvd_right

Result:
no goals

Proof state:
case h.e'_3
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ z

Tactic:
exact h.gcd_dvd

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem smul_mem_smul (hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N :=
  (le_iSup _ ⟨m, hm⟩ : _ ≤ M • N) ⟨n, hn, by rfl⟩

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N : AddSubmonoid A
m : R
n : A
hm : m ∈ M
hn : n ∈ N
⊢ (DistribSMul.toAddMonoidHom A ↑⟨m, hm⟩) n = m • n

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem frobenius_zmod (p : ℕ) [Fact p.Prime] : frobenius (ZMod p) p = RingHom.id _

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ (frobenius (ZMod p) p) a = (RingHom.id (ZMod p)) a

Tactic:
rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ frobenius (ZMod p) p = RingHom.id (ZMod p)

Tactic:
ext a

Result:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ (frobenius (ZMod p) p) a = (RingHom.id (ZMod p)) a
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem exists_pow_lt_factorial (c : ℕ) : ∃ n0 > 1, ∀ n ≥ n0, c ^ n < (n - 1)! :=
  let ⟨n0, h⟩ := (eventually_pow_lt_factorial_sub c 1).exists_forall_of_atTop
  ⟨max n0 2, by omega, fun n hn ↦ h n (by omega)⟩

Proof state:
c n0 : ℕ
h : ∀ b ≥ n0, c ^ b < (b - 1)!
n : ℕ
hn : n ≥ n0 ⊔ 2
⊢ n ≥ n0

Tactic:
omega

Result:
no goals

Proof state:
c n0 : ℕ
h : ∀ b ≥ n0, c ^ b < (b - 1)!
⊢ n0 ⊔ 2 > 1

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem equiv_relation [IsPreconnected J] (r : J → J → Prop) (hr : _root_.Equivalence r)
    (h : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), r j₁ j₂) : ∀ j₁ j₂ : J, r j₁ j₂

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
j₁ j₂ : J
z : ∀ (j : J), r j₁ j
⊢ r j₁ j₂

Tactic:
exact z j₂

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
j₁ j₂ : J
⊢ r j₁ j₂

Tactic:
have z : ∀ j : J, r j₁ j :=
  induct_on_objects {k | r j₁ k} (hr.1 j₁)
    fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
j₁ j₂ : J
z : ∀ (j : J), r j₁ j
⊢ r j₁ j₂

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
⊢ ∀ (j₁ j₂ : J), r j₁ j₂

Tactic:
intros j₁ j₂

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂
j₁ j₂ : J
⊢ r j₁ j₂
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_zero [Zero α] : (diagonal fun _ => 0 : Matrix n n α) = 0

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
⊢ (diagonal fun x => 0) = 0

Tactic:
ext

Result:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
i✝ j✝ : n
⊢ diagonal (fun x => 0) i✝ j✝ = 0 i✝ j✝

Proof state:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
i✝ j✝ : n
⊢ diagonal (fun x => 0) i✝ j✝ = 0 i✝ j✝

Tactic:
simp [diagonal]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma prod_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
    (∏ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a

Proof state:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ (∏ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

Tactic:
rw [coe_prod, Finset.prod_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Submodule.bot_eq_top_of_rank_eq_zero [NoZeroSMulDivisors R M] (h : Module.rank R M = 0) :
    (⊥ : Submodule R M) = ⊤

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Module.rank R M = 0
⊢ ⊥ = ⊤

Tactic:
nontriviality R

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Module.rank R M = 0
a✝ : Nontrivial R
⊢ ⊥ = ⊤

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Subsingleton M
a✝ : Nontrivial R
⊢ ⊥ = ⊤

Tactic:
subsingleton

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Module.rank R M = 0
a✝ : Nontrivial R
⊢ ⊥ = ⊤

Tactic:
rw [rank_zero_iff] at h

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Subsingleton M
a✝ : Nontrivial R
⊢ ⊥ = ⊤
-- Mathlib/Computability/Tape.lean
theorem ListBlank.cons_flatMap {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (a : Γ) (l : ListBlank Γ)
    (f : Γ → List Γ') (hf) : (l.cons a).flatMap f hf = (l.flatMap f hf).append (f a)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ (cons a (mk l)).flatMap f hf = append (f a) ((mk l).flatMap f hf)

Tactic:
simp only [ListBlank.append_mk, ListBlank.flatMap_mk, ListBlank.cons_mk, List.flatMap_cons]

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ (cons a ⟦l⟧).flatMap f hf = append (f a) (flatMap ⟦l⟧ f hf)

Tactic:
suffices ((mk l).cons a).flatMap f hf = ((mk l).flatMap f hf).append (f a) by exact this

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ (cons a (mk l)).flatMap f hf = append (f a) ((mk l).flatMap f hf)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
⊢ (cons a l).flatMap f hf = append (f a) (l.flatMap f hf)

Tactic:
refine l.inductionOn fun l ↦ ?_

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
⊢ (cons a ⟦l⟧).flatMap f hf = append (f a) (flatMap ⟦l⟧ f hf)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
a : Γ
l✝ : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
l : List Γ
this : (cons a (mk l)).flatMap f hf = append (f a) ((mk l).flatMap f hf)
⊢ (cons a ⟦l⟧).flatMap f hf = append (f a) (flatMap ⟦l⟧ f hf)

Tactic:
exact this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.norm.denote ctx = m.denote ctx

Proof state:
ctx : Context
m : Poly
⊢ denote ctx m.norm = denote ctx m

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_zero (l : List α) : l.rotate' 0 = l

Proof state:
α : Type u
l : List α
⊢ l.rotate' 0 = l

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma prod_prod_Ioi_mul_eq_prod_prod_off_diag (f : α → α → M) :
    ∏ i, ∏ j ∈ Ioi i, f j i * f i j = ∏ i, ∏ j ∈ {i}ᶜ, f j i

Proof state:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : Fintype α
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : CommMonoid M
f : α → α → M
⊢ ∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1 = ∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x

Tactic:
rw [prod_sigma', prod_sigma']

Result:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : Fintype α
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : CommMonoid M
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst

Proof state:
α : Type u_1
M : Type u_2
inst✝⁴ : Fintype α
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : CommMonoid M
f : α → α → M
⊢ (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) * ∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1 =
    (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) * ∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x

Tactic:
congr 1

Result:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : Fintype α
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : CommMonoid M
f : α → α → M
⊢ ∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1 = ∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x

Proof state:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : Fintype α
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : CommMonoid M
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst

Tactic:
refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_ <;> simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝⁴ : Fintype α
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : CommMonoid M
f : α → α → M
⊢ ∏ i : α, ∏ j ∈ Ioi i, f j i * f i j = ∏ i : α, ∏ j ∈ {i}ᶜ, f j i

Tactic:
simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]

Result:
α : Type u_1
M : Type u_2
inst✝⁴ : Fintype α
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : CommMonoid M
f : α → α → M
⊢ (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) * ∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1 =
    (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) * ∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem smod_zero {x : BitVec n} : x.smod 0#n = x

Proof state:
case false.a
n : Nat
x : BitVec n
⊢ (match false, false with
      | false, false => x.umod 0#n
      | false, true => if x.umod (-0#n) = 0#n then x.umod (-0#n) else x.umod (-0#n) + 0#n
      | true, false => if (-x).umod 0#n = 0#n then (-x).umod 0#n else 0#n - (-x).umod 0#n
      | true, true => -(-x).umod (-0#n)).toNat =
    x.toNat

Tactic:
simp

Result:
no goals

Proof state:
case true.a
n : Nat
x : BitVec n
⊢ (match true, false with
      | false, false => x.umod 0#n
      | false, true => if x.umod (-0#n) = 0#n then x.umod (-0#n) else x.umod (-0#n) + 0#n
      | true, false => if (-x).umod 0#n = 0#n then (-x).umod 0#n else 0#n - (-x).umod 0#n
      | true, true => -(-x).umod (-0#n)).toNat =
    x.toNat

Tactic:
by_cases h : x = 0#n <;> simp [h]

Result:
no goals

Proof state:
n : Nat
x : BitVec n
⊢ x.smod 0#n = x

Tactic:
simp only [smod_eq, msb_zero]

Result:
n : Nat
x : BitVec n
⊢ (match x.msb, false with
    | false, false => x.umod 0#n
    | false, true => if x.umod (-0#n) = 0#n then x.umod (-0#n) else x.umod (-0#n) + 0#n
    | true, false => if (-x).umod 0#n = 0#n then (-x).umod 0#n else 0#n - (-x).umod 0#n
    | true, true => -(-x).umod (-0#n)) =
    x

Proof state:
n : Nat
x : BitVec n
⊢ (match x.msb, false with
    | false, false => x.umod 0#n
    | false, true => if x.umod (-0#n) = 0#n then x.umod (-0#n) else x.umod (-0#n) + 0#n
    | true, false => if (-x).umod 0#n = 0#n then (-x).umod 0#n else 0#n - (-x).umod 0#n
    | true, true => -(-x).umod (-0#n)) =
    x

Tactic:
rcases x.msb with msb | msb <;> apply eq_of_toNat_eq

Result:
case false.a
n : Nat
x : BitVec n
⊢ (match false, false with
      | false, false => x.umod 0#n
      | false, true => if x.umod (-0#n) = 0#n then x.umod (-0#n) else x.umod (-0#n) + 0#n
      | true, false => if (-x).umod 0#n = 0#n then (-x).umod 0#n else 0#n - (-x).umod 0#n
      | true, true => -(-x).umod (-0#n)).toNat =
    x.toNat

case true.a
n : Nat
x : BitVec n
⊢ (match true, false with
      | false, false => x.umod 0#n
      | false, true => if x.umod (-0#n) = 0#n then x.umod (-0#n) else x.umod (-0#n) + 0#n
      | true, false => if (-x).umod 0#n = 0#n then (-x).umod 0#n else 0#n - (-x).umod 0#n
      | true, true => -(-x).umod (-0#n)).toNat =
    x.toNat
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem QInfty_comp_PInfty : (QInfty : K[X] ⟶ _) ≫ PInfty = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty ≫ PInfty = 0

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (QInfty ≫ PInfty).f n = HomologicalComplex.Hom.f 0 n

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (QInfty ≫ PInfty).f n = HomologicalComplex.Hom.f 0 n

Tactic:
apply QInfty_f_comp_PInfty_f

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
theorem sdiff_insert_of_not_mem {x : α} (h : x ∉ s) (t : Finset α) : s \ insert x t = s \ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
⊢ s \ insert x t = s \ t

Tactic:
refine Subset.antisymm (sdiff_subset_sdiff (Subset.refl _) (subset_insert _ _)) fun y hy => ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
y : α
hy : y ∈ s \ t
⊢ y ∈ s \ insert x t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
y : α
hy : y ∈ s ∧ y ∉ t
⊢ y ∈ s ∧ ¬y = x ∧ y ∉ t

Tactic:
exact ⟨hy.1, fun hxy => h <| hxy ▸ hy.1, hy.2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
y : α
hy : y ∈ s \ t
⊢ y ∈ s \ insert x t

Tactic:
simp only [mem_sdiff, mem_insert, not_or] at hy ⊢

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∉ s
t : Finset α
y : α
hy : y ∈ s ∧ y ∉ t
⊢ y ∈ s ∧ ¬y = x ∧ y ∉ t
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem dist_vsub_cancel_left (x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y z

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y z : P
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z

Tactic:
rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]

Result:
no goals
-- Mathlib/Probability/Distributions/Gamma.lean
/-- The Lebesgue integral of the gamma pdf over nonpositive reals equals 0 -/
lemma lintegral_gammaPDF_of_nonpos {x a r : ℝ} (hx : x ≤ 0) :
    ∫⁻ y in Iio x, gammaPDF a r y = 0

Proof state:
x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (y : ℝ) in Iio x, gammaPDF a r y = 0

Tactic:
rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]

Result:
x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

x a r : ℝ
hx : x ≤ 0
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → gammaPDF a r x_1 = 0

Proof state:
x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

Tactic:
rw [lintegral_zero, ← ENNReal.ofReal_zero]

Result:
no goals

Proof state:
x a✝ r : ℝ
hx : x ≤ 0
a : ℝ
x✝ : a < x
⊢ ¬0 ≤ a

Tactic:
linarith

Result:
no goals

Proof state:
case h
x a✝ r : ℝ
hx : x ≤ 0
a : ℝ
x✝ : a < x
⊢ (if 0 ≤ a then r ^ a✝ / Gamma a✝ * a ^ (a✝ - 1) * rexp (-(r * a)) else 0) ≤ 0

Tactic:
rw [if_neg (by linarith)]

Result:
no goals

Proof state:
x a r : ℝ
hx : x ≤ 0
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → gammaPDF a r x_1 = 0

Tactic:
simp only [gammaPDF_eq, ENNReal.ofReal_eq_zero]

Result:
x a r : ℝ
hx : x ≤ 0
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → (if 0 ≤ x_1 then r ^ a / Gamma a * x_1 ^ (a - 1) * rexp (-(r * x_1)) else 0) ≤ 0

Proof state:
x a r : ℝ
hx : x ≤ 0
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → (if 0 ≤ x_1 then r ^ a / Gamma a * x_1 ^ (a - 1) * rexp (-(r * x_1)) else 0) ≤ 0

Tactic:
filter_upwards with a (_ : a < _)

Result:
case h
x a✝ r : ℝ
hx : x ≤ 0
a : ℝ
x✝ : a < x
⊢ (if 0 ≤ a then r ^ a✝ / Gamma a✝ * a ^ (a✝ - 1) * rexp (-(r * a)) else 0) ≤ 0
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem Convex.image_sub_le_mul_sub_of_deriv_le {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C}
    (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D)
    (hxy : x ≤ y) : f y - f x ≤ C * (y - x) :=
  have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun y => -f y) x := fun x hx => by
    rw [deriv.neg, neg_le_neg_iff]
    exact le_hf' x hx
  by linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ ≤ y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x ≤ C

Tactic:
exact le_hf' x hx

Result:
no goals

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ ≤ y
x : ℝ
hx : x ∈ interior D
⊢ -C ≤ deriv (fun y => -f y) x

Tactic:
rw [deriv.neg, neg_le_neg_iff]

Result:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ ≤ y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x ≤ C

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun y => -f y) x
⊢ f y - f x ≤ C * (y - x)

Tactic:
linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
/-- Dividing `n` by `p^i` is like truncating the first `i` digits of `n` in base `p`.
-/
lemma self_div_pow_eq_ofDigits_drop {p : ℕ} (i n : ℕ) (h : 2 ≤ p) :
    n / p ^ i = ofDigits p ((p.digits n).drop i)

Proof state:
case h.e'_2.h.e'_5
p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

Result:
no goals

Proof state:
p i n : ℕ
h : 2 ≤ p
⊢ n / p ^ i = ofDigits p (List.drop i (p.digits n))

Tactic:
convert ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n)
  (fun l hl ↦ digits_lt_base h hl)

Result:
case h.e'_2.h.e'_5
p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (p.digits n)