harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem SL2_inv_expl (A : SL(2, R)) :
    A⁻¹ = ⟨![![A.1 1 1, -A.1 0 1], ![-A.1 1 0, A.1 0 0]], SL2_inv_expl_det A⟩

Proof state:
case a
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]
⊢ !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0] i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
case a
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
⊢ ↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝

Tactic:
have := Matrix.adjugate_fin_two A.1

Result:
case a
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]
⊢ ↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝

Proof state:
case a
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]
⊢ ↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝

Tactic:
rw [coe_inv, this]

Result:
case a
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]
⊢ !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0] i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝

Proof state:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ A⁻¹ = ⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩

Tactic:
ext

Result:
case a
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
⊢ ↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝
-- Mathlib/Topology/DerivedSet.lean
lemma isClosed_iff_derivedSet_subset (A : Set X) : IsClosed A ↔ derivedSet A ⊆ A where
  mp h := derivedSet_subset_closure A |>.trans h.closure_subset
  mpr h

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False

Tactic:
rw [this, ← acc_principal_iff_cluster] at ha

Result:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : AccPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : AccPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False

Tactic:
exact nh (h ha)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ IsClosed A

Tactic:
rw [isClosed_iff_clusterPt]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ ∀ (a : X), ClusterPt a (𝓟 A) → a ∈ A

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
⊢ False

Tactic:
have : A = A \ {a} := by simp [nh]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ ∀ (a : X), ClusterPt a (𝓟 A) → a ∈ A

Tactic:
intro a ha

Result:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
⊢ a ∈ A

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
⊢ A = A \ {a}

Tactic:
simp [nh]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
⊢ a ∈ A

Tactic:
by_contra! nh

Result:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 A)
nh : a ∉ A
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem _root_.HasStrictDerivAt.rpow {f g : ℝ → ℝ} {f' g' : ℝ} (hf : HasStrictDerivAt f f' x)
    (hg : HasStrictDerivAt g g' x) (h : 0 < f x) : HasStrictDerivAt (fun x => f x ^ g x)
      (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x

Proof state:
x : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x)) x

Tactic:
convert (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x
  (hf.prod hg) using 1

Result:
case h.e'_9
x : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x) =
    ((((fun x => (f x, g x)) x).2 * ((fun x => (f x, g x)) x).1 ^ (((fun x => (f x, g x)) x).2 - 1)) •
          ContinuousLinearMap.fst ℝ ℝ ℝ +
        (((fun x => (f x, g x)) x).1 ^ ((fun x => (f x, g x)) x).2 * log ((fun x => (f x, g x)) x).1) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (f', g')

Proof state:
case h.e'_9
x : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x) =
    ((((fun x => (f x, g x)) x).2 * ((fun x => (f x, g x)) x).1 ^ (((fun x => (f x, g x)) x).2 - 1)) •
          ContinuousLinearMap.fst ℝ ℝ ℝ +
        (((fun x => (f x, g x)) x).1 ^ ((fun x => (f x, g x)) x).2 * log ((fun x => (f x, g x)) x).1) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (f', g')

Tactic:
simp [mul_assoc, mul_comm, mul_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : BinaryInput aig}
    {f : (aig : AIG α) → BinaryInput aig → Entrypoint α} [LawfulOperator α BinaryInput f]
    [LawfulZipOperator α f] {h} :
    ⟦f (f aig input1).aig (input2.cast h), assign⟧
      =
    ⟦f aig input2, assign⟧

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
assign : α → Bool
aig : AIG α
input1 input2 : aig.BinaryInput
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝¹ : LawfulOperator α BinaryInput f
inst✝ : LawfulZipOperator α f
h : aig.decls.size ≤ (f aig input1).aig.decls.size
⊢ ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧

Tactic:
rw [LawfulZipOperator.chainable]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValInt.mul {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
    padicValInt p (a * b) = padicValInt p a + padicValInt p b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs

Tactic:
rw [Int.natAbs_mul, padicValNat.mul] <;> rwa [Int.natAbs_ne_zero]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValInt p (a * b) = padicValInt p a + padicValInt p b

Tactic:
simp_rw [padicValInt]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_pellZd (b : ℤ√(d a1)) (b1 : 1 ≤ b) (hp : IsPell b) : ∃ n, b = pellZd a1 n :=
  let ⟨n, h⟩ := @Zsqrtd.le_arch (d a1) b
  eq_pell_lem a1 n b b1 hp <|
    h.trans <| by
      rw [Zsqrtd.natCast_val]
      exact
        Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _)
          (Int.ofNat_zero_le _)

Proof state:
a : ℕ
a1 : 1 < a
b : ℤ√↑(Pell.d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ { re := ↑n, im := 0 } ≤ pellZd a1 n

Tactic:
exact
  Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _)
    (Int.ofNat_zero_le _)

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
b : ℤ√↑(Pell.d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ ↑n ≤ pellZd a1 n

Tactic:
rw [Zsqrtd.natCast_val]

Result:
a : ℕ
a1 : 1 < a
b : ℤ√↑(Pell.d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ { re := ↑n, im := 0 } ≤ pellZd a1 n
-- Mathlib/Algebra/Order/Floor/Div.lean
@[simp] lemma smul_ceilDiv [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) (b : β) :
    a • b ⌈/⌉ a = b :=
  eq_of_forall_ge_iff <| by simp [smul_le_smul_iff_of_pos_left, ha]

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : OrderedSemiring α
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : MulActionWithZero α β
inst✝² : CeilDiv α β
a : α
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
b : β
⊢ ∀ (c : β), a • b ⌈/⌉ a ≤ c ↔ b ≤ c

Tactic:
simp [smul_le_smul_iff_of_pos_left, ha]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
@[reassoc]
lemma shiftMap_comp {X Y Z : C} {n : M} (f : X ⟶ Y⟦n⟧) (g : Y ⟶ Z) (a a' : M) (ha' : n + a = a') :
    F.shiftMap (f ≫ g⟦n⟧') a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Category.{u_6, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
X Y Z : C
n : M
f : X ⟶ (shiftFunctor C n).obj Y
g : Y ⟶ Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ (shiftFunctor C n).map g) a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g

Tactic:
simp [shiftMap]

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem zero_convolution : 0 ⋆[L, μ] g = 0

Proof state:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x✝ : G
⊢ (0 ⋆[L, μ] g) x✝ = 0 x✝

Tactic:
simp_rw [convolution_def, Pi.zero_apply, L.map_zero₂, integral_zero]

Result:
no goals

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
⊢ 0 ⋆[L, μ] g = 0

Tactic:
ext

Result:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x✝ : G
⊢ (0 ⋆[L, μ] g) x✝ = 0 x✝
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_pos_of_finite [Finite s] : 0 < s.einfsep

Proof state:
case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Subsingleton
⊢ 0 < s.einfsep

Tactic:
exact hs.einfsep.symm ▸ WithTop.top_pos

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ 0 < s.einfsep

Tactic:
by_cases hs : s.Nontrivial

Result:
case pos
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
⊢ 0 < s.einfsep

case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep

Proof state:
case pos.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
x : α
_hx : x ∈ s
y : α
_hy : y ∈ s
hxy : x ≠ y
hxy' : s.einfsep = edist x y
⊢ 0 < s.einfsep

Tactic:
exact hxy'.symm ▸ edist_pos.2 hxy

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
⊢ 0 < s.einfsep

Tactic:
rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩

Result:
case pos.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
x : α
_hx : x ∈ s
y : α
_hy : y ∈ s
hxy : x ≠ y
hxy' : s.einfsep = edist x y
⊢ 0 < s.einfsep

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.einfsep

Tactic:
cases nonempty_fintype s

Result:
case intro
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ 0 < s.einfsep

Proof state:
case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep

Tactic:
rw [not_nontrivial_iff] at hs

Result:
case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Subsingleton
⊢ 0 < s.einfsep
-- Mathlib/Data/ENNReal/Basic.lean
theorem toReal_eq_zero_iff (x : ℝ≥0∞) : x.toReal = 0 ↔ x = 0 ∨ x = ∞

Proof state:
x : ℝ≥0∞
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤

Tactic:
simp [ENNReal.toReal, toNNReal_eq_zero_iff]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/Bounds.lean
theorem harmonic_floor_le_one_add_log (y : ℝ) (hy : 1 ≤ y) :
    harmonic ⌊y⌋₊ ≤ 1 + Real.log y

Proof state:
y : ℝ
hy : 1 ≤ y
⊢ ↑(harmonic ⌊y⌋₊) ≤ 1 + Real.log y

Tactic:
refine (harmonic_le_one_add_log _).trans ?_

Result:
y : ℝ
hy : 1 ≤ y
⊢ 1 + Real.log ↑⌊y⌋₊ ≤ 1 + Real.log y

Proof state:
y : ℝ
hy : 1 ≤ y
⊢ 1 + Real.log ↑⌊y⌋₊ ≤ 1 + Real.log y

Tactic:
gcongr

Result:
case bc.hx
y : ℝ
hy : 1 ≤ y
⊢ 0 < ↑⌊y⌋₊

case bc.hxy
y : ℝ
hy : 1 ≤ y
⊢ ↑⌊y⌋₊ ≤ y

Proof state:
case bc.hxy
y : ℝ
hy : 1 ≤ y
⊢ ↑⌊y⌋₊ ≤ y

Tactic:
exact Nat.floor_le <| zero_le_one.trans hy

Result:
no goals

Proof state:
case bc.hx
y : ℝ
hy : 1 ≤ y
⊢ 0 < ↑⌊y⌋₊

Tactic:
exact_mod_cast Nat.floor_pos.mpr hy

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
    (h : m.WF) {hc : k' ∈ Const.modify m k f} :
    (Const.modify m k f).getKey k' hc =
      if k == k' then
        k
      else
        haveI h' : k' ∈ m := mem_modify h |>.mp hc
        m.getKey k' h'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
hc : k' ∈ modify m k f
⊢ (modify m k f).contains k' = true → (modify m k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp_to_raw using Raw₀.Const.getKey_modify

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
hc : k' ∈ modify m k f
⊢ (modify m k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
hc✝ : k' ∈ modify m k f
hc : (modify m k f).contains k' = true
⊢ (modify m k f).getKey k' hc✝ = if (k == k') = true then k else m.getKey k' ⋯

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
hc✝ : k' ∈ modify m k f
hc : (modify m k f).contains k' = true
⊢ (modify m k f).getKey k' hc✝ = if (k == k') = true then k else m.getKey k' ⋯

Tactic:
revert hc

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
hc : k' ∈ modify m k f
⊢ (modify m k f).contains k' = true → (modify m k f).getKey k' hc = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib/Analysis/Complex/Polynomial/UnitTrinomial.lean
theorem irreducible_of_coprime' (hp : IsUnitTrinomial p)
    (h : ∀ z : ℂ, ¬(aeval z p = 0 ∧ aeval z (mirror p) = 0)) : Irreducible p

Proof state:
case intro
q : ℤ[X]
this : ¬0 < q.natDegree
p : ℤ[X]
h : ∀ (z : ℂ), ¬((aeval z) (q * p) = 0 ∧ (aeval z) (q * p).mirror = 0)
hq' : q ∣ (q * p).mirror
hp : IsUnit (q.leadingCoeff * p.leadingCoeff)
⊢ IsUnit q

Tactic:
replace hp := isUnit_of_mul_isUnit_left hp

Result:
case intro
q : ℤ[X]
this : ¬0 < q.natDegree
p : ℤ[X]
h : ∀ (z : ℂ), ¬((aeval z) (q * p) = 0 ∧ (aeval z) (q * p).mirror = 0)
hq' : q ∣ (q * p).mirror
hp : IsUnit q.leadingCoeff
⊢ IsUnit q
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDeriv_one_apply (m : Fin 1 → E) :
    iteratedFDeriv 𝕜 1 f x m = fderiv 𝕜 f x (m 0)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
⊢ (iteratedFDeriv 𝕜 1 f x) m = (fderiv 𝕜 f x) (m 0)

Tactic:
rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
⊢ (fderiv 𝕜 f x) (m (last 0)) = (fderiv 𝕜 f x) (m 0)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
⊢ (fderiv 𝕜 f x) (m (last 0)) = (fderiv 𝕜 f x) (m 0)

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem Monoid.fg_of_surjective {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M')
    (hf : Function.Surjective f) : Monoid.FG M'

Proof state:
case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure ↑(Finset.image (⇑f) s) = ⊤

Tactic:
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
  MonoidHom.mrange_eq_top]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
⊢ FG M'

Tactic:
obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›

Result:
case intro
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ FG M'

Proof state:
case intro
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ FG M'

Tactic:
use s.image f

Result:
case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure ↑(Finset.image (⇑f) s) = ⊤

Proof state:
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
⊢ FG M'

Tactic:
classical
  obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
  use s.image f
  rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
    MonoidHom.mrange_eq_top]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_add_pi_div_two (x : ℂ) : cos (x + π / 2) = -sin x

Proof state:
x : ℂ
⊢ cos (x + ↑π / 2) = -sin x

Tactic:
simp [cos_add]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_le_rng {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃)
    (h₂ : Continuous[t₁, t₂] f) : Continuous[t₁, t₃] f

Proof state:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃

Tactic:
exact le_trans h₂ h₁

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : Continuous f
⊢ Continuous f

Tactic:
rw [continuous_iff_coinduced_le] at h₂ ⊢

Result:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : coinduced f t₁ ≤ t₂
⊢ coinduced f t₁ ≤ t₃
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem getElem?_zipIdx (l : Array α) (n m) : (zipIdx l n)[m]? = l[m]?.map fun a => (a, n + m)

Proof state:
α : Type u_1
l : Array α
n m : Nat
⊢ (l.zipIdx n)[m]? = Option.map (fun a => (a, n + m)) l[m]?

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_le_succ (h : a ≤ b) : succ a ≤ succ b

Proof state:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b

Tactic:
exact (hb <| hba.trans <| le_succ _).trans (le_succ _)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b

Tactic:
by_cases hba : b ≤ a

Result:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ succ a ≤ succ b

Tactic:
by_cases hb : IsMax b

Result:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b

Proof state:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ a < succ b

Tactic:
apply lt_succ_of_le_of_not_isMax h hb

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b

Tactic:
rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]

Result:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ a < succ b

Proof state:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b

Tactic:
exact succ_le_of_lt ((h.lt_of_not_le hba).trans_le <| le_succ b)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
theorem cotangent_subsingleton_iff : Subsingleton I.Cotangent ↔ IsIdempotentElem I

Proof state:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
H : Subsingleton I.Cotangent
⊢ I ≤ I ^ 2

Tactic:
exact fun x hx => (I.toCotangent_eq_zero ⟨x, hx⟩).mp (Subsingleton.elim _ _)

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Subsingleton I.Cotangent → IsIdempotentElem I

Tactic:
intro H

Result:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
H : Subsingleton I.Cotangent
⊢ IsIdempotentElem I

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Subsingleton I.Cotangent ↔ IsIdempotentElem I

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Subsingleton I.Cotangent → IsIdempotentElem I

case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton I.Cotangent

Proof state:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
H : Subsingleton I.Cotangent
⊢ IsIdempotentElem I

Tactic:
refine (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) ?_)

Result:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
H : Subsingleton I.Cotangent
⊢ I ≤ I ^ 2

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton I.Cotangent

Tactic:
exact fun e =>
  ⟨fun x y =>
    Quotient.inductionOn₂' x y fun x y =>
      I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Polynomial.lean
theorem aeval_mem_adjoin_singleton :
    aeval x p ∈ Algebra.adjoin R {x}

Proof state:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
x : A
⊢ (aeval x) p ∈ Algebra.adjoin R {x}

Tactic:
simpa only [Algebra.adjoin_singleton_eq_range_aeval] using Set.mem_range_self p

Result:
no goals