harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_zero [Zero α] : fromBlocks (0 : Matrix n l α) 0 0 (0 : Matrix o m α) = 0

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks 0 0 0 0 i j = 0 i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
⊢ fromBlocks 0 0 0 0 = 0

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks 0 0 0 0 i j = 0 i j
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.multiplicity_eq_iff (hf : FiniteMultiplicity a b) {n : ℕ} :
    multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
n : ℕ
⊢ multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
simp [← emultiplicity_eq_coe, hf.emultiplicity_eq_multiplicity]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma binEntropy_le_log_two : binEntropy p ≤ log 2

Proof state:
p : ℝ
⊢ binEntropy p ≤ log 2

Tactic:
obtain rfl | hp := eq_or_ne p 2⁻¹

Result:
case inl

⊢ binEntropy 2⁻¹ ≤ log 2

case inr
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2

Proof state:
case inr
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2

Tactic:
exact (binEntropy_lt_log_two.2 hp).le

Result:
no goals

Proof state:
case inl

⊢ binEntropy 2⁻¹ ≤ log 2

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/GradedModule.lean
theorem smulAddMonoidHom_apply_of_of [DecidableEq ιA] [DecidableEq ιB] [GMonoid A] [Gmodule A M]
    {i j} (x : A i) (y : M j) :
    smulAddMonoidHom A M (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
⊢ ((smulAddMonoidHom A M) ((of A i) x)) ((of M j) y) = (of M (i +ᵥ j)) (GSMul.smul x y)

Tactic:
simp [smulAddMonoidHom]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_eq_zero_iff {o} {f : ∀ a < o, Ordinal} : bsup o f = 0 ↔ ∀ i hi, f i hi = 0

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
⊢ o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi = 0

Tactic:
refine
  ⟨fun h i hi => ?_, fun h =>
    le_antisymm (bsup_le fun i hi => Ordinal.le_zero.2 (h i hi)) (Ordinal.zero_le _)⟩

Result:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
h : o.bsup f = 0
i : Ordinal.{u_4}
hi : i < o
⊢ f i hi = 0

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
h : o.bsup f = 0
i : Ordinal.{u_4}
hi : i < o
⊢ f i hi ≤ o.bsup f

Tactic:
exact le_bsup f i hi

Result:
no goals

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
h : o.bsup f = 0
i : Ordinal.{u_4}
hi : i < o
⊢ f i hi = 0

Tactic:
rw [← Ordinal.le_zero, ← h]

Result:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
h : o.bsup f = 0
i : Ordinal.{u_4}
hi : i < o
⊢ f i hi ≤ o.bsup f
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem PosDef.anisotropic {Q : QuadraticMap R₂ M N} (hQ : Q.PosDef) : Q.Anisotropic :=
  fun x hQx => by_contradiction fun hx =>
    lt_irrefl (0 : N) <| by
      have := hQ _ hx
      rw [hQx] at this
      exact this

Proof state:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Q x = 0
hx : ¬x = 0
this : 0 < Q x
⊢ 0 < 0

Tactic:
rw [hQx] at this

Result:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Q x = 0
hx : ¬x = 0
this : 0 < 0
⊢ 0 < 0

Proof state:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Q x = 0
hx : ¬x = 0
this : 0 < 0
⊢ 0 < 0

Tactic:
exact this

Result:
no goals

Proof state:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Q x = 0
hx : ¬x = 0
⊢ 0 < 0

Tactic:
have := hQ _ hx

Result:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Q x = 0
hx : ¬x = 0
this : 0 < Q x
⊢ 0 < 0
-- Mathlib/CategoryTheory/Sites/MorphismProperty.lean
lemma pretopology_inf :
    (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology

Proof state:
case coverings.h.h
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.IsMultiplicative
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : Q.IsMultiplicative
inst✝ : Q.IsStableUnderBaseChange
X : C
S : Presieve X
⊢ S ∈ (P ⊓ Q).pretopology.coverings X ↔ S ∈ (P.pretopology ⊓ Q.pretopology).coverings X

Tactic:
exact ⟨fun hS ↦ ⟨fun hf ↦ (hS hf).left, fun hf ↦ (hS hf).right⟩,
  fun h ↦ fun hf ↦ ⟨h.left hf, h.right hf⟩⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.IsMultiplicative
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : Q.IsMultiplicative
inst✝ : Q.IsStableUnderBaseChange
⊢ (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology

Tactic:
ext X S

Result:
case coverings.h.h
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.IsMultiplicative
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : Q.IsMultiplicative
inst✝ : Q.IsStableUnderBaseChange
X : C
S : Presieve X
⊢ S ∈ (P ⊓ Q).pretopology.coverings X ↔ S ∈ (P.pretopology ⊓ Q.pretopology).coverings X
-- Mathlib/Order/InitialSeg.lean
theorem collapseF_not_lt [IsWellOrder β s] (f : r ↪r s) (a : α) {b}
    (h : ∀ a', r a' a → s (collapseF f a') b) : ¬s b (collapseF f a)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(let_fun H := ⋯;
        ⟨⋯.min
            {b |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun y x =>
                        IsWellFounded.fix r
                          (fun a IH =>
                            let_fun H := ⋯;
                            ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                          y)
                      a_1 h))
                  b}
            ⋯,
          ⋯⟩)

Tactic:
dsimp only

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      (⋯.min
        {b |
          ∀ (a_1 : α),
            r a_1 a →
              s
                (↑(IsWellFounded.fix r (fun a IH => ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                    a_1))
                b}
        ⋯)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      (⋯.min
        {b |
          ∀ (a_1 : α),
            r a_1 a →
              s
                (↑(IsWellFounded.fix r (fun a IH => ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                    a_1))
                b}
        ⋯)

Tactic:
exact WellFounded.not_lt_min _ _ _ h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b ↑(collapseF f a)

Tactic:
rw [collapseF, IsWellFounded.fix_eq]

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(let_fun H := ⋯;
        ⟨⋯.min
            {b |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun y x =>
                        IsWellFounded.fix r
                          (fun a IH =>
                            let_fun H := ⋯;
                            ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                          y)
                      a_1 h))
                  b}
            ⋯,
          ⋯⟩)
-- Mathlib/Order/Filter/Prod.lean
theorem prod_neBot : NeBot (f ×ˢ g) ↔ NeBot f ∧ NeBot g

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
simp only [neBot_iff, Ne, prod_eq_bot, not_or]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma cpow_ofReal (x : ℂ) (y : ℝ) :
    x ^ (y : ℂ) = ↑(‖x‖ ^ y) * (Real.cos (arg x * y) + Real.sin (arg x * y) * I)

Proof state:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑(rexp (↑y * log x).re) * (↑(Real.cos (↑y * log x).im) + ↑(Real.sin (↑y * log x).im) * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
rw [re_ofReal_mul, im_ofReal_mul, log_re, log_im, mul_comm y, mul_comm y, Real.exp_mul,
  Real.exp_log]

Result:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ 0 < ‖x‖

Proof state:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
rw [cpow_def_of_ne_zero hx, exp_eq_exp_re_mul_sin_add_cos, mul_comm (log x)]

Result:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ cexp ↑(↑y * log x).re * (cos ↑(↑y * log x).im + sin ↑(↑y * log x).im * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Proof state:
case inl
y : ℝ
⊢ 0 ^ ↑y = ↑(‖0‖ ^ y) * (↑(Real.cos (arg 0 * y)) + ↑(Real.sin (arg 0 * y)) * I)

Tactic:
simp [ofReal_cpow le_rfl]

Result:
no goals

Proof state:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ 0 < ‖x‖

Tactic:
rwa [norm_pos_iff]

Result:
no goals

Proof state:
x : ℂ
y : ℝ
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
y : ℝ
⊢ 0 ^ ↑y = ↑(‖0‖ ^ y) * (↑(Real.cos (arg 0 * y)) + ↑(Real.sin (arg 0 * y)) * I)

case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Proof state:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ cexp ↑(↑y * log x).re * (cos ↑(↑y * log x).im + sin ↑(↑y * log x).im * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
norm_cast

Result:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑(rexp (↑y * log x).re) * (↑(Real.cos (↑y * log x).im) + ↑(Real.sin (↑y * log x).im) * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_mkArray_of_lt {n : Nat} {m : Nat} (h : m < n) : (mkArray n a)[m]? = some a

Proof state:
α✝ : Type u_1
a : α✝
n m : Nat
h : m < n
⊢ (mkArray n a)[m]? = some a

Tactic:
simp [getElem?_mkArray, h]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem projRestricts_comp_projRestrict (h : ∀ i, J i → K i) :
    ProjRestricts C h ∘ ProjRestrict C K = ProjRestrict C J

Proof state:
case h.a.h
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : ↑C
i : I
⊢ ↑((ProjRestricts C h ∘ ProjRestrict C K) x) i = ↑(ProjRestrict C J x) i

Tactic:
simp only [π, Proj, Function.comp_apply, ProjRestricts_coe, ProjRestrict_coe]

Result:
case h.a.h
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : ↑C
i : I
⊢ (if J i then if K i then ↑x i else false else false) = if J i then ↑x i else false

Proof state:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ ProjRestricts C h ∘ ProjRestrict C K = ProjRestrict C J

Tactic:
ext x i

Result:
case h.a.h
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : ↑C
i : I
⊢ ↑((ProjRestricts C h ∘ ProjRestrict C K) x) i = ↑(ProjRestrict C J x) i

Proof state:
case h.a.h
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : ↑C
i : I
⊢ (if J i then if K i then ↑x i else false else false) = if J i then ↑x i else false

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/CompleteLattice.lean
theorem _root_.Monotone.ciSup_comp_tendsto_atTop_of_linearOrder [Preorder β]
    [ConditionallyCompleteLinearOrder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f)
    {g : α → β} (hg : Tendsto g l atTop) : ⨆ a, f (g a) = ⨆ b, f b

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun a => f (g a))

Tactic:
rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : BddAbove (range f)
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
exact hf.ciSup_comp_tendsto_atTop hb hg

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
if hb : BddAbove (range f) then
  exact hf.ciSup_comp_tendsto_atTop hb hg
else
  rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]
  rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLinearOrder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun a => f (g a))
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_mul_cancel_right (x : M) (y : S) : f.mk' (x * y) y = f.toMap x

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.mk' (x * ↑y) y = f.toMap x

Tactic:
rw [← mul_mk'_one_eq_mk', f.toMap.map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem continuousAt_angle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
    ContinuousAt (fun y : V × V => angle y.1 y.2) x

Proof state:
case funProp.discharger
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ‖x.1‖ * ‖x.2‖ ≠ 0

Tactic:
simp [*]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y => arccos (inner y.1 y.2 / (‖y.1‖ * ‖y.2‖))) x

Tactic:
fun_prop (disch := simp [*])

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y => angle y.1 y.2) x

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y => arccos (inner y.1 y.2 / (‖y.1‖ * ‖y.2‖))) x
-- Mathlib/Data/Finsupp/Basic.lean
theorem equivMapDomain_eq_mapDomain {M} [AddCommMonoid M] (f : α ≃ β) (l : α →₀ M) :
    equivMapDomain f l = mapDomain f l

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_13
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ (equivMapDomain f l) x = (mapDomain (⇑f) l) x

Tactic:
simp [mapDomain_equiv_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_13
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
⊢ equivMapDomain f l = mapDomain (⇑f) l

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_13
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ (equivMapDomain f l) x = (mapDomain (⇑f) l) x
-- Mathlib/Logic/Equiv/Set.lean
theorem sumDiffSubset_symm_apply_of_not_mem {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)]
    {x : t} (hx : x.1 ∉ s) : (Equiv.Set.sumDiffSubset h).symm x = Sum.inr ⟨x, ⟨x.2, hx⟩⟩

Proof state:
case a
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∉ s
⊢ (Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inr ⟨↑x, ⋯⟩)

Tactic:
simp only [apply_symm_apply, sumDiffSubset_apply_inr, Set.inclusion_mk]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∉ s
⊢ (Set.sumDiffSubset h).symm x = Sum.inr ⟨↑x, ⋯⟩

Tactic:
apply (Equiv.Set.sumDiffSubset h).injective

Result:
case a
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∉ s
⊢ (Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inr ⟨↑x, ⋯⟩)
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem yz_sub {m n} (h : n ≤ m) : yz a1 (m - n) = xz a1 n * yz a1 m - xz a1 m * yz a1 n

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 n * yz a1 m - xz a1 m * yz a1 n

Tactic:
rw [sub_eq_add_neg, ← mul_neg, mul_comm, add_comm]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n

Tactic:
exact congr_arg Zsqrtd.im (pellZd_sub a1 h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_push_of_pos (l : Vector α n) (pa : p a) : countP p (l.push a) = countP p l + 1

Proof state:
case mk
α : Type u_1
p : α → Bool
n : Nat
a : α
pa : p a = true
l : Array α
size_toArray✝ : l.size = n
⊢ countP p ({ toArray := l, size_toArray := size_toArray✝ }.push a) =
    countP p { toArray := l, size_toArray := size_toArray✝ } + 1

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
l : Vector α n
pa : p a = true
⊢ countP p (l.push a) = countP p l + 1

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
n : Nat
a : α
pa : p a = true
l : Array α
size_toArray✝ : l.size = n
⊢ countP p ({ toArray := l, size_toArray := size_toArray✝ }.push a) =
    countP p { toArray := l, size_toArray := size_toArray✝ } + 1
-- Mathlib/Topology/PartialHomeomorph.lean
theorem restr_source_inter (s : Set X) : e.restr (e.source ∩ s) = e.restr s

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
⊢ (e.restr (e.source ∩ s)).source = (e.restr s).source

Tactic:
simp [e.open_source.interior_eq, ← inter_assoc]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
⊢ e.restr (e.source ∩ s) = e.restr s

Tactic:
refine PartialHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) ?_

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
⊢ (e.restr (e.source ∩ s)).source = (e.restr s).source
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem extendScalars_self : extendScalars (le_refl F) = ⊥

Proof state:
case h
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ Set.range ⇑(algebraMap (↥F) L) → x ∈ F

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.intro
L : Type u_2
inst✝ : Field L
F : Subfield L
y : ↥F
⊢ (algebraMap (↥F) L) y ∈ F

Proof state:
case h
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ extendScalars ⋯ ↔ x ∈ ⊥

Tactic:
rw [mem_extendScalars, IntermediateField.mem_bot]

Result:
case h
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ F ↔ x ∈ Set.range ⇑(algebraMap (↥F) L)

Proof state:
case h
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ F ↔ x ∈ Set.range ⇑(algebraMap (↥F) L)

Tactic:
refine ⟨fun h ↦ ⟨⟨x, h⟩, rfl⟩, ?_⟩

Result:
case h
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ Set.range ⇑(algebraMap (↥F) L) → x ∈ F

Proof state:
case h.intro
L : Type u_2
inst✝ : Field L
F : Subfield L
y : ↥F
⊢ (algebraMap (↥F) L) y ∈ F

Tactic:
exact y.2

Result:
no goals

Proof state:
L : Type u_2
inst✝ : Field L
F : Subfield L
⊢ extendScalars ⋯ = ⊥

Tactic:
ext x

Result:
case h
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ extendScalars ⋯ ↔ x ∈ ⊥
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_deriv_eq_sub' (f) (hderiv : deriv f = f')
    (hdiff : ∀ x ∈ uIcc a b, DifferentiableAt ℝ f x) (hcont : ContinuousOn f' (uIcc a b)) :
    ∫ y in a..b, f' y = f b - f a

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
rw [← hderiv, integral_deriv_eq_sub hdiff]

Result:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable (deriv f) volume a b

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable f' volume a b

Tactic:
exact hcont.intervalIntegrable

Result:
no goals

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
rw [hderiv]

Result:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable f' volume a b
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem apply_mk_symm (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
    e ⟨b, e.symm b y⟩ = (b, y)

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → Zero (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∈ e.baseSet
y : F
⊢ ↑e { proj := b, snd := e.symm b y } = (b, y)

Tactic:
rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]

Result:
no goals