harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem self_le_basicOpen_union_iff (s : Set Γ(X, U)) :
    (U ≤ ⨆ f : s, X.basicOpen f.1) ↔ Ideal.span s = ⊤

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
⊢ ⨆ f, X.basicOpen ↑f ≤ U

Tactic:
simp only [iSup_le_iff, SetCoe.forall]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
⊢ ∀ x ∈ s, X.basicOpen x ≤ U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
⊢ ∀ x ∈ s, X.basicOpen x ≤ U

Tactic:
intro x _

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ X.basicOpen x ≤ U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ U = ⨆ f, X.basicOpen ↑f

Tactic:
refine ⟨fun h => le_antisymm h ?_, le_of_eq⟩

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
⊢ ⨆ f, X.basicOpen ↑f ≤ U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ Ideal.span s = ⊤

Tactic:
rw [← hU.basicOpen_union_eq_self_iff, @comm _ Eq]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ U = ⨆ f, X.basicOpen ↑f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ X.basicOpen x ≤ U

Tactic:
exact X.basicOpen_le x

Result:
no goals
-- Mathlib/Algebra/Group/NatPowAssoc.lean
theorem npow_mul (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ m) ^ n

Proof state:
case succ
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)

Tactic:
rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]

Result:
no goals

Proof state:
case zero
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m : ℕ
⊢ x ^ (m * 0) = (x ^ m) ^ 0

Tactic:
rw [npow_zero, Nat.mul_zero, npow_zero]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (m * n) = (x ^ m) ^ n

Tactic:
induction n with
| zero => rw [npow_zero, Nat.mul_zero, npow_zero]
| succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π (i : I) :
    (coyonedaOpColimitIsoLimitCoyoneda F).inv ≫ coyoneda.map (colimit.ι F i).op =
      limit.π (F.op.comp coyoneda) ⟨i⟩

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).inv ≫ coyoneda.map (colimit.ι F i).op = limit.π (F.op ⋙ coyoneda) (op i)

Tactic:
rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
  Iso.inv_hom_id, Category.id_comp]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem unbounded_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto f atTop atTop) :
    ¬BddAbove (range f)

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f atTop atTop
⊢ ¬BddAbove (range f)

Tactic:
rintro ⟨M, hM⟩

Result:
case intro
α : Type u_3
β : Type u_4
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ False

Proof state:
case intro
α : Type u_3
β : Type u_4
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ False

Tactic:
obtain ⟨a, ha⟩ := mem_atTop_sets.mp (h <| Ioi_mem_atTop M)

Result:
case intro.intro
α : Type u_3
β : Type u_4
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ b ≥ a, b ∈ f ⁻¹' Ioi M
⊢ False

Proof state:
case intro.intro
α : Type u_3
β : Type u_4
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ b ≥ a, b ∈ f ⁻¹' Ioi M
⊢ False

Tactic:
apply lt_irrefl M

Result:
case intro.intro
α : Type u_3
β : Type u_4
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ b ≥ a, b ∈ f ⁻¹' Ioi M
⊢ M < M

Proof state:
case intro.intro
α : Type u_3
β : Type u_4
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ b ≥ a, b ∈ f ⁻¹' Ioi M
⊢ M < M

Tactic:
calc
  M < f a := ha a le_rfl
  _ ≤ M := hM (Set.mem_range_self a)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem enum_zero_le {r : α → α → Prop} [IsWellOrder α r] (h0 : 0 < type r) (a : α) :
    ¬r a (enum r ⟨0, h0⟩)

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ⟨0, h0⟩ ≤ ⟨(typein r).toRelEmbedding a, ⋯⟩

Tactic:
apply Ordinal.zero_le

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ¬r a ((enum r) ⟨0, h0⟩)

Tactic:
rw [← enum_typein r a, enum_le_enum r]

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ⟨0, h0⟩ ≤ ⟨(typein r).toRelEmbedding a, ⋯⟩
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem hasMFDerivWithinAt_diff_singleton (y : M) :
    HasMFDerivWithinAt I I' f (s \ {y}) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Proof state:
𝕜 : 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'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
⊢ HasMFDerivWithinAt I I' f (s \ {y}) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Tactic:
rw [← hasMFDerivWithinAt_insert, insert_diff_singleton, hasMFDerivWithinAt_insert]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem zpow_add {x : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (m n : ℤ) :
    x ^ (m + n) = x ^ m * x ^ n

Proof state:
case intro
m n : ℤ
x : ℝ≥0
hx : x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n

Tactic:
simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]

Result:
no goals

Proof state:
x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ⊤
m n : ℤ
⊢ x ^ (m + n) = x ^ m * x ^ n

Tactic:
lift x to ℝ≥0 using h'x

Result:
case intro
m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n

Proof state:
case intro
m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n

Tactic:
replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx

Result:
case intro
m n : ℤ
x : ℝ≥0
hx : x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n

Proof state:
m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ x ≠ 0

Tactic:
simpa only [Ne, coe_eq_zero] using hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toVector_inj {a b : Array α} (h₁ : a.size = b.size) (h₂ : a.toVector.cast h₁ = b.toVector) : a = b

Proof state:
case h₂
α : Type u_1
a b : Array α
h₁ : a.size = b.size
h₂ : Vector.cast h₁ a.toVector = b.toVector
i : Nat
ih₁ : i < a.size
ih₂ : i < b.size
⊢ a[i] = b[i]

Tactic:
simpa using congrArg (fun a => a[i]) h₂

Result:
no goals

Proof state:
case h₁
α : Type u_1
a b : Array α
h₁ : a.size = b.size
h₂ : Vector.cast h₁ a.toVector = b.toVector
⊢ a.size = b.size

Tactic:
exact h₁

Result:
no goals

Proof state:
α : Type u_1
a b : Array α
h₁ : a.size = b.size
h₂ : Vector.cast h₁ a.toVector = b.toVector
⊢ a = b

Tactic:
ext i ih₁ ih₂

Result:
case h₁
α : Type u_1
a b : Array α
h₁ : a.size = b.size
h₂ : Vector.cast h₁ a.toVector = b.toVector
⊢ a.size = b.size

case h₂
α : Type u_1
a b : Array α
h₁ : a.size = b.size
h₂ : Vector.cast h₁ a.toVector = b.toVector
i : Nat
ih₁ : i < a.size
ih₂ : i < b.size
⊢ a[i] = b[i]
-- Mathlib/Algebra/Homology/Localization.lean
lemma ComplexShape.QFactorsThroughHomotopy_of_exists_prev [CategoryWithHomology C] :
    c.QFactorsThroughHomotopy C where
  areEqualizedByLocalization {K L f g} h

Proof state:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
⊢ AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

Tactic:
have : DecidableRel c.Rel := by classical infer_instance

Result:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
this : DecidableRel c.Rel
⊢ AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

Proof state:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
⊢ DecidableRel c.Rel

Tactic:
infer_instance

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
this : DecidableRel c.Rel
⊢ AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g

Tactic:
exact h.map_eq_of_inverts_homotopyEquivalences hc _
  (MorphismProperty.IsInvertedBy.of_le _ _ _
    (Localization.inverts _ (HomologicalComplex.quasiIso C _))
    (homotopyEquivalences_le_quasiIso C _))

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
⊢ DecidableRel c.Rel

Tactic:
classical infer_instance

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem toSesqForm_apply_norm_le {f : E →L[𝕜] E'} {v : E'} : ‖toSesqForm f v‖ ≤ ‖f‖ * ‖v‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, f x⟫_𝕜‖ ≤ ‖v‖ * ‖f x‖
⊢ ‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖

Tactic:
calc
  ‖⟪v, f x⟫‖ ≤ ‖v‖ * ‖f x‖ := h₂
  _ ≤ ‖v‖ * (‖f‖ * ‖x‖) := mul_le_mul_of_nonneg_left h₁ (norm_nonneg v)
  _ = ‖f‖ * ‖v‖ * ‖x‖ := by ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖
⊢ ‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖

Tactic:
have h₂ := @norm_inner_le_norm 𝕜 E' _ _ _ v (f x)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, f x⟫_𝕜‖ ≤ ‖v‖ * ‖f x‖
⊢ ‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, f x⟫_𝕜‖ ≤ ‖v‖ * ‖f x‖
⊢ ‖v‖ * (‖f‖ * ‖x‖) = ‖f‖ * ‖v‖ * ‖x‖

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
⊢ 0 ≤ ‖f‖ * ‖v‖

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
⊢ ‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖

Tactic:
have h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖
⊢ ‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
⊢ ‖(toSesqForm f) v‖ ≤ ‖f‖ * ‖v‖

Tactic:
refine opNorm_le_bound _ (by positivity) fun x ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
⊢ ‖((toSesqForm f) v) x‖ ≤ ‖f‖ * ‖v‖ * ‖x‖
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem J_transpose : (J l R)ᵀ = -J l R

Proof state:
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)

Tactic:
simp [fromBlocks]

Result:
no goals

Proof state:
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ (J l R)ᵀ = -J l R

Tactic:
rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R),
  fromBlocks_smul, Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]

Result:
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_eq_some_iff {o : Option α} {x : {x // x ∈ o}} :
    o.attach = some x ↔ o = some x.val

Proof state:
α : Type u_1
o : Option α
x : { x // x ∈ o }
⊢ o.attach = some x ↔ o = some x.val

Tactic:
cases o <;> cases x <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
lemma coxeterWeightIn_eq_zero_iff :
    P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
h : P.coxeterWeightIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0

Tactic:
have : Fintype ι := Fintype.ofFinite ι

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
h : P.coxeterWeightIn ℤ i j = 0
this : Fintype ι
⊢ P.pairingIn ℤ i j = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
h : P.coxeterWeightIn ℤ i j = 0
this : Fintype ι
⊢ P.pairingIn ℤ i j = 0

Tactic:
rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
  P.coxeterWeight_zero_iff_isOrthogonal (P.posRootForm ℤ), IsOrthogonal,
  P.pairing_zero_iff (P.posRootForm ℤ) j i, and_self, ← P.algebraMap_pairingIn ℤ,
  FaithfulSMul.algebraMap_eq_zero_iff] at h

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
⊢ P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [coxeterWeightIn, h, zero_mul]⟩

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
h : P.coxeterWeightIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
h : P.pairingIn ℤ i j = 0
⊢ P.coxeterWeightIn ℤ i j = 0

Tactic:
rw [coxeterWeightIn, h, zero_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Presentable/Basic.lean
@[simp]
lemma isCardinalPresentable_iff_of_isEquivalence
    {C' : Type u₃} [Category.{v₃} C'] (F : C ⥤ C')
    [F.IsEquivalence] :
    IsCardinalPresentable (F.obj X) κ ↔ IsCardinalPresentable X κ

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable (F.obj X) κ ↔ IsCardinalPresentable X κ

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable (F.obj X) κ → IsCardinalPresentable X κ

case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable X κ → IsCardinalPresentable (F.obj X) κ

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable (F.obj X) κ → IsCardinalPresentable X κ

Tactic:
intro

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
a✝ : IsCardinalPresentable (F.obj X) κ
⊢ IsCardinalPresentable X κ

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
a✝ : IsCardinalPresentable X κ
⊢ IsCardinalPresentable (F.obj X) κ

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
a✝ : IsCardinalPresentable (F.obj X) κ
⊢ IsCardinalPresentable X κ

Tactic:
exact isCardinalPresentable_of_iso
  (show F.inv.obj (F.obj X) ≅ X from F.asEquivalence.unitIso.symm.app X :) κ

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable X κ → IsCardinalPresentable (F.obj X) κ

Tactic:
intro

Result:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
a✝ : IsCardinalPresentable X κ
⊢ IsCardinalPresentable (F.obj X) κ
-- Mathlib/RingTheory/Multiplicity.lean
theorem Nat.finiteMultiplicity_iff {a b : ℕ} : FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b

Proof state:
a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
cases h <;> simp [*]

Result:
no goals

Proof state:
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0

Tactic:
exact
  ⟨fun h =>
    or_iff_not_imp_right.2 fun hb =>
      have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1
      Classical.by_contradiction fun ha1 : a ≠ 1 =>
        have ha_gt_one : 1 < a :=
          lt_of_not_ge fun _ =>
            match a with
            | 0 => ha rfl
            | 1 => ha1 rfl
            | b+2 => by omega
        not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (b.lt_pow_self ha_gt_one),
    fun h => by cases h <;> simp [*]⟩

Result:
no goals

Proof state:
a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
rw [ha] at h

Result:
a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Proof state:
a b : ℕ
⊢ FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b

Tactic:
rw [← not_iff_not, FiniteMultiplicity.not_iff_forall, not_and_or, not_ne_iff, not_lt,
  Nat.le_zero]

Result:
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0

Proof state:
a b✝ : ℕ
hb : ¬b✝ = 0
b : ℕ
h : ∀ (n : ℕ), (b + 2) ^ n ∣ b✝
ha : b + 2 ≠ 0
ha1 : b + 2 ≠ 1
x✝ : 1 ≥ b + 2
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
exact h 1

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem rank_adjoin_simple_eq_one_iff :
    Module.rank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ {α} ⊆ ↑⊥ ↔ α ∈ ⊥

Tactic:
exact Set.singleton_subset_iff

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ Module.rank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

Tactic:
rw [rank_adjoin_eq_one_iff]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ {α} ⊆ ↑⊥ ↔ α ∈ ⊥
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
lemma inertiaDeg_map_eq [p.IsMaximal] (P : Ideal S)
    {E : Type*} [EquivLike E S S₁] [AlgEquivClass E R S S₁] (e : E) :
    inertiaDeg p (P.map e) = inertiaDeg p P

Proof state:
R : Type u
inst✝⁷ : CommRing R
S : Type v
inst✝⁶ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝⁵ : CommRing S₁
inst✝⁴ : Algebra R S₁
inst✝³ : Algebra R S
inst✝² : p.IsMaximal
P : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
e : E
⊢ p.inertiaDeg (comap (↑e).symm P) = p.inertiaDeg P

Tactic:
exact p.inertiaDeg_comap_eq (e : S ≃ₐ[R] S₁).symm P

Result:
no goals

Proof state:
R : Type u
inst✝⁷ : CommRing R
S : Type v
inst✝⁶ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝⁵ : CommRing S₁
inst✝⁴ : Algebra R S₁
inst✝³ : Algebra R S
inst✝² : p.IsMaximal
P : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
e : E
⊢ p.inertiaDeg (map e P) = p.inertiaDeg P

Tactic:
rw [show P.map e = _ from map_comap_of_equiv (e : S ≃+* S₁)]

Result:
R : Type u
inst✝⁷ : CommRing R
S : Type v
inst✝⁶ : CommRing S
p : Ideal R
S₁ : Type u_1
inst✝⁵ : CommRing S₁
inst✝⁴ : Algebra R S₁
inst✝³ : Algebra R S
inst✝² : p.IsMaximal
P : Ideal S
E : Type u_2
inst✝¹ : EquivLike E S S₁
inst✝ : AlgEquivClass E R S S₁
e : E
⊢ p.inertiaDeg (comap (↑e).symm P) = p.inertiaDeg P