harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_deriv_comp_smul_deriv' {f f' : ℝ → ℝ} {g g' : ℝ → E} (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
    (hf' : ContinuousOn f' [[a, b]]) (hg : ContinuousOn g [[f a, f b]])
    (hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x)
    (hg' : ContinuousOn g' (f '' [[a, b]])) :
    (∫ x in a..b, f' x • (g' ∘ f) x) = (g ∘ f) b - (g ∘ f) a

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g g' : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (f a ⊓ f b) (f a ⊔ f b), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ g (f b) - g (f a) = (g ∘ f) b - (g ∘ f) a

E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g g' : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (f a ⊓ f b) (f a ⊔ f b), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
exacts [rfl, intermediate_value_uIcc hf]

Result:
no goals

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g g' : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (f a ⊓ f b) (f a ⊔ f b), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a

Tactic:
rw [integral_comp_smul_deriv'' hf hff' hf' hg',
  integral_eq_sub_of_hasDeriv_right hg hgg' (hg'.mono _).intervalIntegrable]

Result:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g g' : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (f a ⊓ f b) (f a ⊔ f b), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ g (f b) - g (f a) = (g ∘ f) b - (g ∘ f) a

E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g g' : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (f a ⊓ f b) (f a ⊔ f b), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ [[f a, f b]] ⊆ f '' [[a, b]]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_push {a : α} {l : Array α} :
    (l.push a).attach =
      (l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩

Proof state:
α : Type ?u.10502
a : α
l : Array α
⊢ a ∈ l.push a

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.push a).attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          { toList := toList✝ }.attach).push
      ⟨a, ⋯⟩

Tactic:
rw [attach_congr (List.push_toArray _ _)]

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (toList✝ ++ [a]).toArray.attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          { toList := toList✝ }.attach).push
      ⟨a, ⋯⟩

Proof state:
α : Type u_1
a : α
l : Array α
⊢ (l.push a).attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          l.attach).push
      ⟨a, ⋯⟩

Tactic:
cases l

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.push a).attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          { toList := toList✝ }.attach).push
      ⟨a, ⋯⟩

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (toList✝ ++ [a]).toArray.attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          { toList := toList✝ }.attach).push
      ⟨a, ⋯⟩

Tactic:
simp [Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_zsmul' (a b : α) (m : ℤ) :
    toIocMod hp (a + m • p) b = toIocMod hp a b + m • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + m • p) b = toIocMod hp a b + m • p

Tactic:
simp only [toIocMod, toIocDiv_add_zsmul', sub_smul, sub_add]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem tail_ofFn {n : ℕ} (f : Fin n.succ → α) : tail (ofFn f) = ofFn fun i => f i.succ :=
  (ofFn_get _).symm.trans <| by
    congr
    funext i
    rw [get_tail, get_ofFn]
    rfl

Proof state:
case e_a.h
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ f ⟨↑i + 1, ⋯⟩ = f i.succ

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ ofFn (ofFn f).tail.get = ofFn fun i => f i.succ

Tactic:
congr

Result:
case e_a
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).tail.get = fun i => f i.succ

Proof state:
case e_a.h
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ (ofFn f).tail.get i = f i.succ

Tactic:
rw [get_tail, get_ofFn]

Result:
case e_a.h
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ f ⟨↑i + 1, ⋯⟩ = f i.succ

Proof state:
case e_a
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).tail.get = fun i => f i.succ

Tactic:
funext i

Result:
case e_a.h
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ (ofFn f).tail.get i = f i.succ
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex [IsNoetherian R M] (f : End R M)
    (μ : R) (k : ℕ∞) :
    f.genEigenspace μ k ≤ f.genEigenspace μ (maxUnifEigenspaceIndex f μ)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ⊤

Tactic:
exact (f.genEigenspace μ).monotone le_top

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
rw [← genEigenspace_top_eq_maxUnifEigenspaceIndex]

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ⊤
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem one_le_rpow_of_pos_of_le_one_of_neg {x : ℝ≥0∞} {z : ℝ} (hx1 : 0 < x) (hx2 : x ≤ 1)
    (hz : z < 0) : 1 ≤ x ^ z

Proof state:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x ≤ 1
⊢ 1 ≤ ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx1),
  NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)]

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
⊢ 1 ≤ x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)

Result:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x ≤ 1
⊢ 1 ≤ ↑x ^ z

Proof state:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x ≤ 1
⊢ 1 ≤ ↑x ^ z

Tactic:
simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢

Result:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x ≤ 1
⊢ 1 ≤ ↑x ^ z
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem geom_series_eq_inverse (x : R) (h : ‖x‖ < 1) :
    ∑' i, x ^ i = Ring.inverse (1 - x)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ Ring.inverse ↑(Units.oneSub x h) = Ring.inverse (1 - x)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ↑(Units.oneSub x h)⁻¹ = Ring.inverse (1 - x)

Tactic:
rw [← Ring.inverse_unit]

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ Ring.inverse ↑(Units.oneSub x h) = Ring.inverse (1 - x)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ i = Ring.inverse (1 - x)

Tactic:
change (Units.oneSub x h) ⁻¹ = Ring.inverse (1 - x)

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ↑(Units.oneSub x h)⁻¹ = Ring.inverse (1 - x)
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem isQuadratic_χ₈' : χ₈'.IsQuadratic

Proof state:
⊢ ∀ (a : ZMod 8), χ₈' a = 0 ∨ χ₈' a = 1 ∨ χ₈' a = -1

Tactic:
decide

Result:
no goals

Proof state:
⊢ χ₈'.IsQuadratic

Tactic:
unfold MulChar.IsQuadratic

Result:
⊢ ∀ (a : ZMod 8), χ₈' a = 0 ∨ χ₈' a = 1 ∨ χ₈' a = -1
-- Mathlib/Order/Filter/Lift.lean
theorem HasBasis.lift {ι} {p : ι → Prop} {s : ι → Set α} {f : Filter α} (hf : f.HasBasis p s)
    {β : ι → Type*} {pg : ∀ i, β i → Prop} {sg : ∀ i, β i → Set γ} {g : Set α → Filter γ}
    (hg : ∀ i, (g (s i)).HasBasis (pg i) (sg i)) (gm : Monotone g) :
    (f.lift g).HasBasis (fun i : Σi, β i => p i.1 ∧ pg i.1 i.2) fun i : Σi, β i => sg i.1 i.2

Proof state:
α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
⊢ (f.lift g).HasBasis (fun i => p i.fst ∧ pg i.fst i.snd) fun i => sg i.fst i.snd

Tactic:
refine ⟨fun t => (hf.mem_lift_iff hg gm).trans ?_⟩

Result:
α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
t : Set γ
⊢ (∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ t) ↔ ∃ i, (p i.fst ∧ pg i.fst i.snd) ∧ sg i.fst i.snd ⊆ t

Proof state:
α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
t : Set γ
⊢ (∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ t) ↔ ∃ i, (p i.fst ∧ pg i.fst i.snd) ∧ sg i.fst i.snd ⊆ t

Tactic:
simp [Sigma.exists, and_assoc, exists_and_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem maxDegree_lt_card_verts [DecidableRel G.Adj] [Nonempty V] :
    G.maxDegree < Fintype.card V

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V

Tactic:
apply G.degree_lt_card_verts v

Result:
no goals

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.maxDegree < Fintype.card V

Tactic:
rw [hv]

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
⊢ G.maxDegree < Fintype.card V

Tactic:
obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.maxDegree < Fintype.card V
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_zero [Fintype m] (v : m → α) : v ᵥ* (0 : Matrix m n α) = 0

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
x✝ : n
⊢ (v ᵥ* 0) x✝ = 0 x✝

Tactic:
simp [vecMul]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
⊢ v ᵥ* 0 = 0

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
v : m → α
x✝ : n
⊢ (v ᵥ* 0) x✝ = 0 x✝
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuousOn_multiset_prod {f : ι → X → M} (s : Multiset ι) {t : Set X} :
    (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (s.map fun i => f i a).prod) t

Proof state:
case mk
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, ContinuousOn (f i) t) →
    ContinuousOn (fun a => (Multiset.map (fun i => f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) t

Tactic:
simpa using continuousOn_list_prod l

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
⊢ (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (Multiset.map (fun i => f i a) s).prod) t

Tactic:
rcases s with ⟨l⟩

Result:
case mk
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, ContinuousOn (f i) t) →
    ContinuousOn (fun a => (Multiset.map (fun i => f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) t
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem coe_sup_of_nonempty {s : Finset β} (h : s.Nonempty) (f : β → α) :
    (↑(s.sup f) : WithBot α) = s.sup ((↑) ∘ f)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
h : s.Nonempty
f : β → α
⊢ ↑(s.sup f) = s.sup (WithBot.some ∘ f)

Tactic:
simp only [← sup'_eq_sup h, coe_sup' h]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma mem_freeLocus_iff_tensor (p : PrimeSpectrum R)
    (Rₚ) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p.asIdeal] :
    p ∈ freeLocus R M ↔ Module.Free Rₚ (Rₚ ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
inst✝² : CommRing Rₚ
inst✝¹ : Algebra R Rₚ
inst✝ : IsLocalization.AtPrime Rₚ p.asIdeal
⊢ p ∈ freeLocus R M ↔ Free Rₚ (Rₚ ⊗[R] M)

Tactic:
have := (isLocalizedModule_iff_isBaseChange p.asIdeal.primeCompl _ _).mpr
  (TensorProduct.isBaseChange R M Rₚ)

Result:
R : Type uR
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
inst✝² : CommRing Rₚ
inst✝¹ : Algebra R Rₚ
inst✝ : IsLocalization.AtPrime Rₚ p.asIdeal
this : IsLocalizedModule p.asIdeal.primeCompl ((TensorProduct.mk R Rₚ M) 1)
⊢ p ∈ freeLocus R M ↔ Free Rₚ (Rₚ ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
inst✝² : CommRing Rₚ
inst✝¹ : Algebra R Rₚ
inst✝ : IsLocalization.AtPrime Rₚ p.asIdeal
this : IsLocalizedModule p.asIdeal.primeCompl ((TensorProduct.mk R Rₚ M) 1)
⊢ p ∈ freeLocus R M ↔ Free Rₚ (Rₚ ⊗[R] M)

Tactic:
exact mem_freeLocus_of_isLocalization p Rₚ (f := TensorProduct.mk R Rₚ M 1)

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem vectorSpan_isOrtho_altitude_direction {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2)) :
    vectorSpan ℝ (s.points '' ↑(Finset.univ.erase i)) ⟂ (s.altitude i).direction

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
⊢ vectorSpan ℝ (s.points '' ↑(univ.erase i)) ⟂
    (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
exact (Submodule.isOrtho_orthogonal_right _).mono_right inf_le_left

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
⊢ vectorSpan ℝ (s.points '' ↑(univ.erase i)) ⟂ (s.altitude i).direction

Tactic:
rw [direction_altitude]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
⊢ vectorSpan ℝ (s.points '' ↑(univ.erase i)) ⟂
    (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
-- Mathlib/RingTheory/UniqueFactorizationDomain/Finsupp.lean
theorem associated_of_factorization_eq (a b : α) (ha : a ≠ 0) (hb : b ≠ 0)
    (h : factorization a = factorization b) : Associated a b

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : factorization a = factorization b
⊢ a ~ᵤ b

Tactic:
simp_rw [factorization, AddEquiv.apply_eq_iff_eq] at h

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : normalizedFactors a = normalizedFactors b
⊢ a ~ᵤ b

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : normalizedFactors a = normalizedFactors b
⊢ a ~ᵤ b

Tactic:
rwa [associated_iff_normalizedFactors_eq_normalizedFactors ha hb]

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/NormedValued.lean
theorem one_le_norm_iff : 1 ≤ ‖x‖ ↔ 1 ≤ val.v x

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
⊢ 1 ≤ ‖x‖ ↔ 1 ≤ v x

Tactic:
simpa only [_root_.map_one] using (Valuation.RankOne.strictMono val.v).le_iff_le (a := 1)

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem eventually_imp_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∀ᶠ x in f, p x → q) ↔ (∃ᶠ x in f, p x) → q

Proof state:
α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q

Tactic:
simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem map_id : map (f₂ := f₁) (g₂ := g₁) (id V₁) (id W₁) rfl rfl = id (f₁.equalizer g₁)

Proof state:
V₁ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst✝ : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
⊢ map (id V₁) (id W₁) ⋯ ⋯ = id ↥(f₁.equalizer g₁)

Tactic:
ext

Result:
case H.a
V₁ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst✝ : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
x✝ : ↥(f₁.equalizer g₁)
⊢ ↑((map (id V₁) (id W₁) ⋯ ⋯) x✝) = ↑((id ↥(f₁.equalizer g₁)) x✝)

Proof state:
case H.a
V₁ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst✝ : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
x✝ : ↥(f₁.equalizer g₁)
⊢ ↑((map (id V₁) (id W₁) ⋯ ⋯) x✝) = ↑((id ↥(f₁.equalizer g₁)) x✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_zero [Nontrivial R] : W'.Nonsingular ![1, 1, 0]

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
⊢ W'.Nonsingular ![1, 1, 0]

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
⊢ ¬(3 * 1 ^ 2 = 0 ∧ 2 * 1 = 0 ∧ W'.a₁ * 1 * 1 = 0)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
⊢ ¬(3 * 1 ^ 2 = 0 ∧ 2 * 1 = 0 ∧ W'.a₁ * 1 * 1 = 0)

Tactic:
exact fun h => one_ne_zero <| by linear_combination (norm := ring1) h.1 - h.2.1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
h : 3 * 1 ^ 2 = 0 ∧ 2 * 1 = 0 ∧ W'.a₁ * 1 * 1 = 0
⊢ 1 = 0

Tactic:
linear_combination (norm := ring1) h.1 - h.2.1

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma op_smul_set_stabilizer_subset (ha : a ∈ s) : (stabilizer G s : Set G) <• a ⊆ s :=
  smul_set_subset_iff.2 fun b hb ↦ by rw [← hb]; exact smul_mem_smul_set ha

Proof state:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ s

Tactic:
rw [← hb]

Result:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ b •> s

Proof state:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ b •> s

Tactic:
exact smul_mem_smul_set ha

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map₂_comm (f : α → α → β) (comm : ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁) :
    map₂ f xs ys = map₂ f ys xs

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f xs ys = map₂ f ys xs

Tactic:
induction xs, ys using Vector.inductionOn₂ <;> simp_all

Result:
no goals