harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Control.lean
theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p

Proof state:
α : Type
p : α → Bool
as : List α
⊢ findM? p as = find? p as

Tactic:
induction as with
| nil => rfl
| cons a as ih =>
  simp only [findM?, find?]
  cases p a with
  | true  => rfl
  | false => rw [ih]; rfl

Result:
no goals

Proof state:
case cons.true
α : Type
p : α → Bool
a : α
as : List α
ih : findM? p as = find? p as
⊢ (do
      let __do_lift ← true
      match __do_lift with
        | true => pure (some a)
        | false => findM? p as) =
    match true with
    | true => some a
    | false => find? p as

Tactic:
rfl

Result:
no goals

Proof state:
case cons.false
α : Type
p : α → Bool
a : α
as : List α
ih : findM? p as = find? p as
⊢ (do
      let __do_lift ← false
      match __do_lift with
        | true => pure (some a)
        | false => findM? p as) =
    match false with
    | true => some a
    | false => find? p as

Tactic:
rw [ih]

Result:
case cons.false
α : Type
p : α → Bool
a : α
as : List α
ih : findM? p as = find? p as
⊢ (do
      let __do_lift ← false
      match __do_lift with
        | true => pure (some a)
        | false => find? p as) =
    match false with
    | true => some a
    | false => find? p as

Proof state:
case cons
α : Type
p : α → Bool
a : α
as : List α
ih : findM? p as = find? p as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => findM? p as) =
    match p a with
    | true => some a
    | false => find? p as

Tactic:
cases p a with
| true  => rfl
| false => rw [ih]; rfl

Result:
no goals

Proof state:
case cons.false
α : Type
p : α → Bool
a : α
as : List α
ih : findM? p as = find? p as
⊢ (do
      let __do_lift ← false
      match __do_lift with
        | true => pure (some a)
        | false => find? p as) =
    match false with
    | true => some a
    | false => find? p as

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type
p : α → Bool
⊢ findM? p [] = find? p []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type
p : α → Bool
a : α
as : List α
ih : findM? p as = find? p as
⊢ findM? p (a :: as) = find? p (a :: as)

Tactic:
simp only [findM?, find?]

Result:
case cons
α : Type
p : α → Bool
a : α
as : List α
ih : findM? p as = find? p as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => findM? p as) =
    match p a with
    | true => some a
    | false => find? p as
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem of_le_add {f : α → ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y) :
    LipschitzOnWith 1 f s :=
  LipschitzOnWith.of_le_add_mul 1 <| by simpa only [NNReal.coe_one, one_mul]

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
f : α → ℝ
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y
⊢ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul]

Result:
no goals
-- Mathlib/Topology/Order/Hom/Esakia.lean
theorem cancel_left {g : PseudoEpimorphism β γ} {f₁ f₂ : PseudoEpimorphism α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
theorem N₁Γ₀_hom_app (K : ChainComplex C ℕ) :
    N₁Γ₀.hom.app K = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫
        (toKaroubi _).map (Γ₀NondegComplexIso K).hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.hom.app K =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Tactic:
change (N₁Γ₀.app K).hom = _

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Tactic:
simp only [N₁Γ₀_app]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
    eraseIdx (l ++ l') k = eraseIdx l k ++ l'

Proof state:
case cons.succ
α : Type u_1
l' : List α
x : α
l : List α
ih : ∀ {k : Nat}, k < l.length → (l ++ l').eraseIdx k = l.eraseIdx k ++ l'
k : Nat
hk : k + 1 < (x :: l).length
⊢ (x :: l ++ l').eraseIdx (k + 1) = (x :: l).eraseIdx (k + 1) ++ l'

Tactic:
simp_all [eraseIdx_cons_succ, Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
l' : List α
x : α
l : List α
ih : ∀ {k : Nat}, k < l.length → (l ++ l').eraseIdx k = l.eraseIdx k ++ l'
hk : 0 < (x :: l).length
⊢ (x :: l ++ l').eraseIdx 0 = (x :: l).eraseIdx 0 ++ l'

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : List α
k : Nat
hk : k < l.length
l' : List α
⊢ (l ++ l').eraseIdx k = l.eraseIdx k ++ l'

Tactic:
induction l generalizing k with
| nil => simp_all
| cons x l ih =>
  cases k with
  | zero => rfl
  | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case nil
α : Type u_1
l' : List α
k : Nat
hk : k < [].length
⊢ ([] ++ l').eraseIdx k = [].eraseIdx k ++ l'

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
l' : List α
x : α
l : List α
ih : ∀ {k : Nat}, k < l.length → (l ++ l').eraseIdx k = l.eraseIdx k ++ l'
k : Nat
hk : k < (x :: l).length
⊢ (x :: l ++ l').eraseIdx k = (x :: l).eraseIdx k ++ l'

Tactic:
cases k with
| zero => rfl
| succ k => simp_all [eraseIdx_cons_succ, Nat.succ_lt_succ_iff]

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem definable_univ : A.Definable L (univ : Set (α → M)) :=
  ⟨⊤, by
    ext
    simp⟩

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ univ = setOf ⊤.Realize

Tactic:
ext

Result:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ univ ↔ x✝ ∈ setOf ⊤.Realize

Proof state:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ univ ↔ x✝ ∈ setOf ⊤.Realize

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem mem_jacobson_bot {x : R} : x ∈ jacobson (⊥ : Ideal R) ↔ ∀ y, IsUnit (x * y + 1) :=
  ⟨fun hx y =>
    let ⟨z, hz⟩ := (mem_jacobson_iff.1 hx) y
    isUnit_iff_exists_inv.2
      ⟨z, by rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]⟩,
    fun h =>
    mem_jacobson_iff.mpr fun y =>
      let ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (h y)
      ⟨b, (Submodule.mem_bot R).2 (hb ▸ by ring)⟩⟩

Proof state:
R : Type u
inst✝ : CommRing R
x : R
hx : x ∈ ⊥.jacobson
y z : R
hz : z * y * x + z - 1 ∈ ⊥
⊢ (x * y + 1) * z = 1

Tactic:
rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x : R
h : ∀ (y : R), IsUnit (x * y + 1)
y b : R
hb : (x * y + 1) * b = 1
⊢ b * y * x + b - (x * y + 1) * b = 0

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mker_inr : mker (inr M N) = ⊥

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inr M N) = ⊥

Tactic:
ext x

Result:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : N
⊢ x ∈ mker (inr M N) ↔ x ∈ ⊥

Proof state:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : N
⊢ x ∈ mker (inr M N) ↔ x ∈ ⊥

Tactic:
simp [mem_mker]

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem three_lt_four_mul_im_sq_of_mem_fdo (h : z ∈ 𝒟ᵒ) : 3 < 4 * z.im ^ 2

Proof state:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 3 < 4 * z.im ^ 2

Tactic:
have : 1 < z.re * z.re + z.im * z.im := by simpa [Complex.normSq_apply] using h.1

Result:
z : ℍ
h : z ∈ 𝒟ᵒ
this : 1 < z.re * z.re + z.im * z.im
⊢ 3 < 4 * z.im ^ 2

Proof state:
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
⊢ 3 < 4 * z.im ^ 2

Tactic:
cases abs_cases z.re <;> nlinarith

Result:
no goals

Proof state:
z : ℍ
h : z ∈ 𝒟ᵒ
this : 1 < z.re * z.re + z.im * z.im
⊢ 3 < 4 * z.im ^ 2

Tactic:
have := h.2

Result:
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
⊢ 3 < 4 * z.im ^ 2

Proof state:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ 1 < z.re * z.re + z.im * z.im

Tactic:
simpa [Complex.normSq_apply] using h.1

Result:
no goals
-- Mathlib/Topology/Germ.lean
theorem forall_restrictGermPredicate_iff {P : ∀ x : X, Germ (𝓝 x) Y → Prop} :
    (∀ x, RestrictGermPredicate P A x f) ↔ ∀ᶠ x in 𝓝ˢ A, P x f

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
⊢ (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f

Tactic:
rw [eventually_nhdsSet_iff_forall]

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
⊢ (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
⊢ (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Bousfield.lean
lemma W_iff_isIso {X Y : C} (f : X ⟶ Y) (hX : P X) (hY : P Y) :
    W P f ↔ IsIso f

Proof state:
case mp.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : W P f
g : Y ⟶ X
hg : (fun g => f ≫ g) g = 𝟙 X
⊢ IsIso f

Tactic:
exact ⟨g, hg, (hf _ hY).1 (by simp only [reassoc_of% hg, comp_id])⟩

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : W P f
⊢ IsIso f

Tactic:
obtain ⟨g, hg⟩ := (hf _ hX).2 (𝟙 X)

Result:
case mp.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : W P f
g : Y ⟶ X
hg : (fun g => f ≫ g) g = 𝟙 X
⊢ IsIso f

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ W P f → IsIso f

Tactic:
intro hf

Result:
case mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : W P f
⊢ IsIso f

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ W P f ↔ IsIso f

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ W P f → IsIso f

case mpr
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ IsIso f → W P f

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : W P f
g : Y ⟶ X
hg : (fun g => f ≫ g) g = 𝟙 X
⊢ (fun g => f ≫ g) (g ≫ f) = (fun g => f ≫ g) (𝟙 Y)

Tactic:
simp only [reassoc_of% hg, comp_id]

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
⊢ IsIso f → W P f

Tactic:
apply W_of_isIso

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem OrthogonalFamily.projection_directSum_coeAddHom [DecidableEq ι] {V : ι → Submodule 𝕜 E}
    (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (x : ⨁ i, V i) (i : ι)
    [CompleteSpace (V i)] :
    orthogonalProjection (V i) (DirectSum.coeAddMonoidHom V x) = x i

Proof state:
case H_basic.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x : ↥(V i)
⊢ (orthogonalProjection (V i)) ↑x = (DFinsupp.single i x) i

Tactic:
rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem hasSum_fourier_series_of_summable (h : Summable (fourierCoeff f)) :
    HasSum (fun i => fourierCoeff f i • fourier i) f

Proof state:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (↑↑((toLp 2 haarAddCircle ℂ) f)) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f

Tactic:
simp_rw [fourierCoeff_toLp] at sum_L2

Result:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f

Proof state:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
⊢ HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f

Tactic:
have sum_L2 := hasSum_fourier_series_L2 (toLp (E := ℂ) 2 haarAddCircle ℂ f)

Result:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (↑↑((toLp 2 haarAddCircle ℂ) f)) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f

Proof state:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun a => ‖fourierCoeff (⇑f) a • fourier a‖

Tactic:
simp_rw [norm_smul, fourier_norm, mul_one]

Result:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun a => ‖fourierCoeff (⇑f) a‖

Proof state:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun a => ‖fourierCoeff (⇑f) a‖

Tactic:
exact h.norm

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f

Tactic:
refine ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2

Result:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun a => ‖fourierCoeff (⇑f) a • fourier a‖
-- Mathlib/RingTheory/Algebraic/Basic.lean
lemma IsAlgebraic.inv_iff {K} [Field K] [Algebra R K] {x : K} :
    IsAlgebraic R (x⁻¹) ↔ IsAlgebraic R x

Proof state:
case pos
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : x = 0
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
simp [hx]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
by_cases hx : x = 0

Result:
case pos
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : x = 0
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

case neg
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : ¬x = 0
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Proof state:
case neg
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : ¬x = 0
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
letI := invertibleOfNonzero hx

Result:
case neg
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : ¬x = 0
this : Invertible x := invertibleOfNonzero hx
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Proof state:
case neg
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : ¬x = 0
this : Invertible x := invertibleOfNonzero hx
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
exact IsAlgebraic.invOf_iff (R := R) (x := x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β}
    (h : m.WF) : (Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback

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

Tactic:
simp only [mem_iff_contains]

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

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

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_modify_self

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
@[simp]
lemma isRkFinite_insert_iff {e : α} : M.IsRkFinite (insert e X) ↔ M.IsRkFinite X

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite (insert e X) ↔ M.IsRkFinite X

Tactic:
rw [← singleton_union, isRkFinite_singleton.isRkFinite_union_iff]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem ne_zero {a b c : ℤ} (h : Fermat42 a b c) : c ≠ 0

Proof state:
a b c : ℤ
h : Fermat42 a b c
⊢ a ^ 4 + b ^ 4 = (a ^ 2) ^ 2 + (b ^ 2) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case h
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < c ^ 2

Tactic:
rw [← h.2.2, (by ring : a ^ 4 + b ^ 4 = (a ^ 2) ^ 2 + (b ^ 2) ^ 2)]

Result:
case h
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < (a ^ 2) ^ 2 + (b ^ 2) ^ 2

Proof state:
case h
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < (a ^ 2) ^ 2 + (b ^ 2) ^ 2

Tactic:
exact
  add_pos (sq_pos_of_ne_zero (pow_ne_zero 2 h.1)) (sq_pos_of_ne_zero (pow_ne_zero 2 h.2.1))

Result:
no goals

Proof state:
a b c : ℤ
h : Fermat42 a b c
⊢ c ≠ 0

Tactic:
apply ne_zero_pow two_ne_zero _

Result:
a b c : ℤ
h : Fermat42 a b c
⊢ c ^ 2 ≠ 0

Proof state:
a b c : ℤ
h : Fermat42 a b c
⊢ c ^ 2 ≠ 0

Tactic:
apply ne_of_gt

Result:
case h
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < c ^ 2
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem gronwallBound_ε0 (δ K x : ℝ) : gronwallBound δ K 0 x = δ * exp (K * x)

Proof state:
case pos
δ K x : ℝ
hK : K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
simp only [gronwallBound_K0, hK, zero_mul, exp_zero, add_zero, mul_one]

Result:
no goals

Proof state:
δ K x : ℝ
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
by_cases hK : K = 0

Result:
case pos
δ K x : ℝ
hK : K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

case neg
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Proof state:
case neg
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
simp only [gronwallBound_of_K_ne_0 hK, zero_div, zero_mul, add_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma BoundaryLE.false_of_isTruncGE {j : ι} (hj : e.BoundaryLE j) [e.IsTruncGE] : False

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst✝ : e.IsTruncGE
⊢ False

Tactic:
obtain ⟨k, hk⟩ := e.mem_next hj.1

Result:
case intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst✝ : e.IsTruncGE
k : ι
hk : e.f k = c'.next (e.f j)
⊢ False

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst✝ : e.IsTruncGE
k : ι
hk : e.f k = c'.next (e.f j)
⊢ c'.Rel (e.f j) (e.f k)

Tactic:
simpa only [hk] using hj.1

Result:
no goals

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
inst✝ : e.IsTruncGE
k : ι
hk : e.f k = c'.next (e.f j)
⊢ False

Tactic:
exact hj.2 k (by simpa only [hk] using hj.1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {l : Vector α n} :
    (x, k + i) ∈ zipIdx l k ↔ l[i]? = some x

Proof state:
α : Type u_1
n k i : Nat
x : α
l : Vector α n
⊢ (x, k + i) ∈ l.zipIdx k ↔ l[i]? = some x

Tactic:
simp [mem_iff_getElem?, and_left_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_le_Lp_mul_Lq (μ : Measure α) {p q : ℝ} (hpq : p.IsConjExponent q)
    {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    (∫⁻ a, (f * g) a ∂μ) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ q ∂μ) ^ (1 / q)

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ⊤
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
rw [mul_comm, mul_comm ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p))]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ⊤
⊢ ∫⁻ (a : α), (g * f) a ∂μ ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_top : ∫⁻ (a : α), g a ^ q ∂μ = ⊤
⊢ ∫⁻ (a : α), (g * f) a ∂μ ≤ (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p)

Tactic:
exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.symm.pos hpq.nonneg hg_top hf_zero

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ¬∫⁻ (a : α), g a ^ q ∂μ = 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ = ⊤
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
exact lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top hpq.pos hpq.symm.nonneg hf_top hg_zero

Result:
no goals