harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem trans_toLinearEquiv (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) :
    (e₁.trans e₂).toLinearEquiv = e₁.toLinearEquiv.trans e₂.toLinearEquiv

Proof state:
case h
R₁ : Type u_3
R₂ : Type u_4
R₃ : Type u_5
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁶ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁵ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹² : RingHomInvPair σ₁₃ σ₃₁
inst✝¹¹ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_6
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_7
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
M₃ : Type u_8
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
x✝ : M₁
⊢ (e₁.trans e₂).toLinearEquiv x✝ = (e₁.trans e₂.toLinearEquiv) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R₁ : Type u_3
R₂ : Type u_4
R₃ : Type u_5
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁶ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁵ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹² : RingHomInvPair σ₁₃ σ₃₁
inst✝¹¹ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_6
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_7
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
M₃ : Type u_8
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
⊢ (e₁.trans e₂).toLinearEquiv = e₁.trans e₂.toLinearEquiv

Tactic:
ext

Result:
case h
R₁ : Type u_3
R₂ : Type u_4
R₃ : Type u_5
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁶ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁵ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹² : RingHomInvPair σ₁₃ σ₃₁
inst✝¹¹ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_6
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_7
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
M₃ : Type u_8
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
x✝ : M₁
⊢ (e₁.trans e₂).toLinearEquiv x✝ = (e₁.trans e₂.toLinearEquiv) x✝
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem eq_zero_iff {a : ℤ} {b : ℕ} : J(a | b) = 0 ↔ b ≠ 0 ∧ a.gcd b ≠ 1 :=
  ⟨fun h => by
    rcases eq_or_ne b 0 with hb | hb
    · rw [hb, zero_right] at h; cases h
    exact ⟨hb, mt jacobiSym.ne_zero <| Classical.not_not.2 h⟩, fun ⟨hb, h⟩ => by
    rw [← neZero_iff] at hb; exact eq_zero_iff_not_coprime.2 h⟩

Proof state:
a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : b ≠ 0
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0

Tactic:
rw [← neZero_iff] at hb

Result:
a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : NeZero b
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0

Proof state:
case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
rw [hb, zero_right] at h

Result:
case inl
a : ℤ
b : ℕ
h : 1 = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Proof state:
case inr
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b ≠ 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
exact ⟨hb, mt jacobiSym.ne_zero <| Classical.not_not.2 h⟩

Result:
no goals

Proof state:
a : ℤ
b : ℕ
h : J(a | b) = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
rcases eq_or_ne b 0 with hb | hb

Result:
case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

case inr
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b ≠ 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Proof state:
case inl
a : ℤ
b : ℕ
h : 1 = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
cases h

Result:
no goals

Proof state:
a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : NeZero b
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0

Tactic:
exact eq_zero_iff_not_coprime.2 h

Result:
no goals
-- Mathlib/Data/Set/Constructions.lean
theorem finiteInter_mem (cond : FiniteInter S) (F : Finset (Set α)) :
    ↑F ⊆ S → ⋂₀ (↑F : Set (Set α)) ∈ S

Proof state:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ∀ ⦃a : Set α⦄ {s : Finset (Set α)}, a ∉ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S

Tactic:
intro a s _ h1 h2

Result:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ ⋂₀ ↑(insert a s) ∈ S

Proof state:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
this : a ∩ ⋂₀ ↑s ∈ S
⊢ ⋂₀ ↑(insert a s) ∈ S

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ ⋂₀ ↑(insert a s) ∈ S

Tactic:
suffices a ∩ ⋂₀ ↑s ∈ S by simpa

Result:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ a ∩ ⋂₀ ↑s ∈ S

Proof state:
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ↑F ⊆ S → ⋂₀ ↑F ∈ S

Tactic:
refine Finset.induction_on F (fun _ => ?_) ?_

Result:
case refine_1
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
x✝ : ↑∅ ⊆ S
⊢ ⋂₀ ↑∅ ∈ S

case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ∀ ⦃a : Set α⦄ {s : Finset (Set α)}, a ∉ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S

Proof state:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ a ∩ ⋂₀ ↑s ∈ S

Tactic:
exact
  cond.inter_mem (h2 (Finset.mem_insert_self a s))
    (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

Result:
no goals

Proof state:
case refine_1
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
x✝ : ↑∅ ⊆ S
⊢ ⋂₀ ↑∅ ∈ S

Tactic:
simp [cond.univ_mem]

Result:
no goals
-- Mathlib/Analysis/Convex/StrictConvexBetween.lean
lemma eq_lineMap_of_dist_eq_mul_of_dist_eq_mul (hxy : dist x y = r * dist x z)
    (hyz : dist y z = (1 - r) * dist x z) : y = AffineMap.lineMap x z r

Proof state:
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
this : y -ᵥ x ∈ [0-[ℝ]z -ᵥ x]
⊢ y = (AffineMap.lineMap x z) r

Tactic:
obtain rfl | hne := eq_or_ne x z

Result:
case inl
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y : PE
hxy : dist x y = r * dist x x
hyz : dist y x = (1 - r) * dist x x
this : y -ᵥ x ∈ [0-[ℝ]x -ᵥ x]
⊢ y = (AffineMap.lineMap x x) r

case inr
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
this : y -ᵥ x ∈ [0-[ℝ]z -ᵥ x]
hne : x ≠ z
⊢ y = (AffineMap.lineMap x z) r
-- Mathlib/Analysis/PSeries.lean
theorem summable_one_div_rpow {p : ℝ} :
    Summable (fun n => 1 / (n : ℝ≥0) ^ p : ℕ → ℝ≥0) ↔ 1 < p

Proof state:
p : ℝ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem absorbs_iff_eventually_nhds_zero (h₀ : 0 ∈ s) :
    Absorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝 0, MapsTo (c • ·) t s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
⊢ MapsTo (fun x => 0 • x) t s

Tactic:
intro x _

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
x : E
a✝ : x ∈ t
⊢ (fun x => 0 • x) x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝 0, MapsTo (fun x => c • x) t s

Tactic:
rw [← nhdsWithin_compl_singleton_sup_pure, Filter.eventually_sup, Filter.eventually_pure,
  ← absorbs_iff_eventually_nhdsWithin_zero, and_iff_left]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
⊢ MapsTo (fun x => 0 • x) t s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
x : E
a✝ : x ∈ t
⊢ (fun x => 0 • x) x ∈ s

Tactic:
simpa only [zero_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_or_self : ∀ (x : Bool), (!x || x) = true

Proof state:
⊢ ∀ (x : Bool), (!x || x) = true

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem card_nthRoots (n : ℕ) (a : R) : Multiset.card (nthRoots n a) ≤ n

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : X ^ n - C a = 0
⊢ (nthRoots n a).card ≤ n

Tactic:
simp [Nat.zero_le, nthRoots, roots, h, dif_pos rfl, empty_eq_zero, Multiset.card_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ (nthRoots n a).card ≤ n

Tactic:
rw [← Nat.cast_le (α := WithBot ℕ)]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(nthRoots n a).card ≤ ↑n

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - C a = 0
⊢ (X ^ n - C a).degree ≤ ↑n

Tactic:
rw [hn, pow_zero, ← C_1, ← RingHom.map_sub]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - C a = 0
⊢ (C (1 - a)).degree ≤ ↑0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(nthRoots n a).card ≤ ↑n

Tactic:
rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(nthRoots n a).card ≤ (X ^ n - C a).degree

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
⊢ (nthRoots n a).card ≤ n

Tactic:
exact
(if hn : n = 0 then
if h : (X : R[X]) ^ n - C a = 0 then by
simp [Nat.zero_le, nthRoots, roots, h, dif_pos rfl, empty_eq_zero, Multiset.card_zero]
else
WithBot.coe_le_coe.1
(le_trans (card_roots h)
(by
rw [hn, pow_zero, ← C_1, ← RingHom.map_sub]
exact degree_C_le))
else by
rw [← Nat.cast_le (α := WithBot ℕ)]
rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
⊢ (nthRoots n a).card ≤ n

Tactic:
classical exact
(if hn : n = 0 then
  if h : (X : R[X]) ^ n - C a = 0 then by
    simp [Nat.zero_le, nthRoots, roots, h, dif_pos rfl, empty_eq_zero, Multiset.card_zero]
  else
    WithBot.coe_le_coe.1
      (le_trans (card_roots h)
        (by
          rw [hn, pow_zero, ← C_1, ← RingHom.map_sub]
          exact degree_C_le))
else by
  rw [← Nat.cast_le (α := WithBot ℕ)]
  rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
  exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : ¬X ^ n - C a = 0
⊢ (C (1 - a)).degree ≤ ↑0

Tactic:
exact degree_C_le

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ ↑(nthRoots n a).card ≤ (X ^ n - C a).degree

Tactic:
exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a)

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem isUnit_toStalk (x : PrimeSpectrum.Top R) (f : x.asIdeal.primeCompl) :
    IsUnit (toStalk R x (f : R))

Proof state:
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : ↥x.asIdeal.primeCompl
⊢ IsUnit ((ConcreteCategory.hom (toStalk R x)) ↑f)

Tactic:
rw [← germ_toOpen R (PrimeSpectrum.basicOpen (f : R)) x f.2 (f : R)]

Result:
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : ↥x.asIdeal.primeCompl
⊢ IsUnit
    ((ConcreteCategory.hom ((structureSheaf R).presheaf.germ (PrimeSpectrum.basicOpen ↑f) x ⋯))
      ((ConcreteCategory.hom (toOpen R (PrimeSpectrum.basicOpen ↑f))) ↑f))

Proof state:
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : ↥x.asIdeal.primeCompl
⊢ IsUnit
    ((ConcreteCategory.hom ((structureSheaf R).presheaf.germ (PrimeSpectrum.basicOpen ↑f) x ⋯))
      ((ConcreteCategory.hom (toOpen R (PrimeSpectrum.basicOpen ↑f))) ↑f))

Tactic:
exact RingHom.isUnit_map _ (isUnit_to_basicOpen_self R f)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem exists_infinite_fiber {β α : Type u} (f : β → α) (w : #α < #β) (w' : Infinite α) :
    ∃ a : α, Infinite (f ⁻¹' {a})

Proof state:
case intro
β α : Type u
f : β → α
w : #α < #β
w' : ℵ₀ ≤ #α
a : α
ha : #α < #↑(f ⁻¹' {a})
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})

Tactic:
exact ⟨a, w'.trans ha.le⟩

Result:
no goals

Proof state:
β α : Type u
f : β → α
w : #α < #β
w' : Infinite α
⊢ ∃ a, Infinite ↑(f ⁻¹' {a})

Tactic:
simp_rw [Cardinal.infinite_iff] at w' ⊢

Result:
β α : Type u
f : β → α
w : #α < #β
w' : ℵ₀ ≤ #α
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})

Proof state:
β α : Type u
f : β → α
w : #α < #β
w' : ℵ₀ ≤ #α
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f w w'

Result:
case intro
β α : Type u
f : β → α
w : #α < #β
w' : ℵ₀ ≤ #α
a : α
ha : #α < #↑(f ⁻¹' {a})
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})
-- Mathlib/Analysis/Convolution.lean
theorem ConvolutionExistsAt.integrable_swap (h : ConvolutionExistsAt f g x L μ) :
    Integrable (fun t => L (f (x - t)) (g t)) μ

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 E'
inst✝⁶ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd G
inst✝ : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
⊢ Integrable (fun t => (L (f (x - t))) (g t)) μ

Tactic:
convert h.comp_sub_left x

Result:
case h.e'_6.h.h.e'_6.h.e'_1
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 E'
inst✝⁶ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd G
inst✝ : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
x✝ : G
⊢ x✝ = x - (x - x✝)

Proof state:
case h.e'_6.h.h.e'_6.h.e'_1
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 E'
inst✝⁶ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd G
inst✝ : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
x✝ : G
⊢ x✝ = x - (x - x✝)

Tactic:
simp_rw [sub_sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.contains_eq [BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) {a : α} :
    l₁.contains a = l₂.contains a

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
h : l₁ ~ l₂
a : α
⊢ l₁.contains a = l₂.contains a

Tactic:
induction h with
| nil => rfl
| cons => simp_all
| swap => simp only [contains_cons, ← Bool.or_assoc, Bool.or_comm]
| trans => simp_all

Result:
no goals

Proof state:
case trans
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
a : α
l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : l₁✝.contains a = l₂✝.contains a
a_ih✝ : l₂✝.contains a = l₃✝.contains a
⊢ l₁✝.contains a = l₃✝.contains a

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
a : α
⊢ [].contains a = [].contains a

Tactic:
rfl

Result:
no goals

Proof state:
case swap
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
a x✝ y✝ : α
l✝ : List α
⊢ (y✝ :: x✝ :: l✝).contains a = (x✝ :: y✝ :: l✝).contains a

Tactic:
simp only [contains_cons, ← Bool.or_assoc, Bool.or_comm]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
a x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : l₁✝.contains a = l₂✝.contains a
⊢ (x✝ :: l₁✝).contains a = (x✝ :: l₂✝).contains a

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem udiv_one {x : BitVec w} : x / 1#w = x

Proof state:
w : Nat
x : BitVec w
⊢ x.toNat / (1 % 2 ^ w) = x.toNat

Tactic:
cases w

Result:
case zero
x : BitVec 0
⊢ x.toNat / (1 % 2 ^ 0) = x.toNat

case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ x.toNat / (1 % 2 ^ (n✝ + 1)) = x.toNat

Proof state:
case zero
x : BitVec 0
⊢ x.toNat / (1 % 2 ^ 0) = x.toNat

Tactic:
simp [eq_nil x]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x / 1#w = x

Tactic:
simp only [udiv_eq, toNat_eq, toNat_udiv, toNat_ofNat]

Result:
w : Nat
x : BitVec w
⊢ x.toNat / (1 % 2 ^ w) = x.toNat

Proof state:
case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ x.toNat / (1 % 2 ^ (n✝ + 1)) = x.toNat

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma coeff_preΨ₄ : W.preΨ₄.coeff 6 = 2

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
            C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
          C (W.b₄ * W.b₈ - W.b₆ ^ 2)).coeff
      6 =
    2

Tactic:
compute_degree!

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.preΨ₄.coeff 6 = 2

Tactic:
rw [preΨ₄]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
            C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
          C (W.b₄ * W.b₈ - W.b₆ ^ 2)).coeff
      6 =
    2
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
@[simp] lemma eval_charpolyRev :
    eval 0 M.charpolyRev = 1

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ((evalRingHom 0).mapMatrix (1 - X • M.map ⇑C)).det = det 1

Tactic:
have : (1 - (X : R[X]) • M.map C).map (eval 0) = 1 := by
  ext i j; rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
this : (1 - X • M.map ⇑C).map (eval 0) = 1
⊢ ((evalRingHom 0).mapMatrix (1 - X • M.map ⇑C)).det = det 1

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ eval 0 M.charpolyRev = 1

Tactic:
rw [charpolyRev, ← coe_evalRingHom, RingHom.map_det, ← det_one (R := R) (n := n)]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ((evalRingHom 0).mapMatrix (1 - X • M.map ⇑C)).det = det 1

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 - X • M.map ⇑C).map (eval 0) = 1

Tactic:
ext i j

Result:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
this : (1 - X • M.map ⇑C).map (eval 0) = 1
⊢ ((evalRingHom 0).mapMatrix (1 - X • M.map ⇑C)).det = det 1

Tactic:
congr

Result:
no goals

Proof state:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j

Tactic:
rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_add_of_commute (A B : Matrix m m 𝔸) (h : Commute A B) :
    exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
⊢ exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B

Tactic:
letI : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B

Tactic:
letI : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B

Tactic:
exact exp_add_of_commute h

Result:
no goals

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B

Tactic:
letI : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A B : Matrix m m 𝔸
h : Commute A B
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B