harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
theorem iter_deriv_exp : ∀ n : ℕ, deriv^[n] exp = exp
  | 0 => rfl
  | n + 1 => by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

Proof state:
n : ℕ
⊢ deriv^[n + 1] rexp = rexp

Tactic:
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem filter_range_nth_subset_insert (k : ℕ) :
    {n ∈ range (nth p (k + 1)) | p n} ⊆ insert (nth p k) {n ∈ range (nth p k) | p n}

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a < nth p (k + 1) ∧ p a
⊢ a = nth p k ∨ a < nth p k ∧ p a

Tactic:
exact (le_nth_of_lt_nth_succ ha.1 ha.2).eq_or_lt.imp_right fun h => ⟨h, ha.2⟩

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
⊢ filter (fun n => p n) (range (nth p (k + 1))) ⊆ insert (nth p k) (filter (fun n => p n) (range (nth p k)))

Tactic:
intro a ha

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a ∈ filter (fun n => p n) (range (nth p (k + 1)))
⊢ a ∈ insert (nth p k) (filter (fun n => p n) (range (nth p k)))

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a ∈ filter (fun n => p n) (range (nth p (k + 1)))
⊢ a ∈ insert (nth p k) (filter (fun n => p n) (range (nth p k)))

Tactic:
simp only [mem_insert, mem_filter, mem_range] at ha ⊢

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
ha : a < nth p (k + 1) ∧ p a
⊢ a = nth p k ∨ a < nth p k ∧ p a
-- Mathlib/Data/Bool/Basic.lean
@[simp] lemma toNat_beq_one (b : Bool) : (b.toNat == 1) =  b

Proof state:
b : Bool
⊢ (b.toNat == 1) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_right_inj (hx₀ : 0 < x) (hx₁ : x ≠ 1) : x ^ y = x ^ z ↔ y = z

Proof state:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ by rw [H]⟩

Result:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
⊢ y = z

Proof state:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : y = z
⊢ x ^ y = x ^ z

Tactic:
rw [H]

Result:
no goals

Proof state:
case inl
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : x < 1
⊢ y = z

Tactic:
exact (strictAnti_rpow_of_base_lt_one hx₀ h).injective H

Result:
no goals

Proof state:
case inr
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : 1 < x
⊢ y = z

Tactic:
exact (strictMono_rpow_of_base_gt_one h).injective H

Result:
no goals

Proof state:
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
⊢ y = z

Tactic:
rcases hx₁.lt_or_lt with h | h

Result:
case inl
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : x < 1
⊢ y = z

case inr
x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
H : x ^ y = x ^ z
h : 1 < x
⊢ y = z
-- Mathlib/Topology/Maps/Basic.lean
theorem comp (hg : IsOpenMap g) (hf : IsOpenMap f) :
    IsOpenMap (g ∘ f) := fun s hs => by rw [image_comp]; exact hg _ (hf _ hs)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen s
⊢ IsOpen (g '' (f '' s))

Tactic:
exact hg _ (hf _ hs)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen s
⊢ IsOpen (g ∘ f '' s)

Tactic:
rw [image_comp]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen s
⊢ IsOpen (g '' (f '' s))
-- Mathlib/Algebra/Homology/Localization.lean
lemma ComplexShape.quotient_isLocalization :
    (HomotopyCategory.quotient C c).IsLocalization
      (HomologicalComplex.homotopyEquivalences _ _)

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
⊢ (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)

Tactic:
apply Functor.IsLocalization.mk'

Result:
case h₁
ι : 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
⊢ Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory C c)

case h₂
ι : 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
⊢ Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c) (HomologicalComplex.homotopyEquivalences C c).Localization

Proof state:
case h₂
ι : 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
⊢ Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c) (HomologicalComplex.homotopyEquivalences C c).Localization

Tactic:
apply c.strictUniversalPropertyFixedTargetQuotient hc

Result:
no goals

Proof state:
case h₁
ι : 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
⊢ Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory C c)

case h₂
ι : 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
⊢ Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
    (HomologicalComplex.homotopyEquivalences C c) (HomologicalComplex.homotopyEquivalences C c).Localization

Tactic:
all_goals apply c.strictUniversalPropertyFixedTargetQuotient hc

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem _root_.Commute.exp_right [T2Space 𝔸] {x y : 𝔸} (h : Commute x y) :
    Commute x (exp 𝕂 y)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)

Tactic:
exact Commute.tsum_right x fun n => (h.pow_right n).smul_right _

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x (exp 𝕂 y)

Tactic:
rw [exp_eq_tsum]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)
-- Mathlib/Data/ENNReal/Inv.lean
theorem top_div : ∞ / a = if a = ∞ then 0 else ∞

Proof state:
a : ℝ≥0∞
⊢ ⊤ / a = if a = ⊤ then 0 else ⊤

Tactic:
simp [div_eq_mul_inv, top_mul']

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem convexOn : ConvexOn ℝ univ p

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ p (a • x + b • y) ≤ a • p x + b • p y

Tactic:
calc
  p (a • x + b • y) ≤ p (a • x) + p (b • y) := map_add_le_add p _ _
  _ = ‖a • (1 : 𝕜)‖ * p x + ‖b • (1 : 𝕜)‖ * p y := by
    rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
  _ = a * p x + b * p y := by
    rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
      Real.norm_of_nonneg hb]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ p (a • x) + p (b • y) = ‖a • 1‖ * p x + ‖b • 1‖ * p y

Tactic:
rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
⊢ ConvexOn ℝ univ ⇑p

Tactic:
refine ⟨convex_univ, fun x _ y _ a b ha hb _ => ?_⟩

Result:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ p (a • x + b • y) ≤ a • p x + b • p y

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ‖a • 1‖ * p x + ‖b • 1‖ * p y = a * p x + b * p y

Tactic:
rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
  Real.norm_of_nonneg hb]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem map_zero₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (y : F) : f 0 y = 0

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹¹ : SeminormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : SeminormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
y : F
⊢ (f 0) y = 0

Tactic:
rw [f.map_zero, zero_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/HomCompletion.lean
theorem NormedAddGroupHom.completion_toCompl (f : NormedAddGroupHom G H) :
    f.completion.comp toCompl = toCompl.comp f

Proof state:
case H
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ (f.completion.comp toCompl) x = (toCompl.comp f) x

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
⊢ f.completion.comp toCompl = toCompl.comp f

Tactic:
ext x

Result:
case H
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ (f.completion.comp toCompl) x = (toCompl.comp f) x
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem tsum_mul_left [T2Space α] : ∑' x, a * f x = a * ∑' x, f x

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x

Tactic:
exact if hf : Summable f then hf.tsum_mul_left a
else if ha : a = 0 then by simp [ha]
else by rw [tsum_eq_zero_of_not_summable hf,
            tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).mp hf), mul_zero]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x

Tactic:
classical
exact if hf : Summable f then hf.tsum_mul_left a
else if ha : a = 0 then by simp [ha]
else by rw [tsum_eq_zero_of_not_summable hf,
            tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).mp hf), mul_zero]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
hf : ¬Summable f
ha : ¬a = 0
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x

Tactic:
rw [tsum_eq_zero_of_not_summable hf,
    tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).mp hf), mul_zero]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
hf : ¬Summable f
ha : a = 0
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_toReal (θ : Angle) : Real.cos θ.toReal = cos θ

Proof state:
θ : Angle
⊢ Real.cos θ.toReal = θ.cos

Tactic:
conv_rhs => rw [← coe_toReal θ, cos_coe]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem IsBase.cardinalMk_eq_cRank (hB : M.IsBase B) : #B = M.cRank

Proof state:
α : Type u
M : Matroid α
B : Set α
inst✝ : M.InvariantCardinalRank
hB : M.IsBase B
⊢ #↑B = M.cRank

Tactic:
have hrw : ∀ B' : {B : Set α // M.IsBase B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB

Result:
α : Type u
M : Matroid α
B : Set α
inst✝ : M.InvariantCardinalRank
hB : M.IsBase B
hrw : ∀ (B' : { B // M.IsBase B }), #↑↑B' = #↑B
⊢ #↑B = M.cRank

Proof state:
α : Type u
M : Matroid α
B : Set α
inst✝ : M.InvariantCardinalRank
hB : M.IsBase B
hrw : ∀ (B' : { B // M.IsBase B }), #↑↑B' = #↑B
⊢ #↑B = M.cRank

Tactic:
simp [cRank, hrw]

Result:
no goals
-- Mathlib/RingTheory/Regular/IsSMulRegular.lean
lemma isSMulRegular_on_submodule_iff_mem_imp_smul_eq_zero_imp_eq_zero :
    IsSMulRegular N r ↔ ∀ x ∈ N, r • x = 0 → x = 0 :=
  Iff.trans (isSMulRegular_iff_smul_eq_zero_imp_eq_zero N r) <|
    Iff.trans Subtype.forall <| by
      simp only [SetLike.mk_smul_mk, Submodule.mk_eq_zero]

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), r • ⟨a, b⟩ = 0 → ⟨a, b⟩ = 0) ↔ ∀ x ∈ N, r • x = 0 → x = 0

Tactic:
simp only [SetLike.mk_smul_mk, Submodule.mk_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem inv_insert (a : α) (s : Set α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
a : α
s : Set α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹

Tactic:
rw [insert_eq, union_inv, inv_singleton, insert_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.mulVec_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R} :
    Function.Injective M.mulVec ↔ LinearIndependent R (fun i ↦ Mᵀ i)

Proof state:
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
R : Type u_6
inst✝ : CommRing R
M : Matrix m n R
⊢ Function.Injective M.mulVec ↔ LinearIndependent R fun i => Mᵀ i

Tactic:
change Function.Injective (fun x ↦ _) ↔ _

Result:
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
R : Type u_6
inst✝ : CommRing R
M : Matrix m n R
⊢ (Function.Injective fun x => M *ᵥ x) ↔ LinearIndependent R fun i => Mᵀ i

Proof state:
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
R : Type u_6
inst✝ : CommRing R
M : Matrix m n R
⊢ (Function.Injective fun x => M *ᵥ x) ↔ LinearIndependent R fun i => Mᵀ i

Tactic:
simp_rw [← M.vecMul_transpose, vecMul_injective_iff]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_one_right_iff (n : ℕ) : Coprime n 1 ↔ True

Proof state:
n : ℕ
⊢ n.Coprime 1 ↔ True

Tactic:
simp [Coprime]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem iterateFrobeniusEquiv_zero_apply (x : R) : iterateFrobeniusEquiv R p 0 x = x

Proof state:
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p 0) x = x

Tactic:
rw [iterateFrobeniusEquiv_def, pow_zero, pow_one]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem nnnorm_equiv_symm_snd (y : β) :
    ‖(WithLp.equiv p (α × β)).symm (0, y)‖₊ = ‖y‖₊

Proof state:
case coe
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y : β
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
⊢ ‖(WithLp.equiv (↑p) (α × β)).symm (0, y)‖₊ = ‖y‖₊

Tactic:
have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'

Result:
case coe
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y : β
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖(WithLp.equiv (↑p) (α × β)).symm (0, y)‖₊ = ‖y‖₊

Proof state:
case top
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y : β
hp : Fact (1 ≤ ⊤)
⊢ ‖(WithLp.equiv ⊤ (α × β)).symm (0, y)‖₊ = ‖y‖₊

Tactic:
simp [prod_nnnorm_eq_sup]

Result:
no goals

Proof state:
case coe
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y : β
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖(WithLp.equiv (↑p) (α × β)).symm (0, y)‖₊ = ‖y‖₊

Tactic:
simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y : β
⊢ ‖(WithLp.equiv p (α × β)).symm (0, y)‖₊ = ‖y‖₊

Tactic:
induction p generalizing hp with
| top =>
  simp [prod_nnnorm_eq_sup]
| coe p =>
  have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
  simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Result:
no goals
-- Mathlib/Algebra/Ring/CharZero.lean
lemma charZero_iff {ϕ : R →+* S} (hϕ : Injective ϕ) : CharZero R ↔ CharZero S :=
  ⟨fun hR =>
    ⟨by intro a b h; rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]⟩,
    fun _ => ϕ.charZero⟩

Proof state:
R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b

Tactic:
rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
⊢ Injective Nat.cast

Tactic:
intro a b h

Result:
R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_cpow_inv_nat (x : ℂ) (n : ℕ) : ‖x ^ (n⁻¹ : ℂ)‖ = ‖x‖ ^ (n⁻¹ : ℝ)

Proof state:
x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x‖ ^ (↑n)⁻¹

Tactic:
rw [← norm_cpow_real]

Result:
x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x ^ ↑(↑n)⁻¹‖

Proof state:
x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x ^ ↑(↑n)⁻¹‖

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma Y_sub_polynomialY : Y - W'.polynomialY = W'.negPolynomial

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - W'.polynomialY = W'.negPolynomial

Tactic:
rw [polynomialY, negPolynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃)) = -Y - C (C W'.a₁ * X + C W'.a₃)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (2 * Y + (C (C W'.a₁) * C X + C (C W'.a₃))) = -Y - (C (C W'.a₁) * C X + C (C W'.a₃))

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (C (C 2) * Y + C (C W'.a₁ * X + C W'.a₃)) = -Y - C (C W'.a₁ * X + C W'.a₃)

Tactic:
C_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - (2 * Y + (C (C W'.a₁) * C X + C (C W'.a₃))) = -Y - (C (C W'.a₁) * C X + C (C W'.a₃))
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem coe_mul (n m : ℤ) : ((n * m : ℤ) : X q) = (n : X q) * (m : X q)

Proof state:
q : ℕ+
n m : ℤ
⊢ ↑(n * m) = ↑n * ↑m

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Basic.lean
theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2^n) : m >>> n = 0

Proof state:
m n : Nat
hn : m < 2 ^ n
⊢ m >>> n = 0

Tactic:
simp [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α β)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
c : Nat
⊢ ¬a ∈ empty c

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem LocallyIntegrableOn.integrableOn_of_isBigO_atBot [IsMeasurablyGenerated (atBot (α := α))]
    (hf : LocallyIntegrableOn f (Iic a) μ) (ho : f =O[atBot] g)
    (hg : IntegrableAtFilter g atBot μ) : IntegrableOn f (Iic a) μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atBot.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ IntegrableOn f (Iic a) μ

Tactic:
refine integrableOn_Iic_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atBot.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atBot.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
exact ⟨Iic a, Iic_mem_atBot a, hf.aestronglyMeasurable⟩

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive] lemma prod_subset {s : Finset ι} {f : ι → α} (h : ∀ i, f i ≠ 1 → i ∈ s) :
    ∏ i ∈ s, f i = ∏ i, f i :=
  Finset.prod_subset s.subset_univ <| by simpa [not_imp_comm (a := _ ∈ s)]

Proof state:
ι : Type u_6
α : Type u_8
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
h : ∀ (i : ι), f i ≠ 1 → i ∈ s
⊢ ∀ x ∈ univ, x ∉ s → f x = 1

Tactic:
simpa [not_imp_comm (a := _ ∈ s)]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
theorem stabilizer_of_subMul {p : SubMulAction R M} (m : p) :
    MulAction.stabilizer R m = MulAction.stabilizer R (m : M)

Proof state:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ (MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid

Tactic:
exact stabilizer_of_subMul.submonoid m

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ MulAction.stabilizer R m = MulAction.stabilizer R ↑m

Tactic:
rw [← Subgroup.toSubmonoid_inj]

Result:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ (MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
-- Mathlib/Computability/Primrec.lean
theorem list_getD (d : α) : Primrec₂ fun l n => List.getD l n d

Proof state:
α : Type u_1
inst✝ : Primcodable α
d : α
⊢ Primrec₂ fun l n => l[n]?.getD d

Tactic:
exact option_getD.comp₂ list_getElem? (const _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
d : α
⊢ Primrec₂ fun l n => l.getD n d

Tactic:
simp only [List.getD_eq_getElem?_getD]

Result:
α : Type u_1
inst✝ : Primcodable α
d : α
⊢ Primrec₂ fun l n => l[n]?.getD d