harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iInf' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, AEMeasurable (f n) μ)
    (h_anti : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a)) (h_fin : ∫⁻ a, f 0 a ∂μ ≠ ∞) :
    ∫⁻ a, ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ a, f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
let p : α → (ℕ → ℝ≥0∞) → Prop := fun _ f' => Antitone f'

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_anti

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

Tactic:
by_cases hx : x ∈ aeSeqSet h_meas p

Result:
case pos
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∈ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x

case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i => f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x
-- Mathlib/Data/List/SplitOn.lean
theorem splitOnP_eq_single (h : ∀ x ∈ xs, ¬p x) : xs.splitOnP p = [xs]

Proof state:
case cons
α : Type u_1
p : α → Bool
xs : List α
hd : α
tl : List α
ih : (∀ (x : α), x ∈ tl → ¬p x = true) → splitOnP p tl = [tl]
h : ∀ (x : α), x ∈ hd :: tl → ¬p x = true
⊢ splitOnP p (hd :: tl) = [hd :: tl]

Tactic:
simp only [splitOnP_cons, h hd (mem_cons_self hd tl), if_false, Bool.false_eq_true,
  modifyHead_cons, ih <| forall_mem_of_forall_mem_cons h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ xs → ¬p x = true
⊢ splitOnP p xs = [xs]

Tactic:
induction xs with
| nil => simp only [splitOnP_nil]
| cons hd tl ih =>
  simp only [splitOnP_cons, h hd (mem_cons_self hd tl), if_false, Bool.false_eq_true,
    modifyHead_cons, ih <| forall_mem_of_forall_mem_cons h]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ [] → ¬p x = true
⊢ splitOnP p [] = [[]]

Tactic:
simp only [splitOnP_nil]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_eq_false {p : α → Bool} {xs : Vector α n} :
    xs.any p = false ↔ ∀ (i : Nat) (_ : i < n), ¬p xs[i]

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ (¬∃ i x, p xs[i] = true) ↔ ∀ (i : Nat) (x : i < n), ¬p xs[i] = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.any p = false ↔ ∀ (i : Nat) (x : i < n), ¬p xs[i] = true

Tactic:
rw [Bool.eq_false_iff, Ne, any_eq_true]

Result:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ (¬∃ i x, p xs[i] = true) ↔ ∀ (i : Nat) (x : i < n), ¬p xs[i] = true
-- Mathlib/CategoryTheory/EqToHom.lean
theorem congrArg_cast_hom_right {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
    cast (congrArg (fun W : C => X ⟶ W) q.symm) p = p ≫ eqToHom q.symm

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ cast ⋯ p = p ≫ eqToHom ⋯

Tactic:
cases q

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ cast ⋯ p = p ≫ eqToHom ⋯

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ cast ⋯ p = p ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem setLIntegral_deterministic' {f : β → ℝ≥0∞} {g : α → β} {a : α} (hg : Measurable g)
    (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a ∈ s)] :
    ∫⁻ x in s, f x ∂deterministic g hg a = if g a ∈ s then f (g a) else 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setLIntegral_dirac' hf hs]

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_rightMoves (o : Ordinal) : o.toPGame.RightMoves = PEmpty

Proof state:
o : Ordinal.{u_1}
⊢ o.toPGame.RightMoves = PEmpty.{u_1 + 1}

Tactic:
rw [toPGame, RightMoves]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem eq_tsub_iff_add_eq_of_le (hc : AddLECancellable c) (h : c ≤ b) :
    a = b - c ↔ a + c = b :=
  ⟨by
    rintro rfl
    exact tsub_add_cancel_of_le h, hc.eq_tsub_of_add_eq⟩

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a = b - c → a + c = b

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ b - c + c = b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ b - c + c = b

Tactic:
exact tsub_add_cancel_of_le h

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem prod_range_mul {f : ℕ → M} {k : ℕ} (h : HasProd (fun n ↦ f (n + k)) m) :
    HasProd f ((∏ i ∈ range k, f i) * m)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℕ → M
k : ℕ
h : HasProd (fun n => f (n + k)) m
⊢ HasProd f ((∏ i ∈ range k, f i) * m)

Tactic:
refine ((range k).hasProd f).mul_compl ?_

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℕ → M
k : ℕ
h : HasProd (fun n => f (n + k)) m
⊢ HasProd (f ∘ Subtype.val) m

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℕ → M
k : ℕ
h : HasProd (fun n => f (n + k)) m
⊢ HasProd (f ∘ Subtype.val) m

Tactic:
rwa [← (notMemRangeEquiv k).symm.hasProd_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Coherence.lean
theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
    normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)

Proof state:
case of
B : Type u
inst✝ : Quiver B
b c a✝ b✝ : B
f✝ : a✝ ⟶ b✝
a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (Hom.of f✝)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.of f✝))

Tactic:
rfl

Result:
no goals

Proof state:
case id
B : Type u
inst✝ : Quiver B
b c a✝ a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (Hom.id a✝)) = (normalizeAux nil f).comp (normalizeAux nil (Hom.id a✝))

Tactic:
rfl

Result:
no goals

Proof state:
case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ normalizeAux nil (f.comp (g.comp g✝)) = (normalizeAux nil f).comp (normalizeAux nil (g.comp g✝))

Tactic:
erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]

Result:
no goals

Proof state:
B : Type u
inst✝ : Quiver B
a b c : B
f : Hom a b
g : Hom b c
⊢ normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)

Tactic:
induction g generalizing a with
| id => rfl
| of => rfl
| comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]

Result:
no goals
-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem primitive_element_iff_minpoly_natDegree_eq (α : E) :
    F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E

Proof state:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E

Tactic:
rw [← adjoin.finrank (IsIntegral.of_finite F α), ← finrank_top F E]

Result:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ finrank F ↥F⟮α⟯ = finrank F ↥⊤

Proof state:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
h : F⟮α⟯ = ⊤
⊢ finrank F ↥F⟮α⟯ = finrank F ↥⊤

Tactic:
exact congr_arg (fun K : IntermediateField F E => finrank F K) h

Result:
no goals

Proof state:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ finrank F ↥F⟮α⟯ = finrank F ↥⊤

Tactic:
refine ⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩

Result:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
h : F⟮α⟯ = ⊤
⊢ finrank F ↥F⟮α⟯ = finrank F ↥⊤
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_singleton (a : α) (s : α → β) : ⨆ x ∈ ({a} : Finset α), s x = s a

Proof state:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
a : α
s : α → β
⊢ ⨆ x ∈ {a}, s x = s a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem mem_dite_univ_right (p : Prop) [Decidable p] (t : p → Set α) (x : α) :
    (x ∈ if h : p then t h else univ) ↔ ∀ h : p, x ∈ t h

Proof state:
α : Type u
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (x ∈ if h : p then t h else univ) ↔ ∀ (h : p), x ∈ t h

Tactic:
simp [mem_dite]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem seminormAux_smul_le (k n : ℕ) (c : 𝕜) (f : 𝓢(E, F)) :
    (c • f).seminormAux k n ≤ ‖c‖ * f.seminormAux k n

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ‖c‖ * SchwartzMap.seminormAux k n f

Tactic:
rw [mul_assoc]

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ ‖c‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖) ≤ ‖c‖ * SchwartzMap.seminormAux k n f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
⊢ SchwartzMap.seminormAux k n (c • f) ≤ ‖c‖ * SchwartzMap.seminormAux k n f

Tactic:
refine
  (c • f).seminormAux_le_bound k n (mul_nonneg (norm_nonneg _) (seminormAux_nonneg _ _ _))
    fun x => (decay_smul_aux k n f c x).le.trans ?_

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ‖c‖ * SchwartzMap.seminormAux k n f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ ‖c‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖) ≤ ‖c‖ * SchwartzMap.seminormAux k n f

Tactic:
exact mul_le_mul_of_nonneg_left (f.le_seminormAux k n x) (norm_nonneg _)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
lemma absolutelyContinuous_map (hf : MeasurableEmbedding f) (hμν : μ ≪ ν) :
    μ.map f ≪ ν.map f

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : ν (f ⁻¹' t) = 0
⊢ μ (f ⁻¹' t) = 0

Tactic:
exact hμν ht

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
⊢ map f μ ≪ map f ν

Tactic:
intro t ht

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : (map f ν) t = 0
⊢ (map f μ) t = 0

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : (map f ν) t = 0
⊢ (map f μ) t = 0

Tactic:
rw [hf.map_apply] at ht ⊢

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : ν (f ⁻¹' t) = 0
⊢ μ (f ⁻¹' t) = 0
-- Mathlib/Algebra/Algebra/Spectrum.lean
@[simp]
lemma inv₀_mem_iff {r : R} {a : Aˣ} :
    r⁻¹ ∈ spectrum R (a : A) ↔ r ∈ spectrum R (↑a⁻¹ : A)

Proof state:
case inl
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
⊢ 0⁻¹ ∈ spectrum R ↑a ↔ 0 ∈ spectrum R ↑a⁻¹

Tactic:
simp [zero_mem_iff]

Result:
no goals

Proof state:
case inr
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : Aˣ
hr : r ≠ 0
⊢ r⁻¹ ∈ spectrum R ↑a ↔ r ∈ spectrum R ↑a⁻¹

Tactic:
lift r to Rˣ using hr.isUnit

Result:
case inr.intro
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
r : Rˣ
hr : ↑r ≠ 0
⊢ (↑r)⁻¹ ∈ spectrum R ↑a ↔ ↑r ∈ spectrum R ↑a⁻¹

Proof state:
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : Aˣ
⊢ r⁻¹ ∈ spectrum R ↑a ↔ r ∈ spectrum R ↑a⁻¹

Tactic:
obtain (rfl | hr) := eq_or_ne r 0

Result:
case inl
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
⊢ 0⁻¹ ∈ spectrum R ↑a ↔ 0 ∈ spectrum R ↑a⁻¹

case inr
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : Aˣ
hr : r ≠ 0
⊢ r⁻¹ ∈ spectrum R ↑a ↔ r ∈ spectrum R ↑a⁻¹

Proof state:
case inr.intro
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : Aˣ
r : Rˣ
hr : ↑r ≠ 0
⊢ (↑r)⁻¹ ∈ spectrum R ↑a ↔ ↑r ∈ spectrum R ↑a⁻¹

Tactic:
simp [inv_mem_iff]

Result:
no goals
-- Mathlib/Algebra/CharP/Algebra.lean
theorem charP_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
    {f : R →+* A} (h : Function.Injective f) (p : ℕ) [CharP R p] : CharP A p where
  cast_eq_zero_iff' x

Proof state:
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x

Tactic:
rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem ModuleCat.eq_range_of_pseudoequal {R : Type*} [CommRing R] {G : ModuleCat R} {x y : Over G}
    (h : PseudoEqual G x y) : LinearMap.range x.hom.hom = LinearMap.range y.hom.hom

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
⊢ LinearMap.range (ModuleCat.Hom.hom x.hom) = LinearMap.range (ModuleCat.Hom.hom y.hom)

Tactic:
refine Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Result:
case intro.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
ha : a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)

case intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
ha : a ∈ LinearMap.range (ModuleCat.Hom.hom y.hom)
⊢ a ∈ LinearMap.range (ModuleCat.Hom.hom x.hom)
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma pow_add_pow_le' (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ n + b ^ n ≤ 2 * (a + b) ^ n

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ 2 * (a + b) ^ n

Tactic:
rw [two_mul]

Result:
R : Type u_3
inst✝ : OrderedSemiring R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n

Proof state:
R : Type u_3
inst✝ : OrderedSemiring R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n

Tactic:
exact add_le_add (pow_le_pow_left₀ ha (le_add_of_nonneg_right hb) _)
  (pow_le_pow_left₀ hb (le_add_of_nonneg_left ha) _)

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_eq_map_of_constant_state (f : α → σ → σ × β) (s : σ) (h : ∀ a, (f a s).fst = s) :
    mapAccumr f xs s = (s, (map (fun x => (f x s).snd) xs))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
⊢ mapAccumr f xs s = (s, map (fun x => (f x s).2) xs)

Tactic:
induction xs using revInductionOn <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem mem_of (h : c ∈ f) (w : Clause.Mem v c) : Mem v f

Proof state:
α✝ : Type u_1
f : CNF α✝
c : Clause α✝
v : α✝
h : c ∈ f
w : Clause.Mem v c
⊢ c ∈ f ∧ Clause.Mem v c

Tactic:
constructor <;> assumption

Result:
no goals

Proof state:
α✝ : Type u_1
f : CNF α✝
c : Clause α✝
v : α✝
h : c ∈ f
w : Clause.Mem v c
⊢ Mem v f

Tactic:
apply Exists.intro c

Result:
α✝ : Type u_1
f : CNF α✝
c : Clause α✝
v : α✝
h : c ∈ f
w : Clause.Mem v c
⊢ c ∈ f ∧ Clause.Mem v c
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.preimage_interior_subset_interior_preimage {t : Set β}
    (hf : ContinuousOn f s) (hs : IsOpen s) : s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t) :=
  calc
    s ∩ f ⁻¹' interior t ⊆ interior (s ∩ f ⁻¹' t) :=
      interior_maximal (inter_subset_inter (Subset.refl _) (preimage_mono interior_subset))
        (hf.isOpen_inter_preimage hs isOpen_interior)
    _ = s ∩ interior (f ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsOpen s
⊢ interior (s ∩ f ⁻¹' t) = s ∩ interior (f ⁻¹' t)

Tactic:
rw [interior_inter, hs.interior_eq]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Colimits.lean
lemma Quot.desc_toCocone_desc [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A)
    (hc : IsColimit c) : (hc.desc (toCocone F f)).hom.comp (Quot.desc F c) = f

Proof state:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((toCocone F f).ι.app j)) x = f ((ι F j) x)

Tactic:
simp

Result:
no goals

Proof state:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (c.ι.app j ≫ hc.desc (toCocone F f))) x = f ((ι F j) x)

Tactic:
rw [hc.fac]

Result:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((toCocone F f).ι.app j)) x = f ((ι F j) x)

Proof state:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
⊢ (Hom.hom (hc.desc (toCocone F f))).comp (desc F c) = f

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)

Result:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ ((Hom.hom (hc.desc (toCocone F f))).comp (desc F c)) ((ι F j) x) = f ((ι F j) x)

Proof state:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ ((Hom.hom (hc.desc (toCocone F f))).comp (desc F c)) ((ι F j) x) = f ((ι F j) x)

Tactic:
rw [AddMonoidHom.comp_apply, ι_desc]

Result:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (Hom.hom (hc.desc (toCocone F f))) ((ConcreteCategory.hom (c.ι.app j)) x) = f ((ι F j) x)

Proof state:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (Hom.hom (hc.desc (toCocone F f))) ((ConcreteCategory.hom (c.ι.app j)) x) = f ((ι F j) x)

Tactic:
change (c.ι.app j ≫ hc.desc (toCocone F f)) _ = _

Result:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (c.ι.app j ≫ hc.desc (toCocone F f))) x = f ((ι F j) x)