harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/OfFn.lean
lemma find?_ofFn_eq_some {n} {f : Fin n → α} {p : α → Bool} {b : α} :
    (ofFn f).find? p = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬(p (f j) = true)

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ j < i, ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ (!p (ofFn f)[j]) = true

Tactic:
simpa using h ⟨j, by omega⟩ (by simpa using hj)

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, ∃ (h : i < (ofFn f).length), (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : (ofFn f)[i] = b
h : ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
j : Fin n
hj : j < ⟨i, ⋯⟩
⊢ ¬p (f j) = true

Tactic:
simpa using h j hj

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, ∃ (h : i < (ofFn f).length), (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
hpb : p b = true
i : ℕ
hi : i < (ofFn f).length
hfb : (ofFn f)[i] = b
h : ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true
⊢ f ⟨i, ⋯⟩ = b

Tactic:
simpa using hfb

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ j < i, ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ ⟨j, ⋯⟩ < i

Tactic:
simpa using hj

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ (p b = true ∧ ∃ i, ∃ (h : i < (ofFn f).length), (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true) ↔
    p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true

Tactic:
exact ⟨fun ⟨hpb, i, hi, hfb, h⟩ ↦
    ⟨hpb, ⟨⟨i, (length_ofFn f) ▸ hi⟩, by simpa using hfb, fun j hj ↦ by simpa using h j hj⟩⟩,
  fun ⟨hpb, i, hfb, h⟩ ↦
    ⟨hpb, ⟨i, (length_ofFn f).symm ▸ i.isLt, by simpa using hfb,
      fun j hj ↦ by simpa using h ⟨j, by omega⟩ (by simpa using hj)⟩⟩⟩

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ find? p (ofFn f) = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true

Tactic:
rw [find?_eq_some_iff_getElem]

Result:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
⊢ (p b = true ∧ ∃ i, ∃ (h : i < (ofFn f).length), (ofFn f)[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p (ofFn f)[j]) = true) ↔
    p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ j < i, ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ j < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ j < i, ¬p (f j) = true
⊢ (ofFn f)[↑i] = b

Tactic:
simpa using hfb

Result:
no goals
-- Mathlib/Analysis/Complex/Schwarz.lean
theorem dist_le_dist_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball c R))
    (h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (hz : z ∈ ball c R) :
    dist (f z) c ≤ dist z c

Proof state:
f : ℂ → ℂ
c z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) c ≤ R / R * dist z c
⊢ R ≠ 0

Tactic:
exact (nonempty_ball.1 ⟨z, hz⟩).ne'

Result:
no goals

Proof state:
f : ℂ → ℂ
c z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) (f c) ≤ R / R * dist z c
⊢ dist (f z) c ≤ dist z c

Tactic:
rwa [hc, div_self, one_mul] at this

Result:
f : ℂ → ℂ
c z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) c ≤ R / R * dist z c
⊢ R ≠ 0

Proof state:
f : ℂ → ℂ
c z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
⊢ MapsTo f (ball c R) (ball (f c) ?m.39745)

Tactic:
rwa [hc]

Result:
no goals

Proof state:
f : ℂ → ℂ
c z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
⊢ dist (f z) c ≤ dist z c

Tactic:
have := dist_le_div_mul_dist_of_mapsTo_ball hd (by rwa [hc]) hz

Result:
f : ℂ → ℂ
c z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) (f c) ≤ R / R * dist z c
⊢ dist (f z) c ≤ dist z c
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.map_of_surjective {N : Type*} [L.Structure N] (h : FG L M) (f : M →[L] N)
    (hs : Function.Surjective f) : FG L N

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ FG L N

Tactic:
rw [fg_def, ← hs]

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.FG

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : Function.Surjective ⇑f
⊢ FG L N

Tactic:
rw [← Hom.range_eq_top] at hs

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ FG L N

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.FG

Tactic:
exact h.range f

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
theorem RingHom.IsIntegralElem.of_mem_closure {x y z : S} (hx : f.IsIntegralElem x)
    (hy : f.IsIntegralElem y) (hz : z ∈ Subring.closure ({x, y} : Set S)) : f.IsIntegralElem z

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
⊢ f.IsIntegralElem z

Tactic:
letI : Algebra R S := f.toAlgebra

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this : Algebra R S := f.toAlgebra
⊢ f.IsIntegralElem z

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this : Algebra R S := f.toAlgebra
⊢ f.IsIntegralElem z

Tactic:
have := (IsIntegral.fg_adjoin_singleton hx).mul (IsIntegral.fg_adjoin_singleton hy)

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule (Algebra.adjoin R {x}) * Subalgebra.toSubmodule (Algebra.adjoin R {y})).FG
⊢ f.IsIntegralElem z

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule (Algebra.adjoin R {x}) * Subalgebra.toSubmodule (Algebra.adjoin R {y})).FG
⊢ f.IsIntegralElem z

Tactic:
rw [← Algebra.adjoin_union_coe_submodule, Set.singleton_union] at this

Result:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule (Algebra.adjoin R {x, y})).FG
⊢ f.IsIntegralElem z

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule (Algebra.adjoin R {x, y})).FG
⊢ f.IsIntegralElem z

Tactic:
exact
  IsIntegral.of_mem_of_fg (Algebra.adjoin R {x, y}) this z
    (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono Set.subset_union_right hz)

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.continuous_convolution_left
    (hcf : HasCompactSupport f) (hf : Continuous f) (hg : LocallyIntegrable g μ) :
    Continuous (f ⋆[L, μ] g)

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace 𝕜 E'
inst✝⁸ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : AddCommGroup G
inst✝⁴ : μ.IsAddLeftInvariant
inst✝³ : μ.IsNegInvariant
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcf : HasCompactSupport f
hf : Continuous f
hg : LocallyIntegrable g μ
⊢ Continuous (f ⋆[L, μ] g)

Tactic:
rw [← convolution_flip]

Result:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace 𝕜 E'
inst✝⁸ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : AddCommGroup G
inst✝⁴ : μ.IsAddLeftInvariant
inst✝³ : μ.IsNegInvariant
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcf : HasCompactSupport f
hf : Continuous f
hg : LocallyIntegrable g μ
⊢ Continuous (g ⋆[L.flip, μ] f)

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace 𝕜 E'
inst✝⁸ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : AddCommGroup G
inst✝⁴ : μ.IsAddLeftInvariant
inst✝³ : μ.IsNegInvariant
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcf : HasCompactSupport f
hf : Continuous f
hg : LocallyIntegrable g μ
⊢ Continuous (g ⋆[L.flip, μ] f)

Tactic:
exact hcf.continuous_convolution_right L.flip hg hf

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_nat_add (n : ℕ) (a : α) : fract (↑n + a) = fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
n : ℕ
a : α
⊢ fract (↑n + a) = fract a

Tactic:
rw [add_comm, fract_add_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : Array ι)
    (h : ∀ a ∈ l₁ ++ l₂, p a) :
    (l₁ ++ l₂).pmap f h =
      (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
        l₂.pmap f fun a ha => h a (mem_append_right l₁ ha)

Proof state:
case mk
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₂ : Array ι
toList✝ : List ι
h : ∀ (a : ι), a ∈ { toList := toList✝ } ++ l₂ → p a
⊢ pmap f ({ toList := toList✝ } ++ l₂) h = pmap f { toList := toList✝ } ⋯ ++ pmap f l₂ ⋯

Tactic:
cases l₂

Result:
case mk.mk
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
toList✝¹ toList✝ : List ι
h : ∀ (a : ι), a ∈ { toList := toList✝¹ } ++ { toList := toList✝ } → p a
⊢ pmap f ({ toList := toList✝¹ } ++ { toList := toList✝ }) h =
    pmap f { toList := toList✝¹ } ⋯ ++ pmap f { toList := toList✝ } ⋯

Proof state:
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : Array ι
h : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
⊢ pmap f (l₁ ++ l₂) h = pmap f l₁ ⋯ ++ pmap f l₂ ⋯

Tactic:
cases l₁

Result:
case mk
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₂ : Array ι
toList✝ : List ι
h : ∀ (a : ι), a ∈ { toList := toList✝ } ++ l₂ → p a
⊢ pmap f ({ toList := toList✝ } ++ l₂) h = pmap f { toList := toList✝ } ⋯ ++ pmap f l₂ ⋯

Proof state:
case mk.mk
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
toList✝¹ toList✝ : List ι
h : ∀ (a : ι), a ∈ { toList := toList✝¹ } ++ { toList := toList✝ } → p a
⊢ pmap f ({ toList := toList✝¹ } ++ { toList := toList✝ }) h =
    pmap f { toList := toList✝¹ } ⋯ ++ pmap f { toList := toList✝ } ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_sub :
    IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : IsTopologicalAddGroup E
s t : Set E
⊢ IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp [sub_eq_add_neg, isVonNBounded_add]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem isClosed_Ioo_iff {a b : α} : IsClosed (Set.Ioo a b) ↔ b ≤ a

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed (Ioo a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioo a b)
hab : a < b
⊢ False

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed (Ioo a b)

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioo a b)
hab : a < b
this : closure (Ioo a b) = Ioo a b
⊢ False

Tactic:
rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioo a b)
hab : a < b
⊢ False

Tactic:
have := h.closure_eq

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed (Ioo a b)
hab : a < b
this : closure (Ioo a b) = Ioo a b
⊢ False
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem subsingleton [Subsingleton B] : minpoly A x = 1

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ degree 1
⊢ minpoly A x = 1

Tactic:
rw [degree_one] at this

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
⊢ minpoly A x = 1

Tactic:
have := minpoly.min A x monic_one (Subsingleton.elim _ _)

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ degree 1
⊢ minpoly A x = 1

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
⊢ minpoly A x = 1

Tactic:
nontriviality A

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
⊢ minpoly A x = 1

Proof state:
case inr
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : 0 < (minpoly A x).degree
⊢ minpoly A x = 1

Tactic:
exact (this.not_lt h).elim

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1

Tactic:
rcases le_or_lt (minpoly A x).degree 0 with h | h

Result:
case inl
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1

case inr
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : 0 < (minpoly A x).degree
⊢ minpoly A x = 1

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : (minpoly A x).degree ≤ 0
⊢ eval₂ (algebraMap A B) x 1 = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case inl
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : (minpoly A x).degree ≤ 0
⊢ minpoly A x = 1

Tactic:
rwa [(monic ⟨1, monic_one, by simp [eq_iff_true_of_subsingleton]⟩ :
       (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem exists_mem_insert {P : α → Prop} {a : α} {s : Set α} :
    (∃ x ∈ insert a s, P x) ↔ (P a ∨ ∃ x ∈ s, P x)

Proof state:
α : Type u
P : α → Prop
a : α
s : Set α
⊢ (∃ x ∈ insert a s, P x) ↔ P a ∨ ∃ x ∈ s, P x

Tactic:
simp [mem_insert_iff, or_and_right, exists_and_left, exists_or]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `(S : Solution)`, we have that `λ ^ 2` does not divide `S.a + η * S.b`. -/
lemma lambda_sq_not_dvd_a_add_eta_mul_b : ¬ λ ^ 2 ∣ (S.a + η * S.b)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ¬λ ^ 2 ∣ S.a + ↑η * S.b

Tactic:
simp_rw [a_add_eta_mul_b, dvd_add_right S.hab, pow_two, mul_dvd_mul_iff_left
  hζ.zeta_sub_one_prime'.ne_zero, S.hb, not_false_eq_true]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem smulRight_one_pow [TopologicalSpace R] [IsTopologicalRing R] (c : R) (n : ℕ) :
    smulRight (1 : R →L[R] R) c ^ n = smulRight (1 : R →L[R] R) (c ^ n)

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
n : ℕ
⊢ smulRight 1 c ^ n = smulRight 1 (c ^ n)

Tactic:
induction n with
| zero => ext; simp
| succ n ihn => rw [pow_succ, ihn, mul_def, smulRight_comp, smul_eq_mul, pow_succ']

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
n : ℕ
ihn : smulRight 1 c ^ n = smulRight 1 (c ^ n)
⊢ smulRight 1 c ^ (n + 1) = smulRight 1 (c ^ (n + 1))

Tactic:
rw [pow_succ, ihn, mul_def, smulRight_comp, smul_eq_mul, pow_succ']

Result:
no goals

Proof state:
case zero.h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
⊢ (smulRight 1 c ^ 0) 1 = (smulRight 1 (c ^ 0)) 1

Tactic:
simp

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
⊢ smulRight 1 c ^ 0 = smulRight 1 (c ^ 0)

Tactic:
ext

Result:
case zero.h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
⊢ (smulRight 1 c ^ 0) 1 = (smulRight 1 (c ^ 0)) 1
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma genWeightSpace_chainTopCoeff_add_one_zsmul_add :
    genWeightSpace M ((chainTopCoeff α β + 1 : ℤ) • α + β : L → R) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M ((↑(chainTopCoeff α β) + 1) • α + ⇑β) = ⊥

Tactic:
rw [← genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα, ← Nat.cast_smul_eq_nsmul ℤ,
  Nat.cast_add, Nat.cast_one]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_admissibleIndex_of_mem_box_aux₂ (x : ℝ) (a : ℤ) :
    x ≤ a ↔ (⌈n * x⌉ - 1 + 1) / (n : ℝ) ≤ a

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑n * ↑a = ↑(↑n * a)

Tactic:
norm_cast

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ x ≤ ↑a ↔ (↑⌈↑n * x⌉ - 1 + 1) / ↑n ≤ ↑a

Tactic:
rw [sub_add_cancel, div_le_iff₀' h,
  show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
  Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_left h]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
⊢ x ≤ ↑a ↔ (↑⌈↑n * x⌉ - 1 + 1) / ↑n ≤ ↑a

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero

Result:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ x ≤ ↑a ↔ (↑⌈↑n * x⌉ - 1 + 1) / ↑n ≤ ↑a
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem linearIndependent_of_isOrthoᵢ {B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V} {v : n → V₁}
    (hv₁ : B.IsOrthoᵢ v) (hv₂ : ∀ i, ¬B.IsOrtho (v i) (v i)) : LinearIndependent K₁ v

Proof state:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
⊢ w i = 0

Tactic:
have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
  apply Finset.sum_eq_single_of_mem i hi
  intro j _hj hij
  rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]

Result:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
hsum : ∑ j ∈ s, I₁ (w j) • (B (v j)) (v i) = I₁ (w i) • (B (v i)) (v i)
⊢ w i = 0

Proof state:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
⊢ ∀ (s : Finset n) (g : n → K₁), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
intro s w hs i hi

Result:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
⊢ w i = 0