harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_fromBlocks₂₂ (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
    (D : Matrix n n α) [Invertible D] :
    (Matrix.fromBlocks A B C D).det = det D * det (A - B * ⅟ D * C)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)

Tactic:
ext (i j)

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
i j : m ⊕ n
⊢ fromBlocks A B C D i j = (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) i j

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
i j : m ⊕ n
⊢ fromBlocks A B C D i j = (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) i j

Tactic:
cases i <;> cases j <;> rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
this : fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)
⊢ (fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det

Tactic:
rw [this, det_submatrix_equiv_self, det_fromBlocks₁₁]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ (fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det

Tactic:
have : fromBlocks A B C D =
    (fromBlocks D C B A).submatrix (Equiv.sumComm _ _) (Equiv.sumComm _ _) := by
  ext (i j)
  cases i <;> cases j <;> rfl

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
this : fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)
⊢ (fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem precomp_uniformContinuous {f : γ → α} :
    UniformContinuous fun g : α →ᵤ β => ofFun (toFun g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β, ∀ x ∈ UniformFun.gen α β ia, (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f)) ∈ UniformFun.gen γ β ib

Tactic:
exact fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ UniformContinuous fun g => ofFun (toFun g ∘ f)

Tactic:
rw [UniformContinuous,
    (UniformFun.hasBasis_uniformity α β).tendsto_iff (UniformFun.hasBasis_uniformity γ β)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β, ∀ x ∈ UniformFun.gen α β ia, (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f)) ∈ UniformFun.gen γ β ib
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma expCoeff_rec (m : ℕ) :
    (expCoeff (2 * (m + 3)) =
      expCoeff (m + 2) ^ 2 * expCoeff (m + 3) * expCoeff (m + 5) -
        expCoeff (m + 1) * expCoeff (m + 3) * expCoeff (m + 4) ^ 2) ∧
    (expCoeff (2 * (m + 2) + 1) =
      expCoeff (m + 4) * expCoeff (m + 2) ^ 3 * (if Even m then 4 ^ 2 else 1) -
        expCoeff (m + 1) * expCoeff (m + 3) ^ 3 * (if Even m then 1 else 4 ^ 2))

Proof state:
m : ℕ
⊢ WeierstrassCurve.expCoeff (2 * (m + 3)) =
      WeierstrassCurve.expCoeff (m + 2) ^ 2 * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 5) -
        WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) * WeierstrassCurve.expCoeff (m + 4) ^ 2 ∧
    WeierstrassCurve.expCoeff (2 * (m + 2) + 1) =
      (WeierstrassCurve.expCoeff (m + 4) * WeierstrassCurve.expCoeff (m + 2) ^ 3 * if Even m then 4 ^ 2 else 1) -
        WeierstrassCurve.expCoeff (m + 1) * WeierstrassCurve.expCoeff (m + 3) ^ 3 * if Even m then 1 else 4 ^ 2

Tactic:
push_cast [← @Int.cast_inj ℚ, expCoeff_cast, even_two_mul, m.not_even_two_mul_add_one,
  Nat.even_add_one, ite_not]

Result:
m : ℕ
⊢ 2 * (↑m + 3) / 2 =
      (((if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 2 * if Even m then ↑m + 3 else (↑m + 3) / 2) *
          if Even m then ↑m + 5 else (↑m + 5) / 2) -
        ((if Even m then ↑m + 1 else (↑m + 1) / 2) * if Even m then ↑m + 3 else (↑m + 3) / 2) *
          (if Even m then (↑m + 4) / 2 else ↑m + 4) ^ 2 ∧
    2 * (↑m + 2) + 1 =
      ((if Even m then (↑m + 4) / 2 else ↑m + 4) * (if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 3 *
          if Even m then 16 else 1) -
        (if Even m then ↑m + 1 else (↑m + 1) / 2) * (if Even m then ↑m + 3 else (↑m + 3) / 2) ^ 3 *
          if Even m then 1 else 16

Proof state:
m : ℕ
⊢ 2 * (↑m + 3) / 2 =
      (((if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 2 * if Even m then ↑m + 3 else (↑m + 3) / 2) *
          if Even m then ↑m + 5 else (↑m + 5) / 2) -
        ((if Even m then ↑m + 1 else (↑m + 1) / 2) * if Even m then ↑m + 3 else (↑m + 3) / 2) *
          (if Even m then (↑m + 4) / 2 else ↑m + 4) ^ 2 ∧
    2 * (↑m + 2) + 1 =
      ((if Even m then (↑m + 4) / 2 else ↑m + 4) * (if Even m then (↑m + 2) / 2 else ↑m + 2) ^ 3 *
          if Even m then 16 else 1) -
        (if Even m then ↑m + 1 else (↑m + 1) / 2) * (if Even m then ↑m + 3 else (↑m + 3) / 2) ^ 3 *
          if Even m then 1 else 16

Tactic:
constructor <;> split_ifs <;> ring1

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma add_le_of_le_sub {a b c : EReal} (h : a ≤ b - c) : a + c ≤ b

Proof state:
a b c : EReal
h : a ≤ b - c
⊢ a + - -c ≤ b

Tactic:
exact sub_le_of_le_add h

Result:
no goals

Proof state:
a b c : EReal
h : a ≤ b - c
⊢ a + c ≤ b

Tactic:
rw [← neg_neg c]

Result:
a b c : EReal
h : a ≤ b - c
⊢ a + - -c ≤ b
-- Mathlib/Order/RelSeries.lean
@[simp] lemma last_append (p q : RelSeries r) (connect : r p.last q.head) :
    (p.append q connect).last = q.last

Proof state:
case h.e'_2.h.e'_4.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ ↑(Fin.last (p.append q connect).length) =
    (↑(Fin.natAdd p.length (Fin.last q.length)) % ((p.append q connect).length + 1) +
        1 % ((p.append q connect).length + 1)) %
      ((p.append q connect).length + 1)

Tactic:
simp only [append_length, Fin.val_last, Fin.natAdd_last, Nat.one_mod, Nat.mod_add_mod,
  Nat.mod_succ]

Result:
no goals

Proof state:
case h.e'_2.h.e'_4
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ Fin.last (p.append q connect).length = ↑↑(Fin.natAdd p.length (Fin.last q.length)) + 1

Tactic:
ext

Result:
case h.e'_2.h.e'_4.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ ↑(Fin.last (p.append q connect).length) = ↑(↑↑(Fin.natAdd p.length (Fin.last q.length)) + 1)

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ (p.append q connect).last = q.last

Tactic:
delta last

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ (p.append q connect).toFun (Fin.last (p.append q connect).length) = q.toFun (Fin.last q.length)

Proof state:
case h.e'_2.h.e'_4.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ ↑(Fin.last (p.append q connect).length) = ↑(↑↑(Fin.natAdd p.length (Fin.last q.length)) + 1)

Tactic:
change _ = _ % _

Result:
case h.e'_2.h.e'_4.h
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ ↑(Fin.last (p.append q connect).length) =
    (↑(Fin.natAdd p.length (Fin.last q.length)) % ((p.append q connect).length + 1) +
        1 % ((p.append q connect).length + 1)) %
      ((p.append q connect).length + 1)

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ (p.append q connect).toFun (Fin.last (p.append q connect).length) = q.toFun (Fin.last q.length)

Tactic:
convert append_apply_right p q connect (Fin.last _)

Result:
case h.e'_2.h.e'_4
α : Type u_1
r : Rel α α
p q : RelSeries r
connect : r p.last q.head
⊢ Fin.last (p.append q connect).length = ↑↑(Fin.natAdd p.length (Fin.last q.length)) + 1
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma klFun_one : klFun 1 = 0

Proof state:
⊢ klFun 1 = 0

Tactic:
simp [klFun]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem preservesColimit_of_comp {B : Type u₄} [Category.{v₄} B] {H : E ⥤ B}
    [PreservesColimit (F ⋙ G) H] : PreservesColimit G H where
  preserves {c} hc

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
refine ⟨isColimitWhiskerEquiv F _ ?_⟩

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
⊢ IsColimit (Cocone.whisker F (H.mapCocone c))

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) := isColimitOfPreserves H ((isColimitWhiskerEquiv F c).symm hc)
⊢ ∀ (j : C),
    (H.mapCocone (Cocone.whisker F c)).ι.app j ≫ (Iso.refl (H.mapCocone (Cocone.whisker F c)).pt).hom =
      (Cocone.whisker F (H.mapCocone c)).ι.app j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) := isColimitOfPreserves H ((isColimitWhiskerEquiv F c).symm hc)
⊢ IsColimit (Cocone.whisker F (H.mapCocone c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocones.ext (Iso.refl _) (by simp))

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
⊢ IsColimit (Cocone.whisker F (H.mapCocone c))

Tactic:
let hc' := isColimitOfPreserves H ((isColimitWhiskerEquiv F _).symm hc)

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) := isColimitOfPreserves H ((isColimitWhiskerEquiv F c).symm hc)
⊢ IsColimit (Cocone.whisker F (H.mapCocone c))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_eq_msb_cond (x : BitVec w) :
    x.toInt = if x.msb then (x.toNat : Int) - (2^w : Nat) else (x.toNat : Int)

Proof state:
w : Nat
x : BitVec w
⊢ (if x.msb = false then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Tactic:
cases x.msb <;> rfl

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Tactic:
simp only [BitVec.toInt, ← msb_eq_false_iff_two_mul_lt]

Result:
w : Nat
x : BitVec w
⊢ (if x.msb = false then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
-- Mathlib/Algebra/Algebra/Prod.lean
theorem snd_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : (snd R B C).comp (prod f g) = g

Proof state:
case H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
ext

Result:
case H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem exists_contracting_iterate :
    ∃ (N : ℕ) (K : _), ContractingWith K (FunSpace.next : v.FunSpace → v.FunSpace)^[N]

Proof state:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
N : ℕ
hN : (↑v.L * v.tDist) ^ N / ↑N ! < 1
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]

Tactic:
have : (0 : ℝ) ≤ (v.L * v.tDist) ^ N / N ! :=
  div_nonneg (pow_nonneg (mul_nonneg v.L.2 v.tDist_nonneg) _) (Nat.cast_nonneg _)

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
N : ℕ
hN : (↑v.L * v.tDist) ^ N / ↑N ! < 1
this : 0 ≤ (↑v.L * v.tDist) ^ N / ↑N !
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]

Proof state:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
N : ℕ
hN : (↑v.L * v.tDist) ^ N / ↑N ! < 1
this : 0 ≤ (↑v.L * v.tDist) ^ N / ↑N !
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]

Tactic:
exact ⟨N, ⟨_, this⟩, hN, LipschitzWith.of_dist_le_mul fun f g =>
  FunSpace.dist_iterate_next_le f g N⟩

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]

Tactic:
rcases ((FloorSemiring.tendsto_pow_div_factorial_atTop (v.L * v.tDist)).eventually
  (gt_mem_nhds zero_lt_one)).exists with ⟨N, hN⟩

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
N : ℕ
hN : (↑v.L * v.tDist) ^ N / ↑N ! < 1
⊢ ∃ N K, ContractingWith K FunSpace.next^[N]
-- Mathlib/Data/Multiset/Sections.lean
theorem card_sections {s : Multiset (Multiset α)} : card (Sections s) = prod (s.map card) :=
  Multiset.induction_on s (by simp) (by simp +contextual)

Proof state:
α : Type u_1
s : Multiset (Multiset α)
⊢ (Sections 0).card = (map card 0).prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ (a : Multiset α) (s : Multiset (Multiset α)),
    s.Sections.card = (map card s).prod → (a ::ₘ s).Sections.card = (map card (a ::ₘ s)).prod

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem polar_closedBall {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ}
    (hr : 0 < r) : polar 𝕜 (closedBall (0 : E) r) = closedBall (0 : Dual 𝕜 E) r⁻¹

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
z : E
x✝ : z ∈ ball 0 r
⊢ ‖x' z‖ ≤ r⁻¹ * ‖z‖

Tactic:
simpa only [one_div] using LinearMap.bound_of_ball_bound' hr 1 x'.toLinearMap h z

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ ‖x'‖ ≤ r⁻¹

Tactic:
refine ContinuousLinearMap.opNorm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => ?_

Result:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
z : E
x✝ : z ∈ ball 0 r
⊢ ‖x' z‖ ≤ r⁻¹ * ‖z‖

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ x' ∈ closedBall 0 r⁻¹

Tactic:
simp only [mem_closedBall_zero_iff]

Result:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ ‖x'‖ ≤ r⁻¹

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ⊆ closedBall 0 r⁻¹

Tactic:
intro x' h

Result:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ x' ∈ closedBall 0 r⁻¹

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) = closedBall 0 r⁻¹

Tactic:
refine Subset.antisymm ?_ (closedBall_inv_subset_polar_closedBall 𝕜)

Result:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ⊆ closedBall 0 r⁻¹
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi {θ ψ : Angle}
    (h : (2 : ℤ) • θ + (2 : ℤ) • ψ = π) : |cos θ| = |sin ψ|

Proof state:
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
exact abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem cpow_eq_nhds {a b : ℂ} (ha : a ≠ 0) :
    (fun x => x ^ b) =ᶠ[𝓝 a] fun x => exp (log x * b)

Proof state:
a b : ℂ
ha : a ≠ 0
⊢ (fun x => x ^ b) =ᶠ[𝓝 a] fun x => cexp (Complex.log x * b)

Tactic:
suffices ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0 from
  this.mono fun x hx ↦ by
    dsimp only
    rw [cpow_def_of_ne_zero hx]

Result:
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0

Proof state:
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = cexp (Complex.log x * b)

Tactic:
rw [cpow_def_of_ne_zero hx]

Result:
no goals

Proof state:
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => x ^ b) x = (fun x => cexp (Complex.log x * b)) x

Tactic:
dsimp only

Result:
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = cexp (Complex.log x * b)

Proof state:
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0

Tactic:
exact IsOpen.eventually_mem isOpen_ne ha

Result:
no goals
-- Mathlib/CategoryTheory/Quotient.lean
theorem induction {P : ∀ {a b : Quotient r}, (a ⟶ b) → Prop}
    (h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)) :
    ∀ {a b : Quotient r} (f : a ⟶ b), P f

Proof state:
case mk.mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
x y : C
f✝ : { as := x } ⟶ { as := y }
f : { as := x }.as ⟶ { as := y }.as
⊢ P (Quot.mk (CompClosure r) f)

Tactic:
exact h f

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
⊢ ∀ {a b : Quotient r} (f : a ⟶ b), P f

Tactic:
rintro ⟨x⟩ ⟨y⟩ ⟨f⟩

Result:
case mk.mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
x y : C
f✝ : { as := x } ⟶ { as := y }
f : { as := x }.as ⟶ { as := y }.as
⊢ P (Quot.mk (CompClosure r) f)
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma congr_left_φH {γ₁ γ₂ : HomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) :
    γ₁.left.φH = γ₂.left.φH

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
γ₁ γ₂ : HomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.left.φH = γ₂.left.φH

Tactic:
rw [eq]

Result:
no goals
-- Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean
theorem isDiscreteValuationRing : IsDiscreteValuationRing (𝕎 k) :=
  IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization (by
    refine ⟨p, irreducible p, fun {x} hx => ?_⟩
    obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx
    exact ⟨n, b, hb.symm⟩)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
⊢ ∃ n, Associated (↑p ^ n) x

Tactic:
obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx

Result:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
n : ℕ
b : (𝕎 k)ˣ
hb : x = ↑p ^ n * ↑b
⊢ ∃ n, Associated (↑p ^ n) x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
⊢ IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (𝕎 k)

Tactic:
refine ⟨p, irreducible p, fun {x} hx => ?_⟩

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
⊢ ∃ n, Associated (↑p ^ n) x

Proof state:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
hx : x ≠ 0
n : ℕ
b : (𝕎 k)ˣ
hb : x = ↑p ^ n * ↑b
⊢ ∃ n, Associated (↑p ^ n) x

Tactic:
exact ⟨n, b, hb.symm⟩

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
/-- A star algebra over `K` has a scalar multiplication that respects the order. -/
lemma _root_.StarModule.instOrderedSMul {A : Type*} [NonUnitalRing A] [StarRing A] [PartialOrder A]
    [StarOrderedRing A] [Module K A] [StarModule K A] [IsScalarTower K A A] [SMulCommClass K A A] :
    OrderedSMul K A where
  smul_lt_smul_of_pos {_ _ _} hxy hc := StarModule.smul_lt_smul_of_pos hxy hc
  lt_of_smul_lt_smul_of_pos {x y c} hxy hc

Proof state:
K : Type u_1
inst✝⁸ : RCLike K
A : Type u_3
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module K A
inst✝² : StarModule K A
inst✝¹ : IsScalarTower K A A
inst✝ : SMulCommClass K A A
x y : A
c : K
hxy : c • x < c • y
hc : 0 < c
⊢ x < y

Tactic:
have : c⁻¹ • c • x < c⁻¹ • c • y :=
  StarModule.smul_lt_smul_of_pos hxy (RCLike.inv_pos_of_pos hc)

Result:
K : Type u_1
inst✝⁸ : RCLike K
A : Type u_3
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module K A
inst✝² : StarModule K A
inst✝¹ : IsScalarTower K A A
inst✝ : SMulCommClass K A A
x y : A
c : K
hxy : c • x < c • y
hc : 0 < c
this : c⁻¹ • c • x < c⁻¹ • c • y
⊢ x < y

Proof state:
K : Type u_1
inst✝⁸ : RCLike K
A : Type u_3
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module K A
inst✝² : StarModule K A
inst✝¹ : IsScalarTower K A A
inst✝ : SMulCommClass K A A
x y : A
c : K
hxy : c • x < c • y
hc : 0 < c
this : c⁻¹ • c • x < c⁻¹ • c • y
⊢ x < y

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc.ne'] using this

Result:
no goals