harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Rat/Lemmas.lean
theorem inv_intCast_den_of_pos {a : ℤ} (ha0 : 0 < a) : ((a : ℚ)⁻¹.den : ℤ) = a

Proof state:
a : ℤ
ha0 : 0 < a
⊢ ↑(↑a)⁻¹.den = a

Tactic:
rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_divInt', divInt_eq_div, Nat.cast_one]

Result:
a : ℤ
ha0 : 0 < a
⊢ ↑(↑1 / ↑a).den = a

Proof state:
a : ℤ
ha0 : 0 < a
⊢ (Int.natAbs 1).Coprime a.natAbs

Tactic:
rw [Int.natAbs_one]

Result:
a : ℤ
ha0 : 0 < a
⊢ Nat.Coprime 1 a.natAbs

Proof state:
a : ℤ
ha0 : 0 < a
⊢ ↑(↑1 / ↑a).den = a

Tactic:
apply den_div_eq_of_coprime ha0

Result:
a : ℤ
ha0 : 0 < a
⊢ (Int.natAbs 1).Coprime a.natAbs

Proof state:
a : ℤ
ha0 : 0 < a
⊢ Nat.Coprime 1 a.natAbs

Tactic:
exact Nat.coprime_one_left _

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

Proof state:
k x : Nat
h : 0 < k
w : k ≤ x
this : x % k < k
⊢ x - k < x - x % k

Tactic:
omega

Result:
no goals

Proof state:
k x : Nat
h : 0 < k
w : k ≤ x
⊢ x - k < x - x % k

Tactic:
have : x % k < k := mod_lt x h

Result:
k x : Nat
h : 0 < k
w : k ≤ x
this : x % k < k
⊢ x - k < x - x % k

Proof state:
k x : Nat
h : 0 < k
w : k ≤ x
⊢ x - k < x / k * k

Tactic:
rw [div_mul_self_eq_mod_sub_self]

Result:
k x : Nat
h : 0 < k
w : k ≤ x
⊢ x - k < x - x % k
-- Mathlib/Topology/Compactification/OnePoint.lean
lemma continuous_iff_from_discrete {Y : Type*} [TopologicalSpace Y]
    [DiscreteTopology X] (f : OnePoint X → Y) :
    Continuous f ↔ Tendsto (fun x : X ↦ f x) cofinite (𝓝 (f ∞))

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : DiscreteTopology X
f : OnePoint X → Y
⊢ Continuous f ↔ Tendsto (fun x => f ↑x) cofinite (𝓝 (f ∞))

Tactic:
simp [continuous_iff, cocompact_eq_cofinite, continuous_of_discreteTopology]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
lemma volume_ball_of_dim_even {k : ℕ} (hk : finrank ℝ E = 2 * k) (x : E) (r : ℝ) :
    volume (ball x r) = .ofReal r ^ finrank ℝ E * .ofReal (π ^ k / (k : ℕ)!)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ (ENNReal.ofReal r ^ 2) ^ k * ENNReal.ofReal (π ^ k / Gamma (↑(2 * k) / 2 + 1)) =
    (ENNReal.ofReal r ^ 2) ^ k * ENNReal.ofReal (π ^ k / ↑k !)

Tactic:
congr

Result:
case e_a.e_r.e_a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ Gamma (↑(2 * k) / 2 + 1) = ↑k !

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ volume (ball x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / ↑k !)

Tactic:
rw [volume_ball, hk, pow_mul, pow_mul, sq_sqrt pi_nonneg]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ (ENNReal.ofReal r ^ 2) ^ k * ENNReal.ofReal (π ^ k / Gamma (↑(2 * k) / 2 + 1)) =
    (ENNReal.ofReal r ^ 2) ^ k * ENNReal.ofReal (π ^ k / ↑k !)

Proof state:
case e_a.e_r.e_a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ Gamma (↑(2 * k) / 2 + 1) = ↑k !

Tactic:
simp [Gamma_nat_eq_factorial]

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem Irreducible.squarefree [CommMonoid R] {x : R} (h : Irreducible x) : Squarefree x

Proof state:
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
⊢ Squarefree x

Tactic:
rintro y ⟨z, hz⟩

Result:
case intro
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * y * z
⊢ IsUnit y

Proof state:
case intro
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * y * z
⊢ IsUnit y

Tactic:
rw [mul_assoc] at hz

Result:
case intro
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
⊢ IsUnit y

Proof state:
case intro.inl
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y

Tactic:
exact hu

Result:
no goals

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit (y * z)
⊢ IsUnit y

Tactic:
apply isUnit_of_mul_isUnit_left hu

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
⊢ IsUnit y

Tactic:
rcases h.isUnit_or_isUnit hz with (hu | hu)

Result:
case intro.inl
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y

case intro.inr
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit (y * z)
⊢ IsUnit y
-- Mathlib/Algebra/Quaternion.lean
theorem mul_star_eq_coe : a * star a = (a * star a).re

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a * star a = ↑(a * star a).re

Tactic:
rw [← star_comm_self']

Result:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a * a = ↑(star a * a).re

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a * a = ↑(star a * a).re

Tactic:
exact a.star_mul_eq_coe

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma pow_eq_neg_pow_iff (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n :=
  match n.even_or_odd with
  | .inl he =>
    suffices a ^ n > -b ^ n by simpa [he, not_odd_iff_even.2 he] using this.ne'
    lt_of_lt_of_le (by simp [he.pow_pos hb]) (he.pow_nonneg _)
  | .inr ho => by
    simp only [ho, and_true, ← ho.neg_pow, (ho.strictMono_pow (R := R)).injective.eq_iff]

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
⊢ -b ^ n < 0

Tactic:
simp [he.pow_pos hb]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
he : Even n
this : a ^ n > -b ^ n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
simpa [he, not_odd_iff_even.2 he] using this.ne'

Result:
no goals

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a b : R
n : ℕ
hb : b ≠ 0
ho : Odd n
⊢ a ^ n = -b ^ n ↔ a = -b ∧ Odd n

Tactic:
simp only [ho, and_true, ← ho.neg_pow, (ho.strictMono_pow (R := R)).injective.eq_iff]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem ContinuousLinearMap.comp_analyticOn (g : F →L[𝕜] G) (h : AnalyticOn 𝕜 f s) :
    AnalyticOn 𝕜 (g ∘ f) s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (⇑g ∘ f) s

Tactic:
rintro x hx

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
⊢ AnalyticWithinAt 𝕜 (⇑g ∘ f) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
⊢ AnalyticWithinAt 𝕜 (⇑g ∘ f) s x

Tactic:
rcases h x hx with ⟨p, r, hp⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticWithinAt 𝕜 (⇑g ∘ f) s x

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticWithinAt 𝕜 (⇑g ∘ f) s x

Tactic:
exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesWithinOnBall hp⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem fderivWithin_inv (x_ne_zero : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x => x⁻¹) s x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹)

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = smulRight 1 (-(x ^ 2)⁻¹)

Tactic:
exact fderiv_inv

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x => x⁻¹) s x = smulRight 1 (-(x ^ 2)⁻¹)

Tactic:
rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs]

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = smulRight 1 (-(x ^ 2)⁻¹)
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin
    [IsManifold I n M] [IsManifold I' n M'] (hn : n ≠ ∞) :
    ContMDiffWithinAt I I' n f s x ↔
      ∀ᶠ x' in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
⊢ ∀ᶠ (x' : M) in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x'

Tactic:
filter_upwards [hu, eventually_mem_nhdsWithin_iff.mpr hu] with x' h'x' hx'

Result:
case h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
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'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
u : Set M
hu : u ∈ 𝓝[insert x s] x
h : ContMDiffOn I I' n f u
x' : M
h'x' : x' ∈ u
hx' : u ∈ 𝓝[insert x s] x'
⊢ ContMDiffWithinAt I I' n f s x'
-- Mathlib/Data/List/SplitBy.lean
theorem chain'_getLast_head_splitBy (r : α → α → Bool) (l : List α) :
    (l.splitBy r).Chain' fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false

Proof state:
case nil
α : Type u_1
r : α → α → Bool
⊢ Chain' (fun a b => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r [])

Tactic:
exact chain'_nil

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Bool
head✝ : α
tail✝ : List α
⊢ ∀ (m : List α), m ∈ [].head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [head✝]).head hb) = false

Tactic:
rintro _ ⟨⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Bool
l : List α
⊢ Chain' (fun a b => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l)

Tactic:
cases l with
| nil => exact chain'_nil
| cons _ _ =>
  apply chain'_getLast_head_splitByLoop _ (not_mem_nil _) chain'_nil
  rintro _ ⟨⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Bool
head✝ : α
tail✝ : List α
⊢ Chain' (fun a b => ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r (head✝ :: tail✝))

Tactic:
apply chain'_getLast_head_splitByLoop _ (not_mem_nil _) chain'_nil

Result:
case cons
α : Type u_1
r : α → α → Bool
head✝ : α
tail✝ : List α
⊢ ∀ (m : List α), m ∈ [].head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [head✝]).head hb) = false
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem denom_add_dvd (x y : RatFunc K) : denom (x + y) ∣ denom x * denom y

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x + y = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
refine ⟨x.num * y.denom + x.denom * y.num, ?_⟩

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x + y =
    (algebraMap K[X] (RatFunc K)) (x.num * y.denom + x.denom * y.num) /
      (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Proof state:
case hd
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) y.denom ≠ 0

Tactic:
exact algebraMap_ne_zero (denom_ne_zero y)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (x + y).denom ∣ x.denom * y.denom

Tactic:
rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x + y = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Proof state:
case hb
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) x.denom ≠ 0

Tactic:
exact algebraMap_ne_zero (denom_ne_zero x)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x + y =
    (algebraMap K[X] (RatFunc K)) (x.num * y.denom + x.denom * y.num) /
      (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
rw [RingHom.map_mul, RingHom.map_add, RingHom.map_mul, RingHom.map_mul, ← div_add_div,
  num_div_denom, num_div_denom]

Result:
case hb
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) x.denom ≠ 0

case hd
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) y.denom ≠ 0
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma cast_negOnePow_natCast (R : Type*) [Ring R] (n : ℕ) : negOnePow n = (-1 : R) ^ n

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑↑(↑n).negOnePow = (-1) ^ n

Tactic:
obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n <;> simp [pow_succ, pow_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem linearIndependent_cols_iff_isUnit {A : Matrix m m K} :
    LinearIndependent K (fun i ↦ Aᵀ i) ↔ IsUnit A

Proof state:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ (LinearIndependent K fun i => Aᵀ i) ↔ IsUnit A

Tactic:
rw [← transpose_transpose A, isUnit_transpose, linearIndependent_rows_iff_isUnit,
  transpose_transpose]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Ideal.lean
/--
If a reflective subcategory is an exponential ideal, then the reflector preserves finite products.
-/
lemma preservesFiniteProducts_of_exponentialIdeal (J : Type) [Finite J] :
    PreservesLimitsOfShape (Discrete J) (reflector i)

Proof state:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : ChosenFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : ChosenFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Finite J
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) (reflector i) := preservesBinaryProducts_of_exponentialIdeal i
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) (reflector i) := leftAdjoint_preservesTerminal_of_reflective i
⊢ PreservesLimitsOfShape (Discrete J) (reflector i)

Tactic:
apply preservesFiniteProducts_of_preserves_binary_and_terminal (reflector i) J

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : ChosenFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : ChosenFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Finite J
⊢ PreservesLimitsOfShape (Discrete J) (reflector i)

Tactic:
letI := preservesBinaryProducts_of_exponentialIdeal i

Result:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : ChosenFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : ChosenFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Finite J
this : PreservesLimitsOfShape (Discrete WalkingPair) (reflector i) := preservesBinaryProducts_of_exponentialIdeal i
⊢ PreservesLimitsOfShape (Discrete J) (reflector i)

Proof state:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : ChosenFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : ChosenFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Finite J
this : PreservesLimitsOfShape (Discrete WalkingPair) (reflector i) := preservesBinaryProducts_of_exponentialIdeal i
⊢ PreservesLimitsOfShape (Discrete J) (reflector i)

Tactic:
letI : PreservesLimitsOfShape _ (reflector i) := leftAdjoint_preservesTerminal_of_reflective.{0} i

Result:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : ChosenFiniteProducts C
inst✝⁴ : Reflective i
inst✝³ : CartesianClosed C
inst✝² : ChosenFiniteProducts D
inst✝¹ : ExponentialIdeal i
J : Type
inst✝ : Finite J
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) (reflector i) := preservesBinaryProducts_of_exponentialIdeal i
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) (reflector i) := leftAdjoint_preservesTerminal_of_reflective i
⊢ PreservesLimitsOfShape (Discrete J) (reflector i)
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_zero_right (x : E) : ⟪x, 0⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ⟪x, 0⟫_𝕜 = 0

Tactic:
rw [← inner_conj_symm, inner_zero_left, RingHom.map_zero]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
/-- See also `Nat.mem_properDivisors`. -/
lemma mem_properDivisors_iff_exists {m n : ℕ} (hn : n ≠ 0) :
    m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k

Proof state:
case refine_2.intro.intro
m k : ℕ
hk : k > 1
hn : m * k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
rw [mul_ne_zero_iff] at hn

Result:
case refine_2.intro.intro
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors

Proof state:
case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors

Tactic:
rintro ⟨k, hk, rfl⟩

Result:
case refine_2.intro.intro
m k : ℕ
hk : k > 1
hn : m * k ≠ 0
⊢ m ∈ (m * k).properDivisors

Proof state:
m n : ℕ
hn : n ≠ 0
⊢ m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k

Tactic:
refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩

Result:
case refine_1
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors

Proof state:
case refine_2.intro.intro
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
exact mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩

Result:
no goals

Proof state:
case refine_1
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

Tactic:
exact (Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_int_eq {M : Type*} [AddCommGroup M] (s : AddSubgroup M) :
    (span ℤ (s : Set M)).toAddSubgroup = s

Proof state:
M : Type u_9
inst✝ : AddCommGroup M
s : AddSubgroup M
⊢ (span ℤ ↑s).toAddSubgroup = s

Tactic:
rw [span_int_eq_addSubgroup_closure, s.closure_eq]

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ n * exp (v * X)` is integrable for all `n : ℕ`. -/
lemma integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet
    (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    Integrable (fun ω ↦ |X ω| ^ n * exp (v * X ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω => |X ω| ^ n * rexp (v * X ω)) μ

Tactic:
convert integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hv
  (by positivity : 0 ≤ (n : ℝ)) with ω

Result:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
ω : Ω
⊢ |X ω| ^ n = |X ω| ^ ↑n

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
ω : Ω
⊢ |X ω| ^ n = |X ω| ^ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N :=
  ⟨fun h => funext fun i => funext <| h i, fun h => by simp [h]⟩

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M N : Matrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_flatMap (l : Array α) (g : α → Array β) (f : β → Bool) :
    (l.flatMap g).filter f = l.flatMap fun a => (g a).filter f

Proof state:
α : Type u_1
β : Type u_2
l : Array α
g : α → Array β
f : β → Bool
⊢ filter f (flatMap g l) = flatMap (fun a => filter f (g a)) l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
g : α → Array β
f : β → Bool
l : List α
⊢ filter f (flatMap g { toList := l }) = flatMap (fun a => filter f (g a)) { toList := l }

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → Array β
f : β → Bool
l : List α
⊢ filter f (flatMap g { toList := l }) = flatMap (fun a => filter f (g a)) { toList := l }

Tactic:
simp [List.filter_flatMap]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_coe_angle_toReal_eq_arg (z : ℂ) : (arg z : Real.Angle).toReal = arg z

Proof state:
z : ℂ
⊢ (↑z.arg).toReal = z.arg

Tactic:
rw [Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]

Result:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Proof state:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
exact arg_mem_Ioc _

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
theorem iSup_iInf_eq_top_of_commute {ι : Type*} {T : ι → E →ₗ[𝕜] E}
    (hT : ∀ i, (T i).IsSymmetric) (h : Pairwise (Commute on T)):
    ⨆ χ : ι → 𝕜, ⨅ i, eigenspace (T i) (χ i) = ⊤ :=
  calc
  _ = ⨆ χ : ι → 𝕜, ⨅ i, maxGenEigenspace (T i) (χ i) :=
    congr(⨆ χ : ι → 𝕜, ⨅ i,
      $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) (χ _))).symm
  _ = ⊤ :=
    iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute T h fun _ ↦ by
    rw [← orthogonal_eq_bot_iff,
      congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
      (hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
ι : Type u_5
T : ι → E →ₗ[𝕜] E
hT : ∀ (i : ι), (T i).IsSymmetric
h : Pairwise (Commute on T)
x✝ : ι
⊢ ⨆ μ, maxGenEigenspace (T x✝) μ = ⊤

Tactic:
rw [← orthogonal_eq_bot_iff,
  congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
  (hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]

Result:
no goals