harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma mu_eq_neg_sum_Ioc_of_ne (hab : a ≠ b) : mu 𝕜 a b = -∑ x ∈ Ioc a b, mu 𝕜 x b

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ (mu 𝕜) a b = -∑ x ∈ Ioc a b, (mu 𝕜) x b

Tactic:
rw [mu_eq_mu', mu'_eq_sum_Ioc_of_ne hab]

Result:
no goals
-- Mathlib/RingTheory/Etale/Kaehler.lean
lemma KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap
    [Algebra.FormallyEtale S T] (s : S) :
    (tensorKaehlerEquivOfFormallyEtale R S T).symm (D R T (algebraMap S T s)) = 1 ⊗ₜ D R S s

Proof state:
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
s : S
⊢ (tensorKaehlerEquivOfFormallyEtale R S T).symm ((D R T) ((algebraMap S T) s)) = 1 ⊗ₜ[S] (D R S) s

Tactic:
rw [LinearEquiv.symm_apply_eq, tensorKaehlerEquivOfFormallyEtale_apply, mapBaseChange_tmul,
  one_smul, map_D]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_closedBall (x : E) {r : ℝ} (hr : 0 ≤ r) :
    μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 ≤ r
⊢ μ (closedBall x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Tactic:
rw [addHaar_closedBall' μ x hr, addHaar_unitClosedBall_eq_addHaar_unitBall]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_X_pow_assoc (m n : ℕ) :
    x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
m n : ℕ
⊢ x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp only [smeval_add, ph, qh, mul_add]
| h_monomial n a =>
  simp only [smeval_monomial, mul_smul_comm, npow_mul_assoc]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
m n✝ n : ℕ
a : R
⊢ x ^ m * x ^ n✝ * ((monomial n) a).smeval x = x ^ m * (x ^ n✝ * ((monomial n) a).smeval x)

Tactic:
simp only [smeval_monomial, mul_smul_comm, npow_mul_assoc]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁵ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
m n : ℕ
p q : R[X]
ph : x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
qh : x ^ m * x ^ n * q.smeval x = x ^ m * (x ^ n * q.smeval x)
⊢ x ^ m * x ^ n * (p + q).smeval x = x ^ m * (x ^ n * (p + q).smeval x)

Tactic:
simp only [smeval_add, ph, qh, mul_add]

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_eq_zero {x : Game} : birthday x = 0 ↔ x = 0

Proof state:
case mp
x : Game
h : x.birthday = 0
⊢ x = 0

Tactic:
let ⟨y, hy₁, hy₂⟩ := birthday_eq_pGameBirthday x

Result:
case mp
x : Game
h : x.birthday = 0
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ x = 0

Proof state:
case mp
x : Game
h : x.birthday = 0
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ ⟦y⟧ = 0

Tactic:
rw [h, PGame.birthday_eq_zero] at hy₂

Result:
case mp
x : Game
h : x.birthday = 0
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : IsEmpty y.LeftMoves ∧ IsEmpty y.RightMoves
⊢ ⟦y⟧ = 0

Proof state:
case mpr

⊢ birthday 0 = 0

Tactic:
exact birthday_zero

Result:
no goals

Proof state:
case mp
x : Game
⊢ x.birthday = 0 → x = 0

Tactic:
intro h

Result:
case mp
x : Game
h : x.birthday = 0
⊢ x = 0

Proof state:
case mpr
x : Game
⊢ x = 0 → x.birthday = 0

Tactic:
rintro rfl

Result:
case mpr

⊢ birthday 0 = 0

Proof state:
case mp
x : Game
h : x.birthday = 0
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ x = 0

Tactic:
rw [← hy₁]

Result:
case mp
x : Game
h : x.birthday = 0
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ ⟦y⟧ = 0

Proof state:
x : Game
⊢ x.birthday = 0 ↔ x = 0

Tactic:
constructor

Result:
case mp
x : Game
⊢ x.birthday = 0 → x = 0

case mpr
x : Game
⊢ x = 0 → x.birthday = 0

Proof state:
case mp
x : Game
h : x.birthday = 0
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : IsEmpty y.LeftMoves ∧ IsEmpty y.RightMoves
⊢ ⟦y⟧ = 0

Tactic:
exact PGame.game_eq (@PGame.Equiv.isEmpty _ hy₂.1 hy₂.2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Lemmas.lean
theorem div_le_iff_le_mul (h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1

Proof state:
k x y : Nat
h : 0 < k
⊢ x / k ≤ y ↔ x ≤ y * k + k - 1

Tactic:
rw [le_iff_lt_add_one, Nat.div_lt_iff_lt_mul h, Nat.add_one_mul]

Result:
k x y : Nat
h : 0 < k
⊢ x < y * k + k ↔ x ≤ y * k + k - 1

Proof state:
k x y : Nat
h : 0 < k
⊢ x < y * k + k ↔ x ≤ y * k + k - 1

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_sub (x y : PGame) : (x - y).birthday = x.birthday ♯ y.birthday

Proof state:
x y : PGame
⊢ x.birthday ♯ (-y).birthday = x.birthday ♯ y.birthday

Tactic:
rw [birthday_neg]

Result:
no goals

Proof state:
x y : PGame
⊢ (x - y).birthday = x.birthday ♯ y.birthday

Tactic:
apply (birthday_add x _).trans

Result:
x y : PGame
⊢ x.birthday ♯ (-y).birthday = x.birthday ♯ y.birthday
-- Mathlib/Algebra/Quaternion.lean
theorem sq_eq_normSq : a ^ 2 = normSq a ↔ a = a.re

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a

Tactic:
exact or_iff_left_of_imp fun ha ↦ ha.symm ▸ star_zero _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = ↑(normSq a) ↔ a = ↑a.re

Tactic:
rw [← star_eq_self, ← star_mul_self, sq, mul_eq_mul_right_iff, eq_comm]

Result:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiffOn.div {f g : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s)
    (hg : ContMDiffOn I' I n g s) : ContMDiffOn I' I n (fun x => f x / g x) s

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
⊢ ContMDiffOn I' I n (fun x => f x * (g x)⁻¹) s

Tactic:
exact hf.mul hg.inv

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
⊢ ContMDiffOn I' I n (fun x => f x / g x) s

Tactic:
simp_rw [div_eq_mul_inv]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
⊢ ContMDiffOn I' I n (fun x => f x * (g x)⁻¹) s
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.cons_getLast_dropLast
    (L : List α) (hL : L ≠ []) : L.getLast hL :: L.dropLast ~r L

Proof state:
α : Type u
L : List α
hL : L ≠ []
⊢ L.getLast hL :: L.dropLast ~r L

Tactic:
induction L using List.reverseRecOn with
| nil => simp at hL
| append_singleton a L _ =>
  simp only [getLast_append, dropLast_concat]
  apply IsRotated.symm
  apply isRotated_concat

Result:
no goals

Proof state:
case append_singleton.h
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ a ++ [L] ~r (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a

Tactic:
apply isRotated_concat

Result:
no goals

Proof state:
case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (a ++ [L]).getLast hL :: (a ++ [L]).dropLast ~r a ++ [L]

Tactic:
simp only [getLast_append, dropLast_concat]

Result:
case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a ~r a ++ [L]

Proof state:
case nil
α : Type u
hL : [] ≠ []
⊢ [].getLast hL :: [].dropLast ~r []

Tactic:
simp at hL

Result:
no goals

Proof state:
case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a ~r a ++ [L]

Tactic:
apply IsRotated.symm

Result:
case append_singleton.h
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ a ++ [L] ~r (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem terminatedAt_iff_s_none : g.TerminatedAt n ↔ g.s.get? n = none

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.s.get? n = none

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem mem_keys_kunion {a} {l₁ l₂ : List (Sigma β)} :
    a ∈ (kunion l₁ l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
⊢ a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys

Tactic:
induction l₁ generalizing l₂ with
| nil => simp
| cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys
l₂ : List (Sigma β)
⊢ a ∈ ((s :: l₁).kunion l₂).keys ↔ a ∈ (s :: l₁).keys ∨ a ∈ l₂.keys

Tactic:
by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
⊢ a ∈ ([].kunion l₂).keys ↔ a ∈ [].keys ∨ a ∈ l₂.keys

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Killing.lean
lemma ideal_eq_bot_of_isLieAbelian
    [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R]
    (I : LieIdeal R L) [IsLieAbelian I] : I = ⊥

Proof state:
R : Type u_1
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : IsKilling R L
inst✝⁴ : Module.Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I ≤ LieIdeal.killingCompl R L ⊤

Tactic:
exact I.le_killingCompl_top_of_isLieAbelian

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : IsKilling R L
inst✝⁴ : Module.Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I = ⊥

Tactic:
rw [eq_bot_iff, ← killingCompl_top_eq_bot]

Result:
R : Type u_1
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : IsKilling R L
inst✝⁴ : Module.Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I ≤ LieIdeal.killingCompl R L ⊤
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_nonneg_of_isNat {n : ℕ} (h : NormNum.IsNat e n) : 0 ≤ Real.log (e : ℝ)

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n

Tactic:
exact Real.log_natCast_nonneg _

Result:
no goals

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Result:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem isCoprime_self : IsCoprime x x ↔ IsUnit x :=
  ⟨fun ⟨a, b, h⟩ => isUnit_of_mul_eq_one x (a + b) <| by rwa [mul_comm, add_mul], fun h =>
    let ⟨b, hb⟩ := isUnit_iff_exists_inv'.1 h
    ⟨b, 0, by rwa [zero_mul, add_zero]⟩⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
h : IsUnit x
b : R
hb : b * x = 1
⊢ b * x + 0 * x = 1

Tactic:
rwa [zero_mul, add_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
x✝ : IsCoprime x x
a b : R
h : a * x + b * x = 1
⊢ x * (a + b) = 1

Tactic:
rwa [mul_comm, add_mul]

Result:
no goals
-- Mathlib/Data/Finset/MulAntidiagonal.lean
theorem IsPWO.mul [OrderedCancelCommMonoid α] (hs : s.IsPWO) (ht : t.IsPWO) : IsPWO (s * t)

Proof state:
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : s.IsPWO
ht : t.IsPWO
⊢ ((fun x => x.1 * x.2) '' s ×ˢ t).IsPWO

Tactic:
exact (hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : s.IsPWO
ht : t.IsPWO
⊢ (s * t).IsPWO

Tactic:
rw [← image_mul_prod]

Result:
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : s.IsPWO
ht : t.IsPWO
⊢ ((fun x => x.1 * x.2) '' s ×ˢ t).IsPWO
-- Mathlib/GroupTheory/Exponent.lean
@[to_additive]
lemma orderOf_eq_two_iff (hG : Monoid.exponent G = 2) {x : G} :
    orderOf x = 2 ↔ x ≠ 1 :=
  ⟨by rintro hx rfl; norm_num at hx, orderOf_eq_prime (hG ▸ Monoid.pow_exponent_eq_one x)⟩

Proof state:
G : Type u
inst✝ : Monoid G
hG : Monoid.exponent G = 2
x : G
⊢ orderOf x = 2 → x ≠ 1

Tactic:
rintro hx rfl

Result:
G : Type u
inst✝ : Monoid G
hG : Monoid.exponent G = 2
hx : orderOf 1 = 2
⊢ False

Proof state:
G : Type u
inst✝ : Monoid G
hG : Monoid.exponent G = 2
hx : orderOf 1 = 2
⊢ False

Tactic:
norm_num at hx

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma pow_def (q : ℚ) (n : ℕ) :
    q ^ n = ⟨q.num ^ n, q.den ^ n,
      by simp [Nat.pow_eq_zero],
      by rw [Int.natAbs_pow]; exact q.reduced.pow _ _⟩ := rfl

Proof state:
q✝ q : ℚ
n : ℕ
⊢ (q.num.natAbs ^ n).Coprime (q.den ^ n)

Tactic:
exact q.reduced.pow _ _

Result:
no goals

Proof state:
q✝ q : ℚ
n : ℕ
⊢ q.den ^ n ≠ 0

Tactic:
simp [Nat.pow_eq_zero]

Result:
no goals

Proof state:
q✝ q : ℚ
n : ℕ
⊢ (q.num ^ n).natAbs.Coprime (q.den ^ n)

Tactic:
rw [Int.natAbs_pow]

Result:
q✝ q : ℚ
n : ℕ
⊢ (q.num.natAbs ^ n).Coprime (q.den ^ n)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_extract {as : Vector α n} {start stop : Nat} :
    (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none

Proof state:
case mk
α : Type u_1
i start stop : Nat
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.extract start stop)[i]? =
    if i < min stop { toArray := as, size_toArray := ⋯ }.size - start then
      { toArray := as, size_toArray := ⋯ }[start + i]?
    else none

Tactic:
simp [Array.getElem?_extract]

Result:
no goals

Proof state:
α : Type u_1
n i : Nat
as : Vector α n
start stop : Nat
⊢ (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
i start stop : Nat
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.extract start stop)[i]? =
    if i < min stop { toArray := as, size_toArray := ⋯ }.size - start then
      { toArray := as, size_toArray := ⋯ }[start + i]?
    else none
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem left_mem_perpBisector : p₁ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ p₁ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂

Tactic:
rw [perpBisector_comm, right_mem_perpBisector, eq_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc]
lemma germ_stalkClosedPointTo (U : Opens X) (hU : f.base (closedPoint R) ∈ U) :
    X.presheaf.germ U _ hU ≫ stalkClosedPointTo f = f.app U ≫
      ((Spec R).presheaf.mapIso (eqToIso (preimage_eq_top_of_closedPoint_mem f hU).symm).op ≪≫
        ΓSpecIso R).hom

Proof state:
case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU ≫ (stalkClosedPointIso R).hom =
    (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom

Tactic:
rw [← Iso.eq_comp_inv, Category.assoc, ΓSpecIso_hom_stalkClosedPointIso_inv]

Result:
case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU =
    (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Proof state:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ U
⊢ Hom.app f U ≫ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU ≫ (stalkClosedPointIso R).hom =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom

Tactic:
congr 1

Result:
case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU ≫ (stalkClosedPointIso R).hom =
    (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom

Proof state:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom f.base) (closedPoint ↑R)) hU ≫ stalkClosedPointTo f =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op ≪≫ ΓSpecIso R).hom

Tactic:
rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, Iso.trans_hom]

Result:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ U
⊢ Hom.app f U ≫ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU ≫ (stalkClosedPointIso R).hom =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom

Proof state:
case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU =
    (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
simp only [TopCat.Presheaf.pushforward_obj_obj, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
  TopCat.Presheaf.germ_res]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem not_nonempty_iff_eq_empty {s : Set α} : ¬s.Nonempty ↔ s = ∅

Proof state:
α : Type u
s : Set α
⊢ ¬s.Nonempty ↔ s = ∅

Tactic:
simp only [Set.Nonempty, not_exists, eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_signExtend {x : BitVec w} :
    (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)

Proof state:
w v : Nat
x : BitVec w
h : w ≥ v
⊢ v - w = 0

Tactic:
omega

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
h : ¬w ≥ v
⊢ ¬v - w = 0

Tactic:
omega

Result:
no goals

Proof state:
case pos
w v : Nat
x : BitVec w
h : w ≥ v
⊢ (signExtend v x).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)

Tactic:
simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
⊢ (signExtend v x).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)

Tactic:
by_cases h : w ≥ v

Result:
case pos
w v : Nat
x : BitVec w
h : w ≥ v
⊢ (signExtend v x).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)

case neg
w v : Nat
x : BitVec w
h : ¬w ≥ v
⊢ (signExtend v x).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)

Proof state:
case neg
w v : Nat
x : BitVec w
h : ¬w ≥ v
⊢ (signExtend v x).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)

Tactic:
simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]

Result:
no goals
-- Mathlib/Algebra/Equiv/TransferInstance.lean
theorem ringEquiv_symm_apply (e : α ≃ β) [Add β] [Mul β] (b : β) : by
    letI := Equiv.add e
    letI := Equiv.mul e
    exact (ringEquiv e).symm b = e.symm b := rfl

Proof state:
α : Type u
β : Type v
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this✝ : Add α := e.add
this : Mul α := e.mul
⊢ Sort ?u.10965

Tactic:
exact (ringEquiv e).symm b = e.symm b

Result:
no goals

Proof state:
α : Type u
β : Type v
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
⊢ Sort ?u.10965

Tactic:
letI := Equiv.add e

Result:
α : Type u
β : Type v
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this : Add α := e.add
⊢ Sort ?u.10965

Proof state:
α : Type u
β : Type v
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this : Add α := e.add
⊢ Sort ?u.10965

Tactic:
letI := Equiv.mul e

Result:
α : Type u
β : Type v
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this✝ : Add α := e.add
this : Mul α := e.mul
⊢ Sort ?u.10965
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left
    [Algebra.IsAlgebraic (⊥ : Subalgebra R S) S] : Algebra.IsAlgebraic R S :=
  Algebra.IsAlgebraic.of_ringHom_of_comp_eq (algebraMap R (⊥ : Subalgebra R S))
    (RingHom.id S) (by rintro ⟨_, r, rfl⟩; exact ⟨r, rfl⟩) Function.injective_id (by ext; rfl)

Proof state:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
⊢ (algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥) = (↑(RingHom.id S)).comp (algebraMap R S)

Tactic:
ext

Result:
case a
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
x✝ : R
⊢ ((algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥)) x✝ = ((↑(RingHom.id S)).comp (algebraMap R S)) x✝

Proof state:
case a
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
x✝ : R
⊢ ((algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥)) x✝ = ((↑(RingHom.id S)).comp (algebraMap R S)) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
⊢ Function.Surjective ⇑(algebraMap R ↥⊥)

Tactic:
rintro ⟨_, r, rfl⟩

Result:
case mk.intro
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩

Proof state:
case mk.intro
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩

Tactic:
exact ⟨r, rfl⟩

Result:
no goals