harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_succ' : mkArray (n + 1) a = #[a] ++ mkArray n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ mkArray (n + 1) a = #[a] ++ mkArray n a

Tactic:
apply Array.ext'

Result:
case h
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray (n + 1) a).toList = (#[a] ++ mkArray n a).toList

Proof state:
case h
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray (n + 1) a).toList = (#[a] ++ mkArray n a).toList

Tactic:
simp [List.replicate_succ]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma IndepFun_iff_Indep [mβ : MeasurableSpace β]
    [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) :
    IndepFun f g μ ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ

Proof state:
Ω : Type u_1
β : Type u_3
γ : Type u_4
x✝ : MeasurableSpace Ω
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
⊢ IndepFun f g μ ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ

Tactic:
simp only [IndepFun, Indep, Kernel.IndepFun]

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem _root_.MeasureTheory.Integrable.condDistrib_ae_map
    (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
    ∀ᵐ b ∂μ.map X, Integrable (fun ω => f (b, ω)) (condDistrib Y X μ b)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂Measure.map X μ, Integrable (fun ω => f (b, ω)) ((condDistrib Y X μ) b)

Tactic:
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂(Measure.map (fun a => (X a, Y a)) μ).fst,
    Integrable (fun ω => f (b, ω)) ((Measure.map (fun a => (X a, Y a)) μ).condKernel b)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂(Measure.map (fun a => (X a, Y a)) μ).fst,
    Integrable (fun ω => f (b, ω)) ((Measure.map (fun a => (X a, Y a)) μ).condKernel b)

Tactic:
exact hf_int.condKernel_ae

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem getElem?_zero_flatten (L : Vector (Vector α m) n) :
    (flatten L)[0]? = L.findSome? fun l => l[0]?

Proof state:
case of
α : Type u_1
m n : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten[0]? =
    findSome? (fun l => l[0]?)
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }

Tactic:
simp [Array.getElem?_zero_flatten, Array.findSome?_map, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
⊢ L.flatten[0]? = findSome? (fun l => l[0]?) L

Tactic:
cases L using vector₂_induction

Result:
case of
α : Type u_1
m n : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten[0]? =
    findSome? (fun l => l[0]?)
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_erase [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} :
    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
fallback : β a
⊢ (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback

Tactic:
simp_to_raw using Raw₀.getD_erase

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem differentiableAt_norm_smul (ht : t ≠ 0) :
    DifferentiableAt ℝ (‖·‖) x ↔ DifferentiableAt ℝ (‖·‖) (t • x) where
  mp hd := (hd.hasFDerivAt.hasFDerivAt_norm_smul ht).differentiableAt
  mpr hd

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
ht : t ≠ 0
hd : DifferentiableAt ℝ (fun x => ‖x‖) (t • x)
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
convert (hd.hasFDerivAt.hasFDerivAt_norm_smul (inv_ne_zero ht)).differentiableAt

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
ht : t ≠ 0
hd : DifferentiableAt ℝ (fun x => ‖x‖) (t • x)
⊢ x = t⁻¹ • t • x

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
ht : t ≠ 0
hd : DifferentiableAt ℝ (fun x => ‖x‖) (t • x)
⊢ x = t⁻¹ • t • x

Tactic:
rw [smul_smul, inv_mul_cancel₀ ht, one_smul]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem comap_mulLeft_nhdsGT_zero {x : 𝕜} (hx : 0 < x) : comap (x * ·) (𝓝[>] 0) = 𝓝[>] 0

Proof state:
case e_a
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ 𝓝 ((Homeomorph.mulLeft₀ x ⋯).symm 0) = 𝓝 0

Tactic:
simp

Result:
no goals

Proof state:
case e_a
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) = 𝓝 0

Tactic:
refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_

Result:
case e_a
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ 𝓝 ((Homeomorph.mulLeft₀ x ⋯).symm 0) = 𝓝 0

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝[>] 0) = 𝓝[>] 0

Tactic:
rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi _ hx, zero_div]

Result:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0) = 𝓝 0 ⊓ 𝓟 (Ioi 0)

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0) = 𝓝 0 ⊓ 𝓟 (Ioi 0)

Tactic:
congr 1

Result:
case e_a
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) = 𝓝 0
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem totalDegree_neg (a : MvPolynomial σ R) : (-a).totalDegree = a.totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
a : MvPolynomial σ R
⊢ (-a).totalDegree = a.totalDegree

Tactic:
simp only [totalDegree, support_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem get?_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α} :
    m.get? a = Raw₀.get? ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
h : m.WF
a : α
⊢ m.get? a = Raw₀.get? ⟨m, ⋯⟩ a

Tactic:
simp [Raw.get?, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumsphere_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V]
    (hd : finrank ℝ V = n) (hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n}
    (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) :
    sx₁.circumsphere = sx₂.circumsphere

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rcases exists_circumsphere_eq_of_cospherical hd hc with ⟨r, hr⟩

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem continuous_iff_isClosed : Continuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s) :=
  continuous_def.trans <| compl_surjective.forall.trans <| by
    simp only [isOpen_compl_iff, preimage_compl]

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (x : Set Y), IsOpen xᶜ → IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s)

Tactic:
simp only [isOpen_compl_iff, preimage_compl]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem liftOn_condition_of_liftOn'_condition {P : Sort v} {f : K[X] → K[X] → P}
    (H : ∀ {p q a} (_ : q ≠ 0) (_ha : a ≠ 0), f (a * p) (a * q) = f p q) ⦃p q p' q' : K[X]⦄
    (hq : q ≠ 0) (hq' : q' ≠ 0) (h : q' * p = q * p') : f p q = f p' q' :=
  calc
    f p q = f (q' * p) (q' * q) := (H hq hq').symm
    _ = f (q * p') (q * q')

Proof state:
K : Type u
inst✝ : CommRing K
P : Sort v
f : K[X] → K[X] → P
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
h : q' * p = q * p'
⊢ f (q' * p) (q' * q) = f (q * p') (q * q')

Tactic:
rw [h, mul_comm q']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem succ_mul_succ_eq (a b : Nat) : succ a * succ b = a * b + a + b + 1

Proof state:
a b : Nat
⊢ a * b + b + a.succ = a * b + b + a + 1

Tactic:
rfl

Result:
no goals

Proof state:
a b : Nat
⊢ a.succ * b.succ = a * b + a + b + 1

Tactic:
rw [mul_succ, succ_mul, Nat.add_right_comm _ a]

Result:
a b : Nat
⊢ a * b + b + a.succ = a * b + b + a + 1
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousAt_finite [Finite ι] {F : ι → X → α} {x₀ : X} :
    EquicontinuousAt F x₀ ↔ ∀ i, ContinuousAt (F i) x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst✝ : Finite ι
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ (i : ι), ContinuousAt (F i) x₀

Tactic:
simp [EquicontinuousAt, ContinuousAt, (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff,
  UniformSpace.ball, @forall_swap _ ι]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
theorem comap_apply₀ (f : α → β) (μ : Measure β) (hfi : Injective f)
    (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ)
    (hs : NullMeasurableSet s (comap f μ)) : comap f μ s = μ (f '' s)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ (comap f μ) s = μ (f '' s)

Tactic:
rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢

Result:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯)
⊢ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s = μ (f '' s)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯)
⊢ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s = μ (f '' s)

Tactic:
rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ioi {a : α} (ha : 0 ≤ a) : (Nat.cast : ℕ → α) ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ Nat.cast ⁻¹' Ioi a = Ioi ⌊a⌋₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋₊

Tactic:
simp [floor_lt, ha]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc (attr := simp)]
lemma Opens.fromSpecStalkOfMem_ι {X : Scheme.{u}} (U : X.Opens) (x : X) (hxU : x ∈ U) :
    U.fromSpecStalkOfMem x hxU ≫ U.ι = X.fromSpecStalk x

Proof state:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).fromSpecStalk ⟨x, hxU⟩ ≫ U.ι = Spec.map (Hom.stalkMap U.ι ⟨x, hxU⟩) ≫ X.fromSpecStalk x

Tactic:
exact (Scheme.Spec_map_stalkMap_fromSpecStalk U.ι (x := ⟨x, hxU⟩)).symm

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.ι = X.fromSpecStalk x

Tactic:
simp only [Opens.fromSpecStalkOfMem, Spec.map_inv, Category.assoc, IsIso.inv_comp_eq]

Result:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).fromSpecStalk ⟨x, hxU⟩ ≫ U.ι = Spec.map (Hom.stalkMap U.ι ⟨x, hxU⟩) ≫ X.fromSpecStalk x
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem Subalgebra.eq_bot_of_isPurelyInseparable_of_isSeparable (L : Subalgebra F E)
    [IsPurelyInseparable F L] [Algebra.IsSeparable F L] : L = ⊥ := bot_unique fun x hx ↦ by
  obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
  exact ⟨y, congr_arg (Subalgebra.val _) hy⟩

Proof state:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Ring E
inst✝² : Algebra F E
L : Subalgebra F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩

Result:
case intro
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Ring E
inst✝² : Algebra F E
L : Subalgebra F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Ring E
inst✝² : Algebra F E
L : Subalgebra F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥

Tactic:
exact ⟨y, congr_arg (Subalgebra.val _) hy⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_congr {as bs : Array α} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g)
     {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') :
    as.foldl f a start stop = bs.foldl g b start' stop'

Proof state:
α : Type u_1
β : Type u_2
as bs : Array α
h₀ : as = bs
f g : β → α → β
h₁ : f = g
a b : β
h₂ : a = b
start start' stop stop' : Nat
h₃ : start = start'
h₄ : stop = stop'
⊢ foldl f a as start stop = foldl g b bs start' stop'

Tactic:
congr

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_lt_univ' (c : Cardinal) : lift.{max (u + 1) v, u} c < univ.{u, v}

Proof state:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
rw [lift_lift, lift_univ, univ_umax.{u,v}] at this

Result:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Proof state:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
exact this

Result:
no goals

Proof state:
c : Cardinal.{u}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
have := lift_lt.{_, max (u+1) v}.2 (lift_lt_univ c)

Result:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getDₘ_eq_getValueCastD [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
    (hm : Raw.WFImp m.1) {a : α} {fallback : β a} :
    m.getDₘ a fallback = getValueCastD a (toListModel m.1.buckets) fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
fallback : β a
⊢ m.getDₘ a fallback = getValueCastD a (toListModel m.val.buckets) fallback

Tactic:
rw [getDₘ, get?ₘ_eq_getValueCast? hm, List.getValueCastD_eq_getValueCast?]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma mul_div_cancel_of_imp (h : b = 0 → a = 0) : a * b / b = a

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a * b / b = a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;>  simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_apply (A : Matrix n n α) (i j : n) :
    adjugate A i j = (A.updateRow j (Pi.single i 1)).det

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ A.adjugate i j = (A.updateRow j (Pi.single i 1)).det

Tactic:
rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_transpose]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioo_bot : (some : α → WithBot α) ⁻¹' Ioo ⊥ a = Iio a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ioo ⊥ ↑a = Iio a

Tactic:
simp [← Ioi_inter_Iio]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sub_sinh : cosh x - sinh x = exp (-x)

Proof state:
x : ℂ
⊢ cosh x - sinh x = cexp (-x)

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem prod_eq_top_iff [Nonempty M] [Nonempty N] {s : Subsemigroup M} {t : Subsemigroup N} :
    s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : Nonempty M
inst✝ : Nonempty N
s : Subsemigroup M
t : Subsemigroup N
⊢ s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Tactic:
simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← srange_eq_map, srange_fst,
  srange_snd]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem preimage_sphere (h : α ≃ᵢ β) (x : β) (r : ℝ) :
    h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r

Tactic:
rw [← h.isometry.preimage_sphere (h.symm x) r, h.apply_symm_apply]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_union_inter_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) :
    image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t

Proof state:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t

Tactic:
rw [image2_comm hf]

Result:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Proof state:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
exact image2_inter_union_subset hf

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.sub [AddGroup α] {A B : Matrix n n α} (ha : A.IsDiag) (hb : B.IsDiag) :
    (A - B).IsDiag

Proof state:
α : Type u_1
n : Type u_4
inst✝ : AddGroup α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
⊢ (A - B).IsDiag

Tactic:
intro i j h

Result:
α : Type u_1
n : Type u_4
inst✝ : AddGroup α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A - B) i j = 0

Proof state:
α : Type u_1
n : Type u_4
inst✝ : AddGroup α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A - B) i j = 0

Tactic:
simp [ha h, hb h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem cos_angle_add_angle_sub_add_angle_sub_eq_neg_one {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1

Tactic:
rw [add_assoc, Real.cos_add, cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle hx hy,
  sin_angle_sub_add_angle_sub_rev_eq_sin_angle hx hy, mul_neg, ← neg_add', add_comm, ← sq, ← sq,
  Real.sin_sq_add_cos_sq]

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.gcd_mul_right_cancel_right (m : ℕ+) {n k : ℕ+} :
    k.Coprime m → m.gcd (n * k) = m.gcd n

Proof state:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (k * n) = m.gcd n

Tactic:
apply Coprime.gcd_mul_left_cancel_right

Result:
no goals

Proof state:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (n * k) = m.gcd n

Tactic:
rw [mul_comm]

Result:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (k * n) = m.gcd n