harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_smul_closedBall (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
    Metric.closedBall (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b ≤ r₂
⊢ ‖a‖ * p b ≤ r₁ * r₂

Tactic:
gcongr

Result:
case b0
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b ≤ r₂
⊢ 0 ≤ r₁

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), p b ≤ r₂ → ‖a‖ * p b ≤ r₁ * r₂

Tactic:
intro a ha b hb

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b ≤ r₂
⊢ ‖a‖ * p b ≤ r₁ * r₂

Proof state:
case b0
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b ≤ r₂
⊢ 0 ≤ r₁

Tactic:
exact (norm_nonneg _).trans ha

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ Metric.closedBall 0 r₁ • p.closedBall 0 r₂ ⊆ p.closedBall 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_closedBall_zero, mem_closedBall_zero_iff, map_smul_eq_mul]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), p b ≤ r₂ → ‖a‖ * p b ≤ r₁ * r₂
-- Mathlib/Analysis/Seminorm.lean
theorem absorbent_ball_zero (hr : 0 < r) : Absorbent 𝕜 (Metric.ball (0 : E) r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 ((normSeminorm 𝕜 E).ball 0 r)

Tactic:
exact (normSeminorm _ _).absorbent_ball_zero hr

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 (Metric.ball 0 r)

Tactic:
rw [← ball_normSeminorm 𝕜]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 ((normSeminorm 𝕜 E).ball 0 r)
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.coe_reApplyInnerSelf_apply {T : E →L[𝕜] E} (hT : IsSymmetric (T : E →ₗ[𝕜] E))
    (x : E) : (T.reApplyInnerSelf x : 𝕜) = ⟪T x, x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ (starRingEnd 𝕜) (inner (T x) x) = inner (T x) x

Tactic:
exact hT.conj_inner_sym x x

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
r : ℝ
hr : inner (T x) x = ↑r
⊢ ↑(T.reApplyInnerSelf x) = inner (T x) x

Tactic:
simp [hr, T.reApplyInnerSelf_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ↑(T.reApplyInnerSelf x) = inner (T x) x

Tactic:
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
r : ℝ
hr : inner (T x) x = ↑r
⊢ ↑(T.reApplyInnerSelf x) = inner (T x) x

𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ∃ r, inner (T x) x = ↑r

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ ∃ r, inner (T x) x = ↑r

Tactic:
rw [← conj_eq_iff_real]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
x : E
⊢ (starRingEnd 𝕜) (inner (T x) x) = inner (T x) x
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem eq_prod_roots_of_monic_of_splits_id {p : K[X]} (m : Monic p)
    (hsplit : Splits (RingHom.id K) p) : p = (p.roots.map fun a => X - C a).prod

Proof state:
case h.e'_3
K : Type v
inst✝ : Field K
p : K[X]
m : p.Monic
hsplit : Splits (RingHom.id K) p
⊢ (Multiset.map (fun a => X - C a) p.roots).prod = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod

Tactic:
simp [m]

Result:
no goals

Proof state:
K : Type v
inst✝ : Field K
p : K[X]
m : p.Monic
hsplit : Splits (RingHom.id K) p
⊢ p = (Multiset.map (fun a => X - C a) p.roots).prod

Tactic:
convert eq_prod_roots_of_splits_id hsplit

Result:
case h.e'_3
K : Type v
inst✝ : Field K
p : K[X]
m : p.Monic
hsplit : Splits (RingHom.id K) p
⊢ (Multiset.map (fun a => X - C a) p.roots).prod = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.even_odd₁ (a b c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 1)
    (hc : a / 2 = c) (hr : jacobiSymNat c b = r) : jacobiSymNat a b = r

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
simp [hb]

Result:
no goals

Proof state:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
norm_num

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Result:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.ofNat_ediv, Nat.cast_ofNat]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 2) b
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma even_xor'_odd' (n : ℤ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)

Proof state:
n : ℤ
⊢ ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)

Tactic:
rcases even_or_odd n with (⟨k, rfl⟩ | ⟨k, rfl⟩) <;> use k

Result:
case h
k : ℤ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)

case h
k : ℤ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)

Proof state:
case h
k : ℤ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)

Tactic:
simpa only [← two_mul, Xor', true_and, eq_self_iff_true, not_true, or_false,
  and_false] using (succ_ne_self (2 * k)).symm

Result:
no goals

Proof state:
case h
k : ℤ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)

Tactic:
simp only [Xor', add_right_eq_self, false_or, eq_self_iff_true, not_true, not_false_iff,
  one_ne_zero, and_self_iff]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem nonzero_mul_comm (a b : A) : σ (a * b) \ {0} = σ (b * a) \ {0}

Proof state:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}

Tactic:
rintro _ _ k ⟨k_mem, k_neq⟩

Result:
case intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_mem : k ∈ σ (x✝ * y✝)
k_neq : k ∉ {0}
⊢ k ∈ σ (y✝ * x✝) \ {0}

Proof state:
case intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_mem : k ∈ σ (x✝ * y✝)
k_neq : k ∉ {0}
⊢ k ∈ σ (y✝ * x✝) \ {0}

Tactic:
change ((Units.mk0 k k_neq) : 𝕜) ∈ _ at k_mem

Result:
case intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_neq : k ∉ {0}
k_mem : ↑(Units.mk0 k k_neq) ∈ σ (x✝ * y✝)
⊢ k ∈ σ (y✝ * x✝) \ {0}

Proof state:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ σ (a * b) \ {0} = σ (b * a) \ {0}

Tactic:
suffices h : ∀ x y : A, σ (x * y) \ {0} ⊆ σ (y * x) \ {0} from
  Set.eq_of_subset_of_subset (h a b) (h b a)

Result:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ ∀ (x y : A), σ (x * y) \ {0} ⊆ σ (y * x) \ {0}

Proof state:
case intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_neq : k ∉ {0}
k_mem : ↑(Units.mk0 k k_neq) ∈ σ (x✝ * y✝)
⊢ k ∈ σ (y✝ * x✝) \ {0}

Tactic:
exact ⟨unit_mem_mul_comm.mp k_mem, k_neq⟩

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : ∑ i ∈ range n, x ^ i / i ! ≤ exp x :=
  calc
    ∑ i ∈ range n, x ^ i / i ! ≤ lim (⟨_, isCauSeq_re (exp' x)⟩ : CauSeq ℝ abs)

Proof state:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ↑(const abs (∑ i ∈ range n, x ^ i / ↑i !)) j ≤ ↑⟨fun n => (↑(exp' ↑x) n).re, ⋯⟩ j

Tactic:
simp only [exp', const_apply, re_sum]

Result:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ range n, x ^ i / ↑i ! ≤ ∑ i ∈ range j, (↑x ^ i / ↑i !).re

Proof state:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ ∑ i ∈ range n, x ^ i / ↑i ! ≤ CauSeq.lim ⟨fun n => (↑(exp' ↑x) n).re, ⋯⟩

Tactic:
refine le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)

Result:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ↑(const abs (∑ i ∈ range n, x ^ i / ↑i !)) j ≤ ↑⟨fun n => (↑(exp' ↑x) n).re, ⋯⟩ j

Proof state:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ CauSeq.lim ⟨fun n => (↑(exp' ↑x) n).re, ⋯⟩ = rexp x

Tactic:
rw [exp, Complex.exp, ← cauSeqRe, lim_re]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ range n, x ^ i / ↑i ! ≤ ∑ i ∈ range j, x ^ i / ↑i !

Tactic:
refine sum_le_sum_of_subset_of_nonneg (range_mono hj) fun _ _ _ ↦ ?_

Result:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
x✝² : ℕ
x✝¹ : x✝² ∈ range j
x✝ : x✝² ∉ range n
⊢ 0 ≤ x ^ x✝² / ↑x✝²!

Proof state:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
x✝² : ℕ
x✝¹ : x✝² ∈ range j
x✝ : x✝² ∉ range n
⊢ 0 ≤ x ^ x✝² / ↑x✝²!

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ range n, x ^ i / ↑i ! ≤ ∑ i ∈ range j, (↑x ^ i / ↑i !).re

Tactic:
norm_cast

Result:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ range n, x ^ i / ↑i ! ≤ ∑ i ∈ range j, x ^ i / ↑i !
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem two_zsmul_oangle_of_vectorSpan_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P}
    (h₁₂₄₅ : vectorSpan ℝ ({p₁, p₂} : Set P) = vectorSpan ℝ ({p₄, p₅} : Set P))
    (h₃₂₆₅ : vectorSpan ℝ ({p₃, p₂} : Set P) = vectorSpan ℝ ({p₆, p₅} : Set P)) :
    (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ 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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅}
h₃₂₆₅ : vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆

Tactic:
simp_rw [vectorSpan_pair] at h₁₂₄₅ h₃₂₆₅

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Submodule.span ℝ {p₁ -ᵥ p₂} = Submodule.span ℝ {p₄ -ᵥ p₅}
h₃₂₆₅ : Submodule.span ℝ {p₃ -ᵥ p₂} = Submodule.span ℝ {p₆ -ᵥ p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ 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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₁₂₄₅ : Submodule.span ℝ {p₁ -ᵥ p₂} = Submodule.span ℝ {p₄ -ᵥ p₅}
h₃₂₆₅ : Submodule.span ℝ {p₃ -ᵥ p₂} = Submodule.span ℝ {p₆ -ᵥ p₅}
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆

Tactic:
exact o.two_zsmul_oangle_of_span_eq_of_span_eq h₁₂₄₅ h₃₂₆₅

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma mul_entry_mul_eq_inner_toCLM [DecidableEq m] [DecidableEq n] {M : CStarMatrix m n A}
    {i : m} {j : n} (a b : A) :
    star a * M i j * b
      = ⟪equiv _ |>.symm (Pi.single i a), toCLM M (equiv _ |>.symm <| Pi.single j b)⟫_A

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : NonUnitalCStarAlgebra A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : CStarMatrix m n A
i : m
j : n
a b : A
⊢ star a * M i j * b = ⟪(equiv (m → A)).symm (Pi.single i a), (toCLM M) ((equiv (n → A)).symm (Pi.single j b))⟫_A

Tactic:
simp [mul_assoc, inner_def]

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem equiv_image_eq_iff_subset (e : α ≃ α) (hs : s.Finite) : e '' s = s ↔ e '' s ⊆ s :=
  ⟨fun h ↦ by rw [h], fun h ↦ hs.eq_of_subset_of_card_le h <|
    ge_of_eq (Nat.card_congr (e.image s).symm)⟩

Proof state:
α : Type u_1
s : Set α
e : α ≃ α
hs : s.Finite
h : ⇑e '' s = s
⊢ ⇑e '' s ⊆ s

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem perm_card_two_iff {a₁ b₁ a₂ b₂ : α} :
    [a₁, b₁].Perm [a₂, b₂] ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂ :=
  { mp

Proof state:
case p
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [].Perm []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
apply List.Perm.swap'

Result:
case p
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [].Perm []

Proof state:
α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁].Perm [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.coe_nil, Multiset.cons_zero,
  Multiset.cons_eq_cons, Multiset.singleton_inj, ne_eq, Multiset.singleton_eq_cons_iff,
  exists_eq_right_right, and_true]

Result:
α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Proof state:
α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
done

Result:
no goals

Proof state:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [a₁, b₁].Perm [a₂, b₂]

Tactic:
rw [h₁, h₂]

Result:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Proof state:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
first | done | apply List.Perm.swap'; rfl

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem rank_congr {H K : Subgroup G} [Group.FG H] [Group.FG K] (h : H = K) :
    Group.rank H = Group.rank K

Proof state:
G : Type u_3
inst✝² : Group G
H : Subgroup G
inst✝¹ inst✝ : Group.FG ↥H
⊢ Group.rank ↥H = Group.rank ↥H

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_3
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Group.FG ↥H
inst✝ : Group.FG ↥K
h : H = K
⊢ Group.rank ↥H = Group.rank ↥K

Tactic:
subst h

Result:
G : Type u_3
inst✝² : Group G
H : Subgroup G
inst✝¹ inst✝ : Group.FG ↥H
⊢ Group.rank ↥H = Group.rank ↥H
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_sub_natCast' {n : ℕ} (h : y - n ≠ 0) (x : ℝ≥0) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
y : ℝ
n : ℕ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
ext

Result:
case a
y : ℝ
n : ℕ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Proof state:
case a
y : ℝ
n : ℕ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
exact Real.rpow_sub_natCast' (mod_cast x.2) h

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem log_monotone {b : ℕ} : Monotone (log b)

Proof state:
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)

Tactic:
exact zero_le _

Result:
no goals

Proof state:
b n : ℕ
⊢ log b n ≤ log b (n + 1)

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)

case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)

Proof state:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)

Tactic:
rw [log_of_left_le_one hb]

Result:
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)

Proof state:
b : ℕ
⊢ Monotone (log b)

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

Result:
b n : ℕ
⊢ log b n ≤ log b (n + 1)

Proof state:
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)

Tactic:
exact le_log_of_pow_le hb (pow_log_le_add_one _ _)

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem trans_transHomeomorph (e : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z)
    (f'' : Z ≃ₜ Z') :
    (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
e' : PartialHomeomorph Y Z
f'' : Z ≃ₜ Z'
⊢ (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')

Tactic:
simp only [transHomeomorph_eq_trans, trans_assoc, Homeomorph.trans_toPartialHomeomorph]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_add_left_iff {f : M → N} {x x' y : M} :
    polar f (x + x') y = polar f x y + polar f x' y ↔
      f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Tactic:
simp only [add_right_comm _ (f y) _, add_right_comm _ (f x') (f x)]

Result:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

Tactic:
simp only [← add_assoc]

Result:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Tactic:
rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)),
  add_right_comm (f (x + y)), add_left_inj]

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Tactic:
simp only [polar, sub_eq_iff_eq_add, eq_sub_iff_add_eq, sub_add_eq_add_sub, add_sub]

Result:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem coeff_hermite_of_even_add {n k : ℕ} (hnk : Even (n + k)) :
    coeff (hermite n) k = (-1) ^ ((n - k) / 2) * (n - k - 1)‼ * Nat.choose n k

Proof state:
case inl
n k : ℕ
hnk : Even (n - k)
h_le : k ≤ n
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
obtain ⟨m, hm⟩ := hnk

Result:
case inl.intro
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Proof state:
case inl
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
rw [Nat.even_add, ← Nat.even_sub h_le] at hnk

Result:
case inl
n k : ℕ
hnk : Even (n - k)
h_le : k ≤ n
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Proof state:
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ n = 2 * m + k

Tactic:
omega

Result:
no goals

Proof state:
n k : ℕ
hnk : Even (n + k)
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
rcases le_or_lt k n with h_le | h_lt

Result:
case inl
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

case inr
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Proof state:
case inl.intro
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
rw [(by omega : n = 2 * m + k),
  Nat.add_sub_cancel, Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]

Result:
no goals

Proof state:
case inr
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
simp [Nat.choose_eq_zero_of_lt h_lt, coeff_hermite_of_lt h_lt]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformlyOn.mono (h : TendstoLocallyUniformlyOn F f p s) (h' : s' ⊆ s) :
    TendstoLocallyUniformlyOn F f p s'

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
⊢ TendstoLocallyUniformlyOn F f p s'

Tactic:
intro u hu x hx

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases h u hu x (h' hx) with ⟨t, ht, H⟩

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

Result:
no goals