harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/AddChar.lean
lemma sum_eq_ite (ψ : AddChar A R) [Decidable (ψ = 0)] :
    ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0

Proof state:
case neg.intro
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ∑ i : A, ψ x * ψ i = ∑ a : A, ψ a

Tactic:
exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm

Result:
no goals

Proof state:
case neg.intro
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ψ x * ∑ a : A, ψ a = ∑ a : A, ψ a

Tactic:
rw [Finset.mul_sum]

Result:
case neg.intro
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ∑ i : A, ψ x * ψ i = ∑ a : A, ψ a

Proof state:
case pos
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ψ = 0
⊢ ∑ a : A, ψ a = ↑(card A)

Tactic:
simp [h]

Result:
no goals

Proof state:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
⊢ ∑ a : A, ψ a = if ψ = 0 then ↑(card A) else 0

Tactic:
split_ifs with h

Result:
case pos
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ψ = 0
⊢ ∑ a : A, ψ a = ↑(card A)

case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
⊢ ∑ a : A, ψ a = 0

Proof state:
case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
⊢ ∑ a : A, ψ a = 0

Tactic:
obtain ⟨x, hx⟩ := ne_one_iff.1 h

Result:
case neg.intro
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ∑ a : A, ψ a = 0

Proof state:
case neg.intro
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ∑ a : A, ψ a = 0

Tactic:
refine eq_zero_of_mul_eq_self_left hx ?_

Result:
case neg.intro
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ψ x * ∑ a : A, ψ a = ∑ a : A, ψ a
-- Mathlib/Analysis/Complex/Periodic.lean
theorem qParam_right_inv (hh : h ≠ 0) {q : ℂ} (hq : q ≠ 0) : 𝕢 h (invQParam h q) = q

Proof state:
h : ℝ
hh : h ≠ 0
q : ℂ
hq : q ≠ 0
⊢ 𝕢 h (invQParam h q) = q

Tactic:
simp only [qParam, invQParam, ← mul_assoc, mul_div_cancel₀ _ two_pi_I_ne_zero,
  mul_div_cancel_left₀ _ (ofReal_ne_zero.mpr hh), exp_log hq]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem IsAlgebraic.of_mul [NoZeroDivisors R] {y z : S} (hy : y ∈ nonZeroDivisors S)
    (alg_y : IsAlgebraic R y) (alg_yz : IsAlgebraic R (y * z)) : IsAlgebraic R z

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ Algebra.adjoin R {y}
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z

Tactic:
exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ Algebra.adjoin R {y}
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (y * z * t)
⊢ IsAlgebraic R z

Tactic:
rw [mul_right_comm, eq, ← Algebra.smul_def] at this

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ Algebra.adjoin R {y}
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (r • z)
⊢ IsAlgebraic R z

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ Algebra.adjoin R {y}
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
⊢ IsAlgebraic R z

Tactic:
have := alg_yz.mul (Algebra.isAlgebraic_adjoin_singleton_iff.mpr alg_y _ ht)

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ Algebra.adjoin R {y}
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
this : IsAlgebraic R (y * z * t)
⊢ IsAlgebraic R z

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
⊢ IsAlgebraic R z

Tactic:
have ⟨t, ht, r, hr, eq⟩ := alg_y.exists_nonzero_eq_adjoin_mul hy

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
y z : S
hy : y ∈ nonZeroDivisors S
alg_y : IsAlgebraic R y
alg_yz : IsAlgebraic R (y * z)
t : S
ht : t ∈ Algebra.adjoin R {y}
r : R
hr : r ≠ 0
eq : y * t = (algebraMap R S) r
⊢ IsAlgebraic R z
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_le_iSup {f : Filter β} {u : β → α} : limsup u f ≤ ⨆ n, u n :=
  limsup_le_of_le (by isBoundedDefault) (Eventually.of_forall (le_iSup u))

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u

Tactic:
isBoundedDefault

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem ext : ∀ l₁ l₂ : LowerAdjoint u, (l₁ : α → β) = (l₂ : α → β) → l₁ = l₂
  | ⟨l₁, _⟩, ⟨l₂, _⟩, h => by
    congr

Proof state:
α : Type u_1
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
u : β → α
l₁ : α → β
gc'✝¹ : GaloisConnection l₁ u
l₂ : α → β
gc'✝ : GaloisConnection l₂ u
h : { toFun := l₁, gc' := gc'✝¹ }.toFun = { toFun := l₂, gc' := gc'✝ }.toFun
⊢ { toFun := l₁, gc' := gc'✝¹ } = { toFun := l₂, gc' := gc'✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma not_spanning_iff_closure_ssubset (hS : S ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ ¬M.Spanning S ↔ M.closure S ⊂ M.E

Tactic:
rw [spanning_iff_closure_eq, ssubset_iff_subset_ne, iff_and_self,
  iff_true_intro (M.closure_subset_ground _)]

Result:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ ¬M.closure S = M.E → True

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ ¬M.closure S = M.E → True

Tactic:
exact fun _ ↦ trivial

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_left_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y

Proof state:
⊢ ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem zero_dvd_iff : 0 ∣ a ↔ a = 0 :=
  ⟨eq_zero_of_zero_dvd, fun h => by
    rw [h]
    exact ⟨0, by simp⟩⟩

Proof state:
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 = 0 * 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a

Tactic:
rw [h]

Result:
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ 0

Proof state:
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ 0

Tactic:
exact ⟨0, by simp⟩

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma polyCharpolyAux_coeff_eval [Module.Finite R M] [Module.Free R M] (x : L) (i : ℕ) :
    MvPolynomial.eval (b.repr x) ((polyCharpolyAux φ b bₘ).coeff i) = (φ x).charpoly.coeff i

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Module.Free R M
x : L
i : ℕ
⊢ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (charpoly (φ x)).coeff i

Tactic:
nontriviality R

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Module.Free R M
x : L
i : ℕ
a✝ : Nontrivial R
⊢ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (charpoly (φ x)).coeff i

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Module.Free R M
x : L
i : ℕ
a✝ : Nontrivial R
⊢ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (charpoly (φ x)).coeff i

Tactic:
rw [← polyCharpolyAux_map_eq_charpoly φ b bₘ x, Polynomial.coeff_map]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
lemma awayMap_fromZeroRingHom (a) :
    awayMap 𝒜 hg hx (fromZeroRingHom 𝒜 _ a) = fromZeroRingHom 𝒜 _ a

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ (awayMap 𝒜 hg hx) ((fromZeroRingHom 𝒜 (Submonoid.powers f)) a) = (fromZeroRingHom 𝒜 (Submonoid.powers x)) a

Tactic:
ext

Result:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ val ((awayMap 𝒜 hg hx) ((fromZeroRingHom 𝒜 (Submonoid.powers f)) a)) =
    ((fromZeroRingHom 𝒜 (Submonoid.powers x)) a).val

Proof state:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ val ((awayMap 𝒜 hg hx) ((fromZeroRingHom 𝒜 (Submonoid.powers f)) a)) =
    ((fromZeroRingHom 𝒜 (Submonoid.powers x)) a).val

Tactic:
simp only [fromZeroRingHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
  val_awayMap, val_mk, SetLike.GradeZero.coe_one]

Result:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯) (Localization.mk ↑a ⟨1, ⋯⟩) =
    Localization.mk ↑a ⟨1, ⋯⟩

Proof state:
case a
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ (Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯) (Localization.mk ↑a ⟨1, ⋯⟩) =
    Localization.mk ↑a ⟨1, ⋯⟩

Tactic:
convert IsLocalization.lift_eq _ _

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Ioc_map_sectL : (Ioc a b).map (.sectL _ c) = Ioc (a, c) (b, c)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioc a b) = Ioc (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_sub : exp (x - y) = exp x / exp y

Proof state:
x y : ℂ
⊢ cexp (x - y) = cexp x / cexp y

Tactic:
simp [sub_eq_add_neg, exp_add, exp_neg, div_eq_mul_inv]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem one_div_zpow {A : M} (n : ℤ) : (1 / A) ^ n = 1 / A ^ n

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ (1 / A) ^ n = 1 / A ^ n

Tactic:
simp only [one_div, inv_zpow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem back!_filter [Inhabited α] (p : α → Bool) (l : Array α) :
    (l.filter p).back! = (l.findRev? p).get!

Proof state:
case mk
α : Type
inst✝ : Inhabited α
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ }).back! = (findRev? p { toList := toList✝ }).get!

Tactic:
simp [Option.get!_eq_getD]

Result:
no goals

Proof state:
α : Type
inst✝ : Inhabited α
p : α → Bool
l : Array α
⊢ (filter p l).back! = (findRev? p l).get!

Tactic:
cases l

Result:
case mk
α : Type
inst✝ : Inhabited α
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ }).back! = (findRev? p { toList := toList✝ }).get!
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_map_iff {f : α → β} :
    L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
L₁ L₂ : List β
l : List α
f : α → β
⊢ L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Tactic:
rw [eq_comm, map_eq_append_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Ioi {a : ℝ} : volume (Ioi a) = ∞ :=
  top_unique <|
    le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n =>
      calc
        (n : ℝ≥0∞) = volume (Ioo a (a + n))

Proof state:
a : ℝ
n : ℕ
⊢ ↑n = volume (Ioo a (a + ↑n))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem eq_nil_of_le {n m : ℕ} (h : m ≤ n) : Ico n m = []

Proof state:
n m : ℕ
h : m ≤ n
⊢ Ico n m = []

Tactic:
simp [Ico, Nat.sub_eq_zero_iff_le.mpr h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mk_beq_mk [BEq α] {a b : Array α} {h : a.size = n} {h' : b.size = n} :
    (Vector.mk a h == Vector.mk b h') = (a == b)

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a b : Array α
h : a.size = n
h' : b.size = n
⊢ ({ toArray := a, size_toArray := h } == { toArray := b, size_toArray := h' }) = (a == b)

Tactic:
simp [instBEq, isEqv, Array.instBEq, Array.isEqv, h, h']

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
lemma pairingIn_le_zero_of_ne :
    P.pairingIn ℤ i j ≤ 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
h : 0 < P.pairingIn ℤ i j
⊢ False

Tactic:
exact b.sub_nmem_range_root hi hj <| P.root_sub_root_mem_of_pairingIn_pos h hij

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
⊢ P.pairingIn ℤ i j ≤ 0

Tactic:
by_contra! h

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : NoZeroDivisors R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
b : P.Base
i j : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
h : 0 < P.pairingIn ℤ i j
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_ssubset_edgeFinset : G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂

Proof state:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.isZero_X₂ (hS : S.Exact) (hf : S.f = 0) (hg : S.g = 0) : IsZero S.X₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
this : Mono S.g
⊢ IsZero S.X₂

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_mono S.g, hg, comp_zero, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero S.X₂

Tactic:
have := hS.mono_g hf

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
this : Mono S.g
⊢ IsZero S.X₂
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem strictAntiOn_of_deriv_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, deriv f x < 0) : StrictAntiOn f D :=
  fun x hx y => by
  simpa only [zero_mul, sub_lt_zero] using
    hD.image_sub_lt_mul_sub_of_deriv_lt hf
      (fun z hz => (differentiableAt_of_deriv_ne_zero (hf' z hz).ne).differentiableWithinAt) hf' x
      hx y

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, deriv f x < 0
x : ℝ
hx : x ∈ D
y : ℝ
⊢ y ∈ D → x < y → f y < f x

Tactic:
simpa only [zero_mul, sub_lt_zero] using
  hD.image_sub_lt_mul_sub_of_deriv_lt hf
    (fun z hz => (differentiableAt_of_deriv_ne_zero (hf' z hz).ne).differentiableWithinAt) hf' x
    hx y

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.lintegral_kernel_prod_right'' {f : β × γ → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun x => ∫⁻ y, f (x, y) ∂η (a, x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable ((fun x => ∫⁻ (y : γ), (fun u => f (u.1.2, u.2)) (x, y) ∂η x) ∘ Prod.mk a)

Tactic:
refine (Measurable.lintegral_kernel_prod_right' (κ := η)
  (f := (fun u ↦ f (u.fst.snd, u.snd))) ?_).comp measurable_prod_mk_left

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun u => f (u.1.2, u.2)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun u => f (u.1.2, u.2)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun x => ∫⁻ (y : γ), f (x, y) ∂η (a, x)

Tactic:
change
  Measurable
    ((fun x => ∫⁻ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ Prod.mk a)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst✝ : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable ((fun x => ∫⁻ (y : γ), (fun u => f (u.1.2, u.2)) (x, y) ∂η x) ∘ Prod.mk a)
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_eq_zero_iff (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt a = 0 ↔ a = 0

Tactic:
rw [sqrt_eq_iff a _, mul_zero, eq_comm]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem mk_def_of_mem (p : K[X]) {q} (hq : q ∈ K[X]⁰) :
    RatFunc.mk p q = ofFractionRing (IsLocalization.mk' (FractionRing K[X]) p ⟨q, hq⟩)

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
hq : q ∈ K[X]⁰
⊢ RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, hq⟩ }

Tactic:
simp only [← mk_coe_def]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_apply_same (i : Fin (n + 1)) (x : α i) (p : ∀ j, α (i.succAbove j)) :
    insertNth i x p i = x

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth x p i = x

Tactic:
simp [insertNth, succAboveCases]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_id : map (fun i ↦ (LinearMap.id : s i →ₗ[R] s i)) = .id

Proof state:
case H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ ((map fun i => LinearMap.id).compMultilinearMap (tprod R)) x✝ = (LinearMap.id.compMultilinearMap (tprod R)) x✝

Tactic:
simp only [LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.id_coe, id_eq]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
⊢ (map fun i => LinearMap.id) = LinearMap.id

Tactic:
ext

Result:
case H.H
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
x✝ : (i : ι) → s i
⊢ ((map fun i => LinearMap.id).compMultilinearMap (tprod R)) x✝ = (LinearMap.id.compMultilinearMap (tprod R)) x✝
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousAt_iff_continuousAt {F : ι → X → α} {x₀ : X} :
    EquicontinuousAt F x₀ ↔ ContinuousAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ContinuousAt (⇑ofFun ∘ swap F) x₀

Tactic:
rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m

Proof state:
k n m : Nat
⊢ k + n - (k + m) = n - m

Tactic:
rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]

Result:
no goals