harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(-π / 2)) : ∠ p₁ p₂ p₃ = π / 2

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₃ = ↑(-π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]

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₃ = ↑(-π / 2)
⊢ inner (p₁ -ᵥ p₂) (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₃ = ↑(-π / 2)
⊢ inner (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 0

Tactic:
exact o.inner_eq_zero_of_oangle_eq_neg_pi_div_two h

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
lemma span_singleton_toAddSubgroup_eq_zmultiples (a : ℤ) :
    (span ℤ {a}).toAddSubgroup = AddSubgroup.zmultiples a

Proof state:
a : ℤ
⊢ (span ℤ {a}).toAddSubgroup = AddSubgroup.zmultiples a

Tactic:
ext i

Result:
case h
a i : ℤ
⊢ i ∈ (span ℤ {a}).toAddSubgroup ↔ i ∈ AddSubgroup.zmultiples a

Proof state:
case h
a i : ℤ
⊢ i ∈ (span ℤ {a}).toAddSubgroup ↔ i ∈ AddSubgroup.zmultiples a

Tactic:
simp [Ideal.mem_span_singleton', AddSubgroup.mem_zmultiples_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Extensive.lean
theorem finitaryExtensive_of_preserves_and_reflects_isomorphism (F : C ⥤ D) [FinitaryExtensive D]
    [HasFiniteCoproducts C] [HasPullbacks C] [PreservesLimitsOfShape WalkingCospan F]
    [PreservesColimitsOfShape (Discrete WalkingPair) F] [F.ReflectsIsomorphisms] :
    FinitaryExtensive C

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : F.ReflectsIsomorphisms
⊢ FinitaryExtensive C

Tactic:
haveI : ReflectsLimitsOfShape WalkingCospan F := reflectsLimitsOfShape_of_reflectsIsomorphisms

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ FinitaryExtensive C

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ FinitaryExtensive C

Tactic:
haveI : ReflectsColimitsOfShape (Discrete WalkingPair) F :=
  reflectsColimitsOfShape_of_reflectsIsomorphisms

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : F.ReflectsIsomorphisms
this✝ : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape (Discrete WalkingPair) F
⊢ FinitaryExtensive C

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : F.ReflectsIsomorphisms
this✝ : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape (Discrete WalkingPair) F
⊢ FinitaryExtensive C

Tactic:
exact finitaryExtensive_of_preserves_and_reflects F

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem map_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.map f = l.unattach.map g

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : map f l = map g (map (fun x => x.val) l)
⊢ map f (a :: l) = map g (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ map f l = map g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ map f l = map g l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ map f l = map g (map (fun x => x.val) l)

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ map f [] = map g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_inj : Set.InjOn factorization { x : ℕ | x ≠ 0 } := fun a ha b hb h =>
  eq_of_factorization_eq ha hb fun p => by simp [h]

Proof state:
a : ℕ
ha : a ∈ {x | x ≠ 0}
b : ℕ
hb : b ∈ {x | x ≠ 0}
h : a.factorization = b.factorization
p : ℕ
⊢ a.factorization p = b.factorization p

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem accepts_comap (f : α' → α) : (M.comap f).accepts = List.map f ⁻¹' M.accepts

Proof state:
case h
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ M.eval (List.map f x) ∈ M.accept

Tactic:
simp [mem_accepts]

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
⊢ (comap f M).accepts = List.map f ⁻¹' M.accepts

Tactic:
ext x

Result:
case h
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts

Proof state:
case h
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts

Tactic:
conv =>
  rhs
  rw [Set.mem_preimage, mem_accepts]

Result:
case h
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ M.eval (List.map f x) ∈ M.accept
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem fromSpec_preimage_basicOpen :
    hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f

Tactic:
rw [fromSpec_preimage_basicOpen', ← basicOpen_eq_of_affine]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
theorem exists_index_pow_le (hna : IsNonarchimedean p) (x y : R) (n : ℕ) :
    ∃ (m : ℕ), m < n + 1 ∧ p ((x + y) ^ (n : ℕ)) ^ (1 / (n : ℝ)) ≤
      (p (x ^ m) * p (y ^ (n - m : ℕ))) ^ (1 / (n : ℝ))

Proof state:
R : Type u_1
inst✝ : CommRing R
p : RingSeminorm R
hna : IsNonarchimedean ⇑p
x y : R
n : ℕ
⊢ ∃ m < n + 1, p ((x + y) ^ n) ^ (1 / ↑n) ≤ (p (x ^ m) * p (y ^ (n - m))) ^ (1 / ↑n)

Tactic:
obtain ⟨m, hm_lt, hm⟩ := IsNonarchimedean.add_pow_le hna n x y

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p : RingSeminorm R
hna : IsNonarchimedean ⇑p
x y : R
n m : ℕ
hm_lt : m < n + 1
hm : p ((x + y) ^ n) ≤ p (x ^ m) * p (y ^ (n - m))
⊢ ∃ m < n + 1, p ((x + y) ^ n) ^ (1 / ↑n) ≤ (p (x ^ m) * p (y ^ (n - m))) ^ (1 / ↑n)

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p : RingSeminorm R
hna : IsNonarchimedean ⇑p
x y : R
n m : ℕ
hm_lt : m < n + 1
hm : p ((x + y) ^ n) ≤ p (x ^ m) * p (y ^ (n - m))
⊢ ∃ m < n + 1, p ((x + y) ^ n) ^ (1 / ↑n) ≤ (p (x ^ m) * p (y ^ (n - m))) ^ (1 / ↑n)

Tactic:
exact ⟨m, hm_lt, Real.rpow_le_rpow (apply_nonneg p _) hm (one_div_nonneg.mpr n.cast_nonneg')⟩

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem strictMono_iterate_of_lt_map (hf : StrictMono f) (hx : x < f x) :
    StrictMono fun n => f^[n] x :=
  strictMono_nat_of_lt_succ fun n => by
    rw [iterate_succ_apply]
    exact hf.iterate n hx

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x

Tactic:
rw [iterate_succ_apply]

Result:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)

Tactic:
exact hf.iterate n hx

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem IndepFun.integrable_exp_mul_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ)
    (h_int_X : Integrable (fun ω => exp (t * X ω)) μ)
    (h_int_Y : Integrable (fun ω => exp (t * Y ω)) μ) :
    Integrable (fun ω => exp (t * (X + Y) ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ Integrable (fun ω => rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
exact (h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ Integrable (fun ω => rexp (t * (X + Y) ω)) μ

Tactic:
simp_rw [Pi.add_apply, mul_add, exp_add]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : IndepFun X Y μ
h_int_X : Integrable (fun ω => rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ Integrable (fun ω => rexp (t * X ω) * rexp (t * Y ω)) μ
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma div_mul_div_cancel₀ (hb : b ≠ 0) : a / b * (b / c) = a / c

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a / b * (b / c) = a / c

Tactic:
rw [← mul_div_assoc, div_mul_cancel₀ _ hb]

Result:
no goals
-- Mathlib/RingTheory/Noetherian/Filter.lean
theorem eventuallyConst_of_isNoetherian [IsNoetherian R M] (f : ℕ →o Submodule R M) :
    atTop.EventuallyConst f

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ EventuallyConst (⇑f) atTop

Tactic:
simp_rw [eventuallyConst_atTop, eq_comm]

Result:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j

Tactic:
exact (monotone_stabilizes_iff_noetherian.mpr inferInstance) f

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem card_congr {α β} [Fintype α] [Fintype β] (f : α ≃ β) : card α = card β

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β

Tactic:
congr!

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card α = card β

Tactic:
rw [← ofEquiv_card f]

Result:
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_push (L : Array (Array α)) (l : Array α) :
    flatten (L.push l) = flatten L ++ l

Proof state:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
this : [l.toArray] = List.map List.toArray [l]
⊢ (List.map List.toArray xss✝ ++ [{ toList := l }]).toArray.flatten = (xss✝.flatten ++ l).toArray

Tactic:
rw [this, ← List.map_append, flatten_toArray_map]

Result:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
this : [l.toArray] = List.map List.toArray [l]
⊢ (xss✝ ++ [l]).flatten.toArray = (xss✝.flatten ++ l).toArray

Proof state:
α : Type u_1
L : Array (Array α)
l : Array α
⊢ (L.push l).flatten = L.flatten ++ l

Tactic:
induction L using array₂_induction

Result:
case of
α : Type u_1
l : Array α
xss✝ : List (List α)
⊢ ((List.map List.toArray xss✝).toArray.push l).flatten = (List.map List.toArray xss✝).toArray.flatten ++ l

Proof state:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
⊢ ((List.map List.toArray xss✝).toArray.push { toList := l }).flatten =
    (List.map List.toArray xss✝).toArray.flatten ++ { toList := l }

Tactic:
have this : [l.toArray] = [l].map List.toArray := by simp

Result:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
this : [l.toArray] = List.map List.toArray [l]
⊢ ((List.map List.toArray xss✝).toArray.push { toList := l }).flatten =
    (List.map List.toArray xss✝).toArray.flatten ++ { toList := l }

Proof state:
α : Type u_1
xss✝ : List (List α)
l : List α
⊢ [l.toArray] = List.map List.toArray [l]

Tactic:
simp

Result:
no goals

Proof state:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
this : [l.toArray] = List.map List.toArray [l]
⊢ (xss✝ ++ [l]).flatten.toArray = (xss✝.flatten ++ l).toArray

Tactic:
simp

Result:
no goals

Proof state:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
this : [l.toArray] = List.map List.toArray [l]
⊢ ((List.map List.toArray xss✝).toArray.push { toList := l }).flatten =
    (List.map List.toArray xss✝).toArray.flatten ++ { toList := l }

Tactic:
simp only [List.push_toArray, flatten_toArray_map, List.append_toArray]

Result:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
this : [l.toArray] = List.map List.toArray [l]
⊢ (List.map List.toArray xss✝ ++ [{ toList := l }]).toArray.flatten = (xss✝.flatten ++ l).toArray

Proof state:
case of
α : Type u_1
l : Array α
xss✝ : List (List α)
⊢ ((List.map List.toArray xss✝).toArray.push l).flatten = (List.map List.toArray xss✝).toArray.flatten ++ l

Tactic:
rcases l with ⟨l⟩

Result:
case of.mk
α : Type u_1
xss✝ : List (List α)
l : List α
⊢ ((List.map List.toArray xss✝).toArray.push { toList := l }).flatten =
    (List.map List.toArray xss✝).toArray.flatten ++ { toList := l }
-- Mathlib/Analysis/Seminorm.lean
theorem zero_or_exists_apply_eq_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) :
    s.sup p x = 0 ∨ ∃ i ∈ s, s.sup p x = p i x

Proof state:
case inr.h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
exact exists_apply_eq_finset_sup p hs x

Result:
no goals

Proof state:
case inl
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = 0 ∨ ∃ i ∈ ∅, (∅.sup p) x = (p i) x

Tactic:
left

Result:
case inl.h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = 0

Proof state:
case inl.h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = 0

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
⊢ (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
rcases Finset.eq_empty_or_nonempty s with (rfl|hs)

Result:
case inl
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = 0 ∨ ∃ i ∈ ∅, (∅.sup p) x = (p i) x

case inr
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x

Proof state:
case inr
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
right

Result:
case inr.h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ ∃ i ∈ s, (s.sup p) x = (p i) x
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem vanishingIdeal_univ : vanishingIdeal (∅ : Set (ProjectiveSpectrum 𝒜)) = ⊤

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ vanishingIdeal ∅ = ⊤

Tactic:
simpa using (gc_ideal _).u_top

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
protected lemma _root_.Set.Sized.compls (h𝒜 : (𝒜 : Set (Finset α)).Sized n) :
    (𝒜ᶜˢ : Set (Finset α)).Sized (Fintype.card α - n) :=
  Finset.forall_mem_compls.2 <| fun s hs ↦ by rw [Finset.card_compl, h𝒜 hs]

Proof state:
α : Type u_4
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
h𝒜 : Set.Sized n ↑𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ #sᶜ = Fintype.card α - n

Tactic:
rw [Finset.card_compl, h𝒜 hs]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem toDirectSum_comp_ofDirectSum :
    toDirectSum.comp ofDirectSum = AlgHom.id R (⨁ n, ⨂[R]^n M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toDirectSum.comp ofDirectSum = AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)

Tactic:
ext

Result:
case h.H.H.w
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝¹ : ℕ
x✝ : Fin i✝¹ → M
i✝ : ℕ
⊢ ((((toDirectSum.comp ofDirectSum).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i => ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝ =
    ((((AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i => ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝

Proof state:
case h.H.H.w
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝¹ : ℕ
x✝ : Fin i✝¹ → M
i✝ : ℕ
⊢ ((((toDirectSum.comp ofDirectSum).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i => ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝ =
    ((((AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i => ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝

Tactic:
simp [DirectSum.lof_eq_of, -tprod_apply, toDirectSum_tensorPower_tprod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
    (l : List α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
      l.foldlM (fun b a => g a b <$> f a b) init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → β → m γ
g : α → β → γ → β
init : β
⊢ (forIn l init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    List.foldlM (fun b a => g a b <$> f a b) init l

Tactic:
simp only [forIn_eq_foldlM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → β → m γ
g : α → β → γ → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => (fun c => ForInStep.yield (g a b c)) <$> f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    List.foldlM (fun b a => g a b <$> f a b) init l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → β → m γ
g : α → β → γ → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => (fun c => ForInStep.yield (g a b c)) <$> f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    List.foldlM (fun b a => g a b <$> f a b) init l

Tactic:
induction l generalizing init <;> simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem Measurable.mul_iff_right {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G]
    [MeasurableMul₂ G] [MeasurableInv G] {f g : α → G} (hf : Measurable f) :
    Measurable (f * g) ↔ Measurable g :=
  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
    fun h ↦ hf.mul h⟩

Proof state:
α : Type u_1
G : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSpace α
inst✝² : CommGroup G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
f g : α → G
hf : Measurable f
h : Measurable (f * g)
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_eq_empty_iff : range' s n step = #[] ↔ n = 0

Proof state:
s n step : Nat
⊢ range' s n step = #[] ↔ n = 0

Tactic:
rw [← size_eq_zero, size_range']

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma measurable_densityProcess_aux (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ)
    {s : Set β} (hs : MeasurableSet s) :
    Measurable (fun (p : α × γ) ↦
      κ p.1 (countablePartitionSet n p.2 ×ˢ s) / ν p.1 (countablePartitionSet n p.2))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun p => (κ p.1) (countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (countablePartitionSet n p.2)

Tactic:
refine Measurable.mono (measurable_densityProcess_countableFiltration_aux κ ν n hs) ?_ le_rfl

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ mα.prod (↑(countableFiltration γ) n) ≤ Prod.instMeasurableSpace

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ mα.prod (↑(countableFiltration γ) n) ≤ Prod.instMeasurableSpace

Tactic:
exact sup_le_sup le_rfl (comap_mono ((countableFiltration γ).le _))

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem ne_one (h : Irrational x) : x ≠ 1

Proof state:
x : ℝ
h : Irrational x
⊢ x ≠ 1

Tactic:
simpa only [Nat.cast_one] using h.ne_nat 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_inj : ∀ {x y : Bool}, (!x) = (!y) → x = y

Proof state:
⊢ ∀ {x y : Bool}, (!x) = !y → x = y

Tactic:
decide

Result:
no goals