harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem span_X_isPrime : (Ideal.span ({X} : Set R⟦X⟧)).IsPrime

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Ideal.span {X} = RingHom.ker (constantCoeff R)

Tactic:
apply Ideal.ext

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ∀ (x : R⟦X⟧), x ∈ Ideal.span {X} ↔ x ∈ RingHom.ker (constantCoeff R)

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ∀ (x : R⟦X⟧), x ∈ Ideal.span {X} ↔ x ∈ RingHom.ker (constantCoeff R)

Tactic:
intro φ

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ : R⟦X⟧
⊢ φ ∈ Ideal.span {X} ↔ φ ∈ RingHom.ker (constantCoeff R)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
this : Ideal.span {X} = RingHom.ker (constantCoeff R)
⊢ (RingHom.ker (constantCoeff R)).IsPrime

Tactic:
exact RingHom.ker_isPrime _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (Ideal.span {X}).IsPrime

Tactic:
suffices Ideal.span ({X} : Set R⟦X⟧) = RingHom.ker (constantCoeff R) by
  rw [this]
  exact RingHom.ker_isPrime _

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Ideal.span {X} = RingHom.ker (constantCoeff R)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
this : Ideal.span {X} = RingHom.ker (constantCoeff R)
⊢ (Ideal.span {X}).IsPrime

Tactic:
rw [this]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
this : Ideal.span {X} = RingHom.ker (constantCoeff R)
⊢ (RingHom.ker (constantCoeff R)).IsPrime

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ : R⟦X⟧
⊢ φ ∈ Ideal.span {X} ↔ φ ∈ RingHom.ker (constantCoeff R)

Tactic:
rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]

Result:
no goals
-- Mathlib/Algebra/Module/Rat.lean
theorem map_ratCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [DivisionRing R] [DivisionRing S] [Module R M]
    [Module S M₂] (c : ℚ) (x : M) :
    f ((c : R) • x) = (c : S) • f x

Proof state:
M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ f (↑c • x) = ↑c • f x

Tactic:
rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
  map_intCast_smul f R S, map_inv_natCast_smul f R S]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem valuation_compare (f : K⸨X⸩) :
    (Valued.v : (RatFuncAdicCompl K) → ℤₘ₀)
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg f) =
      Valued.v f

Proof state:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f

Tactic:
rw [← valuation_LaurentSeries_equal_extension, ← compare_comp_eq_compare
  (pkg := ratfuncAdicComplPkg) (cont_f := Valued.continuous_valuation)]

Result:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) =
    (⋯.extend ⇑Valued.v ∘ (LaurentSeriesPkg K).compare ratfuncAdicComplPkg) f

case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ ∀ (a : ratfuncAdicComplPkg.space),
    Tendsto (⇑Valued.v) (comap ratfuncAdicComplPkg.coe (𝓝 a)) (𝓝 (⋯.extend (⇑Valued.v) a))

Proof state:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) =
    (⋯.extend ⇑Valued.v ∘ (LaurentSeriesPkg K).compare ratfuncAdicComplPkg) f

Tactic:
rfl

Result:
no goals

Proof state:
case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ ∀ (a : ratfuncAdicComplPkg.space),
    Tendsto (⇑Valued.v) (comap ratfuncAdicComplPkg.coe (𝓝 a)) (𝓝 (⋯.extend (⇑Valued.v) a))

Tactic:
exact (tendsto_valuation K)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_append (s m n step : Nat) :
    range' s m step ++ range' (s + step * m) n step = range' s (m + n) step

Proof state:
s m n step : Nat
⊢ range' s m step ++ range' (s + step * m) n step = range' s (m + n) step

Tactic:
rw [← toArray_inj]

Result:
s m n step : Nat
⊢ (range' s m step ++ range' (s + step * m) n step).toArray = (range' s (m + n) step).toArray

Proof state:
s m n step : Nat
⊢ (range' s m step ++ range' (s + step * m) n step).toArray = (range' s (m + n) step).toArray

Tactic:
simp [Array.range'_append]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem trans_transPartialHomeomorph (e : X ≃ₜ Y) (e' : Y ≃ₜ Z) (f'' : PartialHomeomorph Z Z') :
    (e.trans e').transPartialHomeomorph f'' =
      e.transPartialHomeomorph (e'.transPartialHomeomorph f'')

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : X ≃ₜ Y
e' : Y ≃ₜ Z
f'' : PartialHomeomorph Z Z'
⊢ (e.trans e').transPartialHomeomorph f'' = e.transPartialHomeomorph (e'.transPartialHomeomorph f'')

Tactic:
simp only [transPartialHomeomorph_eq_trans, PartialHomeomorph.trans_assoc,
  trans_toPartialHomeomorph]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem right_ne_of_oangle_ne_zero {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ ≠ 0) : p₃ ≠ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ ≠ p₂

Tactic:
rw [← @vsub_ne_zero V]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ -ᵥ p₂ ≠ 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ -ᵥ p₂ ≠ 0

Tactic:
exact o.right_ne_zero_of_oangle_ne_zero h

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem chartAt_inclusion_symm_eventuallyEq {U V : Opens M} (hUV : U ≤ V) {x : U} :
    (chartAt H (Opens.inclusion hUV x)).symm
    =ᶠ[𝓝 (chartAt H (Opens.inclusion hUV x) (Set.inclusion hUV x))]
    Opens.inclusion hUV ∘ (chartAt H x).symm

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)

Tactic:
apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑e ↑x ∈ (e.subtypeRestr ⋯).target

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑e ↑x ∈ (e.subtypeRestr ⋯).target

Tactic:
exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (Set.inclusion hUV x))]
    inclusion hUV ∘ ↑(chartAt H x).symm

Tactic:
have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
  apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
  exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)
⊢ ↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (Set.inclusion hUV x))]
    inclusion hUV ∘ ↑(chartAt H x).symm

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 (↑e ↑x)
⊢ ↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (Set.inclusion hUV x))]
    inclusion hUV ∘ ↑(chartAt H x).symm

Tactic:
exact Filter.eventuallyEq_of_mem heUx_nhds <| e.subtypeRestr_symm_eqOn_of_le ⟨x⟩
  ⟨Opens.inclusion hUV x⟩ hUV

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ ↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (Set.inclusion hUV x))]
    inclusion hUV ∘ ↑(chartAt H x).symm

Tactic:
set e := chartAt H (x : M)

Result:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : PartialHomeomorph M H := chartAt H ↑x
⊢ ↑(chartAt H (inclusion hUV x)).symm =ᶠ[𝓝 (↑(chartAt H (inclusion hUV x)) (Set.inclusion hUV x))]
    inclusion hUV ∘ ↑(chartAt H x).symm
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem zero_power_le (c : Cardinal.{u}) : (0 : Cardinal.{u}) ^ c ≤ 1

Proof state:
case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ≤ 1

Tactic:
apply zero_le

Result:
no goals

Proof state:
case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1

Tactic:
rw [zero_power h]

Result:
case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ≤ 1

Proof state:
c : Cardinal.{u}
⊢ 0 ^ c ≤ 1

Tactic:
by_cases h : c = 0

Result:
case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1

case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1

Proof state:
case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1

Tactic:
rw [h, power_zero]

Result:
no goals
-- Mathlib/Topology/LocallyFinite.lean
theorem comp_injOn {g : ι' → ι} (hf : LocallyFinite f) (hg : InjOn g { i | (f (g i)).Nonempty }) :
    LocallyFinite (f ∘ g) := fun x => by
  let ⟨t, htx, htf⟩ := hf x
  refine ⟨t, htx, htf.preimage <| ?_⟩
  exact hg.mono fun i (hi : Set.Nonempty _) => hi.left

Proof state:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
⊢ ∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite

Tactic:
let ⟨t, htx, htf⟩ := hf x

Result:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : {i | (f i ∩ t).Nonempty}.Finite
⊢ ∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite

Proof state:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : {i | (f i ∩ t).Nonempty}.Finite
⊢ InjOn g (g ⁻¹' {i | (f i ∩ t).Nonempty})

Tactic:
exact hg.mono fun i (hi : Set.Nonempty _) => hi.left

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : {i | (f i ∩ t).Nonempty}.Finite
⊢ ∃ t ∈ 𝓝 x, {i | ((f ∘ g) i ∩ t).Nonempty}.Finite

Tactic:
refine ⟨t, htx, htf.preimage <| ?_⟩

Result:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | (f (g i)).Nonempty}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : {i | (f i ∩ t).Nonempty}.Finite
⊢ InjOn g (g ⁻¹' {i | (f i ∩ t).Nonempty})
-- Mathlib/Order/Disjoint.lean
theorem isCompl_iff [BoundedOrder α] [BoundedOrder β] {x y : α × β} :
    IsCompl x y ↔ IsCompl x.1 y.1 ∧ IsCompl x.2 y.2

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd

Tactic:
simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem map_apply_div_ne_zero {R F : Type*} [CommRing R] [IsDomain R]
    [FunLike F K[X] R[X]] [MonoidHomClass F K[X] R[X]]
    (φ : F) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) (p q : K[X]) (hq : q ≠ 0) :
    map φ hφ (algebraMap _ _ p / algebraMap _ _ q) =
      algebraMap _ _ (φ p) / algebraMap _ _ (φ q)

Proof state:
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
hq' : φ q ≠ 0
⊢ (map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) =
    (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)

Tactic:
simp only [← mk_eq_div, mk_eq_localization_mk _ hq, map_apply_ofFractionRing_mk,
  mk_eq_localization_mk _ hq']

Result:
no goals

Proof state:
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ (map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) =
    (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)

Tactic:
have hq' : φ q ≠ 0 := nonZeroDivisors.ne_zero (hφ (mem_nonZeroDivisors_iff_ne_zero.mpr hq))

Result:
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
hq' : φ q ≠ 0
⊢ (map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) =
    (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem isPrincipal_inv (I : FractionalIdeal R₁⁰ K) [Submodule.IsPrincipal (I : Submodule R₁ K)]
    (h : I ≠ 0) : Submodule.IsPrincipal I⁻¹.1

Proof state:
case h
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ I⁻¹ = spanSingleton R₁⁰ (generator ↑I)⁻¹

Tactic:
have hI : I * spanSingleton _ (generator (I : Submodule R₁ K))⁻¹ = 1 :=
  mul_generator_self_inv _ I h

Result:
case h
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
hI : I * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1
⊢ I⁻¹ = spanSingleton R₁⁰ (generator ↑I)⁻¹

Proof state:
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ (↑I⁻¹).IsPrincipal

Tactic:
rw [val_eq_coe, isPrincipal_iff]

Result:
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ ∃ x, I⁻¹ = spanSingleton R₁⁰ x

Proof state:
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ ∃ x, I⁻¹ = spanSingleton R₁⁰ x

Tactic:
use (generator (I : Submodule R₁ K))⁻¹

Result:
case h
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
⊢ I⁻¹ = spanSingleton R₁⁰ (generator ↑I)⁻¹

Proof state:
case h
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
hI : I * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1
⊢ I⁻¹ = spanSingleton R₁⁰ (generator ↑I)⁻¹

Tactic:
exact (right_inverse_eq _ I (spanSingleton _ (generator (I : Submodule R₁ K))⁻¹) hI).symm

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem yn_add (m n) : yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ ↑(yn a1 (m + n)) = ↑(xn a1 m) * ↑(yn a1 n) + ↑(yn a1 m) * ↑(xn a1 n)

Tactic:
rw [h]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re =
    ↑(xn a1 m) * ↑(yn a1 n) + ↑(yn a1 m) * ↑(xn a1 n)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

Tactic:
injection pellZd_add a1 m n with _ h

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re =
    ↑(xn a1 m) * ↑(yn a1 n) + ↑(yn a1 m) * ↑(xn a1 n)

Tactic:
simp [pellZd]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

Tactic:
zify

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ ↑(yn a1 (m + n)) = ↑(xn a1 m) * ↑(yn a1 n) + ↑(yn a1 m) * ↑(xn a1 n)
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_eq_zero_iff (x y : E) : o.kahler x y = 0 ↔ x = 0 ∨ y = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ x = 0 ∨ y = 0 → (o.kahler x) y = 0

Tactic:
rintro (rfl | rfl) <;> simp

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler x) y = 0 ↔ x = 0 ∨ y = 0

Tactic:
refine ⟨o.eq_zero_or_eq_zero_of_kahler_eq_zero, ?_⟩

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ x = 0 ∨ y = 0 → (o.kahler x) y = 0
-- Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
theorem min_mul_distrib' (a b c : α) : min (a * b) c = min (min a c * min b c) c

Proof state:
α : Type u
inst✝¹ : LinearOrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
a b c : α
⊢ a * b ⊓ c = (a ⊓ c) * (b ⊓ c) ⊓ c

Tactic:
simpa [min_comm _ c] using min_mul_distrib c a b

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem mem_stepSet_iff : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t a)

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

Tactic:
simp_rw [stepSet, mem_iUnion₂, exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l
  | [], _ => rfl
  | b :: l, h => by
    rw [mem_cons, not_or] at h
    simp only [erase_cons, if_neg, erase_of_not_mem h.2, beq_iff_eq, Ne.symm h.1, not_false_eq_true]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : ¬a ∈ b :: l
⊢ (b :: l).erase a = b :: l

Tactic:
rw [mem_cons, not_or] at h

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : ¬a = b ∧ ¬a ∈ l
⊢ (b :: l).erase a = b :: l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
h : ¬a = b ∧ ¬a ∈ l
⊢ (b :: l).erase a = b :: l

Tactic:
simp only [erase_cons, if_neg, erase_of_not_mem h.2, beq_iff_eq, Ne.symm h.1, not_false_eq_true]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem MeasurePreserving.integrable_comp {ν : Measure δ} {g : δ → β} {f : α → δ}
    (hf : MeasurePreserving f μ ν) (hg : AEStronglyMeasurable g ν) :
    Integrable (g ∘ f) μ ↔ Integrable g ν

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable g ν
⊢ Integrable (g ∘ f) μ ↔ Integrable g ν

Tactic:
rw [← hf.map_eq] at hg ⊢

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable g (Measure.map f μ)
⊢ Integrable (g ∘ f) μ ↔ Integrable g (Measure.map f μ)

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
ν : Measure δ
g : δ → β
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable g (Measure.map f μ)
⊢ Integrable (g ∘ f) μ ↔ Integrable g (Measure.map f μ)

Tactic:
exact (integrable_map_measure hg hf.measurable.aemeasurable).symm

Result:
no goals