harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/GradedModule.lean
theorem of_smul_of [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
    {i j} (x : A i) (y : M j) :
    DirectSum.of A i x • of M j y = of M (i +ᵥ j) (GSMul.smul x y)

Proof state:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
i : ιA
j : ιB
x : A i
y : M j
⊢ (of A i) x • (of M j) y = (of M (i +ᵥ j)) (GSMul.smul x y)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_transpose (A : Matrix m m 𝔸) : exp 𝕂 Aᵀ = (exp 𝕂 A)ᵀ

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq m
inst✝⁵ : Field 𝕂
inst✝⁴ : CommRing 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra 𝕂 𝔸
inst✝ : T2Space 𝔸
A : Matrix m m 𝔸
⊢ exp 𝕂 Aᵀ = (exp 𝕂 A)ᵀ

Tactic:
simp_rw [exp_eq_tsum, transpose_tsum, transpose_smul, transpose_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
    getKey! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then k else getKey! m a

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ m.contains k = false then k else m.getKey! a

Tactic:
exact Raw₀.getKey!_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ ¬k ∈ m then k else m.getKey! a

Tactic:
simp [mem_iff_contains, contains_insertIfNew]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ m.contains k = false then k else m.getKey! a
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean
lemma prod_pos {s : List R} (h : ∀ a ∈ s, 0 < a) : 0 < s.prod

Proof state:
case nil
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
h : ∀ (a : R), a ∈ [] → 0 < a
⊢ 0 < [].prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a : R
s : List R
hind : (∀ (a : R), a ∈ s → 0 < a) → 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
⊢ 0 < (a :: s).prod

Tactic:
simp only [prod_cons]

Result:
case cons
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a : R
s : List R
hind : (∀ (a : R), a ∈ s → 0 < a) → 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
⊢ 0 < a * s.prod

Proof state:
case cons
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a : R
s : List R
hind : (∀ (a : R), a ∈ s → 0 < a) → 0 < s.prod
h : 0 < a ∧ ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < a * s.prod

Tactic:
exact mul_pos h.1 (hind h.2)

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a : R
s : List R
hind : (∀ (a : R), a ∈ s → 0 < a) → 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
⊢ 0 < a * s.prod

Tactic:
simp only [mem_cons, forall_eq_or_imp] at h

Result:
case cons
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a : R
s : List R
hind : (∀ (a : R), a ∈ s → 0 < a) → 0 < s.prod
h : 0 < a ∧ ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < a * s.prod

Proof state:
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
s : List R
h : ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < s.prod

Tactic:
induction s with
| nil => simp
| cons a s hind =>
  simp only [prod_cons]
  simp only [mem_cons, forall_eq_or_imp] at h
  exact mul_pos h.1 (hind h.2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_map {l : List α} (f : α → β) :
    (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ (map f l).attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      l.attach

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_iff_contDiffAt (h : s ∈ 𝓝 x) :
    ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
h : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [← univ_inter s, contDiffWithinAt_inter h, contDiffWithinAt_univ]

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem linearMapAt_symmₗ (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet) (y : F) : e.linearMapAt R b (e.symmₗ R b y) = y

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
y : F
⊢ ↑(linearEquivAt R e b hb) ((Pretrivialization.symmₗ R e b) y) = y

Tactic:
exact (e.linearEquivAt R b hb).right_inv y

Result:
no goals

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
y : F
⊢ (Pretrivialization.linearMapAt R e b) ((Pretrivialization.symmₗ R e b) y) = y

Tactic:
rw [e.linearMapAt_def_of_mem hb]

Result:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
y : F
⊢ ↑(linearEquivAt R e b hb) ((Pretrivialization.symmₗ R e b) y) = y
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem aeval_algHom (f : B →ₐ[A] B') (x : B) : (Polynomial.aeval (f x)) (minpoly A x) = 0

Proof state:
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
x : B
⊢ (Polynomial.aeval (f x)) (minpoly A x) = 0

Tactic:
rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
/-- A space is locally path-connected iff all path components of open subsets are open. -/
lemma locPathConnectedSpace_iff_isOpen_pathComponentIn {X : Type*} [TopologicalSpace X] :
    LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u) :=
  ⟨fun _ _ _ hu ↦ hu.pathComponentIn _, fun h ↦ ⟨fun x ↦ ⟨fun s ↦ by
    refine ⟨fun hs ↦ ?_, fun ⟨_, ht⟩ ↦ Filter.mem_of_superset ht.1.1 ht.2⟩
    let ⟨u, hu⟩ := mem_nhds_iff.mp hs
    exact ⟨pathComponentIn x u, ⟨(h x u hu.2.1).mem_nhds (mem_pathComponentIn_self hu.2.2),
      isPathConnected_pathComponentIn hu.2.2⟩, pathComponentIn_subset.trans hu.1⟩⟩⟩⟩

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)
x : X
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
refine ⟨fun hs ↦ ?_, fun ⟨_, ht⟩ ↦ Filter.mem_of_superset ht.1.1 ht.2⟩

Result:
X : Type u_4
inst✝ : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)
x : X
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hu : u ⊆ s ∧ IsOpen u ∧ x ∈ u
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
exact ⟨pathComponentIn x u, ⟨(h x u hu.2.1).mem_nhds (mem_pathComponentIn_self hu.2.2),
  isPathConnected_pathComponentIn hu.2.2⟩, pathComponentIn_subset.trans hu.1⟩

Result:
no goals

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let ⟨u, hu⟩ := mem_nhds_iff.mp hs

Result:
X : Type u_4
inst✝ : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)
x : X
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hu : u ⊆ s ∧ IsOpen u ∧ x ∈ u
⊢ ∃ i, (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem forall_of_forall_mem_closedBall (p : α → Prop) (x : α)
    (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ closedBall x R, p y) (y : α) : p y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
⊢ p y

Tactic:
obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z :=
  frequently_iff.1 H (Ici_mem_atTop (dist y x))

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
R : ℝ
hR : R ≥ dist y x
h : ∀ z ∈ closedBall x R, p z
⊢ p y

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
R : ℝ
hR : R ≥ dist y x
h : ∀ z ∈ closedBall x R, p z
⊢ p y

Tactic:
exact h _ hR

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
    as.contains a = decide (a ∈ as)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : List α
⊢ as.contains a = decide (a ∈ as)

Tactic:
rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_succ_of_some {f : Fin (n+1) → Option α} (h : f 0 = some x) :
    findSome? f = some x

Proof state:
n : Nat
α : Type u_1
x : α
f : Fin (n + 1) → Option α
h : f 0 = some x
⊢ findSome? f = some x

Tactic:
simp [findSome?_succ, h]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normalClosure_def' : normalClosure F K L = ⨆ f : L →ₐ[F] L, K.map f

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
⊢ normalClosure F (↥K) L = ⨆ f, map f K

Tactic:
refine (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))

Result:
case refine_1
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : ↥K →ₐ[F] L
⊢ f.fieldRange ≤ ⨆ f, map f K

case refine_2
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ f, f.fieldRange

Proof state:
case refine_1
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : ↥K →ₐ[F] L
⊢ f.fieldRange ≤ ⨆ f, map f K

Tactic:
exact le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)

Result:
no goals

Proof state:
case refine_2
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ f, f.fieldRange

Tactic:
exact le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
@[simp]
lemma lie_lie : ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

Proof state:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x y : L
m : M
⊢ ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

Tactic:
rw [leibniz_lie, add_sub_cancel_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_six : cos (π / 6) = √3 / 2

Proof state:
⊢ cos (π / 6) = √3 / 2

Tactic:
rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
  ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self] <;> linarith [pi_pos]

Result:
no goals

Proof state:
⊢ 6 = 3 * 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) :
    (lift S g h).comp (mkLinearMap S M) = g

Proof state:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
x : M
⊢ (lift S g h ∘ₗ mkLinearMap S M) x = g x

Tactic:
simp [LocalizedModule.lift_mk]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
⊢ lift S g h ∘ₗ mkLinearMap S M = g

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
x : M
⊢ (lift S g h ∘ₗ mkLinearMap S M) x = g x
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_div_div_le (a₁ a₂ b₁ b₂ : E) : dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
simpa only [div_eq_mul_inv, dist_inv_inv] using dist_mul_mul_le a₁ a₂⁻¹ b₁ b₂⁻¹

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.squarefree_span_singleton {a : R} :
    Squarefree (span {a}) ↔ Squarefree a

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
⊢ Squarefree (span {a}) ↔ Squarefree a

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h I hI ↦ ?_⟩

Result:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : x * x ∣ a
⊢ IsUnit x

case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : I * I ∣ span {a}
⊢ IsUnit I

Proof state:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : Submodule.IsPrincipal.generator I * Submodule.IsPrincipal.generator I ∣ a
⊢ IsUnit I

Tactic:
exact isUnit_iff.mpr <| eq_top_of_isUnit_mem _ (Submodule.IsPrincipal.generator_mem I) (h _ hI)

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : x * x ∣ a
⊢ IsUnit x

Tactic:
rw [← span_singleton_dvd_span_singleton_iff_dvd, ← span_singleton_mul_span_singleton] at hx

Result:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : span {x} * span {x} ∣ span {a}
⊢ IsUnit x

Proof state:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : I * I ∣ span {a}
⊢ IsUnit I

Tactic:
rw [← span_singleton_generator I, span_singleton_mul_span_singleton,
  span_singleton_dvd_span_singleton_iff_dvd] at hI

Result:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : Submodule.IsPrincipal.generator I * Submodule.IsPrincipal.generator I ∣ a
⊢ IsUnit I

Proof state:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : span {x} * span {x} ∣ span {a}
⊢ IsUnit x

Tactic:
simpa using h _ hx

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_ite_eq (b : β) [DecidablePred (· = b)] (a : α) :
    HasProd (fun b' ↦ if b' = b then a else 1) a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ HasProd (fun b' => if b' = b then a else 1) a

Tactic:
convert @hasProd_single _ _ _ _ (fun b' ↦ if b' = b then a else 1) b (fun b' hb' ↦ if_neg hb')

Result:
case h.e'_6
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ a = if b = b then a else 1

Proof state:
case h.e'_6
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
b : β
inst✝ : DecidablePred fun x => x = b
a : α
⊢ a = if b = b then a else 1

Tactic:
exact (if_pos rfl).symm

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_opow {b : Ordinal} (hb : 1 < b) (x : Ordinal) : log b (b ^ x) = x

Proof state:
case h.e'_2
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = log b (b ^ x * 1)

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
case h.e'_3
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x = x + log b 1

Tactic:
rw [log_one_right, add_zero]

Result:
no goals

Proof state:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = x

Tactic:
convert log_opow_mul hb x zero_ne_one.symm using 1

Result:
case h.e'_2
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = log b (b ^ x * 1)

case h.e'_3
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x = x + log b 1
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Raised.dist_le {n m} (H : Raised n m) : Nat.dist n m ≤ 1

Proof state:
case intro
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1

Tactic:
rwa [Nat.dist_eq_sub_of_le H1, tsub_le_iff_left]

Result:
no goals

Proof state:
n m : ℕ
H : Raised n m
⊢ n.dist m ≤ 1

Tactic:
obtain ⟨H1, H2⟩ := raised_iff.1 H

Result:
case intro
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_rotateLeft {x : BitVec w} {r i : Nat}  :
    (x.rotateLeft r).getLsbD i =
      cond (i < r % w)
      (x.getLsbD (w - (r % w) + i))
      (decide (i < w) && x.getLsbD (i - (r % w)))

Proof state:
case zero
r i : Nat
x : BitVec 0
⊢ (x.rotateLeft r).getLsbD i =
    bif decide (i < r % 0) then x.getLsbD (0 - r % 0 + i) else decide (i < 0) && x.getLsbD (i - r % 0)

Tactic:
simp

Result:
no goals

Proof state:
r i n✝ : Nat
x : BitVec (n✝ + 1)
⊢ n✝ + 1 > 0

Tactic:
omega

Result:
no goals

Proof state:
case succ
r i n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (x.rotateLeft r).getLsbD i =
    bif decide (i < r % (n✝ + 1)) then x.getLsbD (n✝ + 1 - r % (n✝ + 1) + i)
    else decide (i < n✝ + 1) && x.getLsbD (i - r % (n✝ + 1))

Tactic:
rw [← rotateLeft_mod_eq_rotateLeft, getLsbD_rotateLeft_of_le (Nat.mod_lt _ (by omega))]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
⊢ (x.rotateLeft r).getLsbD i =
    bif decide (i < r % w) then x.getLsbD (w - r % w + i) else decide (i < w) && x.getLsbD (i - r % w)

Tactic:
rcases w with ⟨rfl, w⟩

Result:
case zero
r i : Nat
x : BitVec 0
⊢ (x.rotateLeft r).getLsbD i =
    bif decide (i < r % 0) then x.getLsbD (0 - r % 0 + i) else decide (i < 0) && x.getLsbD (i - r % 0)

case succ
r i n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (x.rotateLeft r).getLsbD i =
    bif decide (i < r % (n✝ + 1)) then x.getLsbD (n✝ + 1 - r % (n✝ + 1) + i)
    else decide (i < n✝ + 1) && x.getLsbD (i - r % (n✝ + 1))
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem thickening_closedBall (hε : 0 < ε) (hδ : 0 ≤ δ) (x : E) :
    thickening ε (closedBall x δ) = ball x (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
x : E
⊢ thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)

Tactic:
rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
theorem LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute [DecidableEq (n → 𝕜)]
    (hT : ∀ i, (T i).IsSymmetric) (hC : Pairwise (Commute on T)) :
    DirectSum.IsInternal (fun α : n → 𝕜 ↦ ⨅ j, eigenspace (T j) (α j))

Proof state:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ DirectSum.IsInternal fun α => ⨅ j, (T j).eigenspace (α j)

Tactic:
rw [OrthogonalFamily.isInternal_iff]

Result:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ (⨆ α, ⨅ j, (T j).eigenspace (α j))ᗮ = ⊥

𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (fun i => ↥(⨅ j, (T j).eigenspace (i j))) fun i => (⨅ j, (T j).eigenspace (i j)).subtypeₗᵢ

Proof state:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ (⨆ α, ⨅ j, (T j).eigenspace (α j))ᗮ = ⊥

Tactic:
rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (fun i => ↥(⨅ j, (T j).eigenspace (i j))) fun i => (⨅ j, (T j).eigenspace (i j)).subtypeₗᵢ

Tactic:
exact orthogonalFamily_iInf_eigenspaces hT

Result:
no goals