harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean
theorem sum_characters_eq_zero ⦃a : ZMod n⦄ (ha : a ≠ 1) :
    ∑ χ : DirichletCharacter R n, χ a = 0

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ χ : DirichletCharacter R n, χ a = 0

Tactic:
refine eq_zero_of_mul_eq_self_left hχ ?_

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ χ a * ∑ χ : DirichletCharacter R n, χ a = ∑ χ : DirichletCharacter R n, χ a

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ x : DirichletCharacter R n, (χ * x) a = ∑ χ : DirichletCharacter R n, χ a

Tactic:
exact Fintype.sum_bijective _ (Group.mulLeft_bijective χ) _ _ fun χ' ↦ rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
⊢ ∑ χ : DirichletCharacter R n, χ a = 0

Tactic:
obtain ⟨χ, hχ⟩ := exists_apply_ne_one_of_hasEnoughRootsOfUnity R ha

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ χ : DirichletCharacter R n, χ a = 0

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ χ a * ∑ χ : DirichletCharacter R n, χ a = ∑ χ : DirichletCharacter R n, χ a

Tactic:
simp only [Finset.mul_sum, ← MulChar.mul_apply]

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ x : DirichletCharacter R n, (χ * x) a = ∑ χ : DirichletCharacter R n, χ a
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.fderivWithin_right_apply
    {f : F → G} {k : F → F} {s : Set F} {x₀ : F}
    (hf : ContDiffWithinAt 𝕜 n f s x₀) (hk : ContDiffWithinAt 𝕜 m k s x₀)
    (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) (hx₀s : x₀ ∈ s) :
    ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 f s x (k x)) s x₀ :=
  ContDiffWithinAt.fderivWithin_apply
    (ContDiffWithinAt.comp (x₀, x₀) hf contDiffWithinAt_snd <| prod_subset_preimage_snd s s)
    contDiffWithinAt_id hk hs hmn hx₀s (by rw [preimage_id'])

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m n : WithTop ℕ∞
f : F → G
k : F → F
s : Set F
x₀ : F
hf : ContDiffWithinAt 𝕜 n f s x₀
hk : ContDiffWithinAt 𝕜 m k s x₀
hs : UniqueDiffOn 𝕜 s
hmn : m + 1 ≤ n
hx₀s : x₀ ∈ s
⊢ s ⊆ (fun x => x) ⁻¹' s

Tactic:
rw [preimage_id']

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem norm_sum_neg_one_pow_le (n : ℕ) : ‖∑ i ∈ range n, (-1 : ℝ) ^ i‖ ≤ 1

Proof state:
n : ℕ
⊢ ‖if Even n then 0 else 1‖ ≤ 1

Tactic:
split_ifs <;> norm_num

Result:
no goals

Proof state:
n : ℕ
⊢ ‖∑ i ∈ Finset.range n, (-1) ^ i‖ ≤ 1

Tactic:
rw [neg_one_geom_sum]

Result:
n : ℕ
⊢ ‖if Even n then 0 else 1‖ ≤ 1
-- Mathlib/Topology/Category/CompHausLike/Limits.lean
lemma finiteCoproduct.hom_ext {B : CompHausLike P} (f g : finiteCoproduct X ⟶ B)
    (h : ∀ a : α, finiteCoproduct.ι X a ≫ f = finiteCoproduct.ι X a ≫ g) : f = g

Proof state:
case h.h.mk
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩

Tactic:
apply_fun (fun q ↦ q x) at h

Result:
case h.h.mk
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : (ConcreteCategory.hom (ι X a ≫ f)) x = (ConcreteCategory.hom (ι X a ≫ g)) x
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩

Proof state:
case h.h.mk
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩

Tactic:
specialize h a

Result:
case h.h.mk
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : ι X a ≫ f = ι X a ≫ g
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩

Proof state:
case h.h.mk
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
a : α
x : ↑(X a).toTop
h : (ConcreteCategory.hom (ι X a ≫ f)) x = (ConcreteCategory.hom (ι X a ≫ g)) x
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩

Tactic:
exact h

Result:
no goals

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g

Tactic:
ext ⟨a, x⟩

Result:
case h.h.mk
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom f) ⟨a, x⟩ = (ConcreteCategory.hom g) ⟨a, x⟩
-- Mathlib/Data/Set/Prod.lean
theorem offDiag_insert (ha : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Proof state:
α : Type u_1
s : Set α
b : α
hb : b ∈ s
ha : b ∉ s
⊢ False

Tactic:
exact ha hb

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ s → a_1 ∉ {a}

Tactic:
rintro b hb (rfl : b = a)

Result:
α : Type u_1
s : Set α
b : α
hb : b ∈ s
ha : b ∉ s
⊢ False

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Tactic:
rw [insert_eq, union_comm, offDiag_union, offDiag_singleton, union_empty, union_right_comm]

Result:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ Disjoint s {a}

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ Disjoint s {a}

Tactic:
rw [disjoint_left]

Result:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ s → a_1 ∉ {a}
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem τ_symm_apply_infinity :
    Equiv.symm τ ∞ = fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩

Proof state:
A B : Grp
f : A ⟶ B
⊢ (Equiv.symm τ) ∞ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
rw [tau, Equiv.symm_swap, Equiv.swap_apply_right]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
theorem tendsto_iff_tendstoUniformly {ι : Type*} {F : ι → C₀(α, β)} {f : C₀(α, β)} {l : Filter ι} :
    Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => F i) f l

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
ι : Type u_2
F : ι → α →C₀ β
f : α →C₀ β
l : Filter ι
⊢ Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l

Tactic:
simpa only [Metric.tendsto_nhds] using
  @BoundedContinuousFunction.tendsto_iff_tendstoUniformly _ _ _ _ _ (fun i => (F i).toBCF)
    f.toBCF l

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
theorem UniqueMDiffOn.uniqueDiffWithinAt_range_inter (hs : UniqueMDiffOn I s) (x : M) (y : E)
    (hy : y ∈ (extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) :
    UniqueDiffWithinAt 𝕜 (range I ∩ (extChartAt I x).symm ⁻¹' s) y

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : E
hy : y ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s
⊢ UniqueDiffWithinAt 𝕜 (range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s) y

Tactic:
apply (hs.uniqueDiffOn_target_inter x y hy).mono

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : E
hy : y ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s
⊢ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s ⊆ range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : E
hy : y ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s
⊢ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s ⊆ range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s

Tactic:
apply inter_subset_inter_left _ (extChartAt_target_subset_range x)

Result:
no goals
-- Mathlib/Algebra/Order/Invertible.lean
theorem invOf_pos [Invertible a] : 0 < ⅟ a ↔ 0 < a :=
  haveI : 0 < a * ⅟ a

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ 0 < a * ⅟a

Tactic:
simp only [mul_invOf_self, zero_lt_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma sum_boole_mul (s : Finset ι) (f : ι → α) (i : ι) :
    ∑ j ∈ s, ite (i = j) 1 0 * f j = ite (i ∈ s) (f i) 0

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : ι
⊢ ∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equiv.lean
theorem isUniformInducing (h : α ≃ᵤ β) : IsUniformInducing h :=
  IsUniformInducing.of_comp h.uniformContinuous h.symm.uniformContinuous <| by
    simp only [symm_comp_self, IsUniformInducing.id]

Proof state:
α : Type u
β : Type u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
h : α ≃ᵤ β
⊢ IsUniformInducing (⇑h.symm ∘ ⇑h)

Tactic:
simp only [symm_comp_self, IsUniformInducing.id]

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Even.smul_even [SMul β γ] (hf : f.Even) (hg : g.Even) : (f • g).Even

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝ : SMul β γ
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f • g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝ : SMul β γ
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = (f • g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝ : SMul β γ
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f • g) (-a) = (f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addX_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) : W.addX P Q / W.addZ P Q =
    W.toAffine.addX (P x / P z) (Q x / Q z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.addX P Q / W.addZ P Q =
    (toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
rw [addX_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
  toAffine_addX_of_ne hPz hQz <| sub_ne_zero.mpr hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
    l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h)

Proof state:
α : Type u_1
l₁ l₂ : List α
w : l₁ = l₂
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₂.attachWith P ⋯

Tactic:
subst w

Result:
α : Type u_1
l₁ : List α
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₁.attachWith P ⋯

Proof state:
α : Type u_1
l₁ : List α
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₁.attachWith P ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian. -/
lemma gaussianReal_map_mul_const (c : ℝ) :
    (gaussianReal μ v).map (· * c) = gaussianReal (c * μ) (⟨c^2, sq_nonneg _⟩ * v)

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
exact gaussianReal_map_const_mul c

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x => x * c) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
simp_rw [mul_comm _ c]

Result:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_reverse (a : Vector α n) : a.reverse.toList = a.toList.reverse

Proof state:
α : Type u_1
n : Nat
a : Vector α n
⊢ a.reverse.toList = a.toList.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem ofDual_compares_ofDual [LT α] {a b : αᵒᵈ} {o : Ordering} :
    Compares o (ofDual a) (ofDual b) ↔ Compares o b a

Proof state:
case lt
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ lt.Compares (ofDual a) (ofDual b) ↔ lt.Compares b a

case eq
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ eq.Compares (ofDual a) (ofDual b) ↔ eq.Compares b a

case gt
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ gt.Compares (ofDual a) (ofDual b) ↔ gt.Compares b a

Tactic:
exacts [Iff.rfl, eq_comm, Iff.rfl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
o : Ordering
⊢ o.Compares (ofDual a) (ofDual b) ↔ o.Compares b a

Tactic:
cases o

Result:
case lt
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ lt.Compares (ofDual a) (ofDual b) ↔ lt.Compares b a

case eq
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ eq.Compares (ofDual a) (ofDual b) ↔ eq.Compares b a

case gt
α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
⊢ gt.Compares (ofDual a) (ofDual b) ↔ gt.Compares b a
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comap_incl_self : comap N.incl N = ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ Submodule.comap (↑N).subtype ↑N = ⊤

Tactic:
rw [Submodule.comap_subtype_self]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ comap N.incl N = ⊤

Tactic:
simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, top_toSubmodule]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ Submodule.comap (↑N).subtype ↑N = ⊤
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem of_measurable_inverse_on_range {g : range f → α} (hf₁ : Measurable f)
    (hf₂ : MeasurableSet (range f)) (hg : Measurable g) (H : LeftInverse g (rangeFactorization f)) :
    MeasurableEmbedding f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
e : α ≃ᵐ ↑(range f) :=
  { toFun := rangeFactorization f, invFun := g, left_inv := H, right_inv := ⋯, measurable_toFun := ⋯,
    measurable_invFun := hg }
⊢ MeasurableEmbedding f

Tactic:
exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
⊢ MeasurableEmbedding f

Tactic:
set e : α ≃ᵐ range f :=
  ⟨⟨rangeFactorization f, g, H, H.rightInverse_of_surjective surjective_onto_range⟩,
    hf₁.subtype_mk, hg⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
e : α ≃ᵐ ↑(range f) :=
  { toFun := rangeFactorization f, invFun := g, left_inv := H, right_inv := ⋯, measurable_toFun := ⋯,
    measurable_invFun := hg }
⊢ MeasurableEmbedding f
-- Mathlib/Data/List/Basic.lean
theorem getLast_replicate_succ (m : ℕ) (a : α) :
    (replicate (m + 1) a).getLast (ne_nil_of_length_eq_add_one (length_replicate _ _)) = a

Proof state:
α : Type u
m : ℕ
a : α
⊢ (replicate m a ++ [a]).getLast ⋯ = a

Tactic:
exact getLast_append_singleton _

Result:
no goals

Proof state:
α : Type u
m : ℕ
a : α
⊢ (replicate (m + 1) a).getLast ⋯ = a

Tactic:
simp only [replicate_succ']

Result:
α : Type u
m : ℕ
a : α
⊢ (replicate m a ++ [a]).getLast ⋯ = a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isSome_getValueCast?_eq_isSome_getEntry? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)}
    {a : α} : (getValueCast? a l).isSome = (getEntry? a l).isSome

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
⊢ (getValueCast? a l).isSome = (getEntry? a l).isSome

Tactic:
rw [getValueCast?_eq_getEntry?, Option.isSome_dmap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_iff_right_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ y) ↔ p → x = y

Proof state:
p : Prop
inst✝ : Decidable p
x y : Prop
⊢ ((if p then x else y) ↔ y) ↔ p → x = y

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidtNormed_unit_length' {f : ι → E} {n : ι} (hn : gramSchmidtNormed 𝕜 f n ≠ 0) :
    ‖gramSchmidtNormed 𝕜 f n‖ = 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0
⊢ ‖(↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n‖ = 1

Tactic:
rw [norm_smul_inv_norm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0
⊢ gramSchmidt 𝕜 f n ≠ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0
⊢ gramSchmidt 𝕜 f n ≠ 0

Tactic:
simpa using hn

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
hn : gramSchmidtNormed 𝕜 f n ≠ 0
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1

Tactic:
rw [gramSchmidtNormed] at *

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0
⊢ ‖(↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n‖ = 1
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem exists_pos_measure_of_not_restrict_le_zero (hi : ¬v ≤[i] 0) :
    ∃ j : Set α, MeasurableSet j ∧ j ⊆ i ∧ 0 < v j

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j

Tactic:
have hi₁ : MeasurableSet i := measurable_of_not_restrict_le_zero _ hi

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j

Tactic:
rw [restrict_le_restrict_iff _ _ hi₁] at hi

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑0 j
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑0 j
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j

Tactic:
push_neg at hi

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₁ : MeasurableSet i
hi : ∃ j, MeasurableSet j ∧ j ⊆ i ∧ ↑0 j < ↑v j
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : LinearOrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₁ : MeasurableSet i
hi : ∃ j, MeasurableSet j ∧ j ⊆ i ∧ ↑0 j < ↑v j
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j

Tactic:
exact hi

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem conj_cpow (x : ℂ) (n : ℂ) (hx : x.arg ≠ π) : conj x ^ n = conj (x ^ conj n)

Proof state:
x n : ℂ
hx : x.arg ≠ π
⊢ (starRingEnd ℂ) x ^ n = (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)

Tactic:
rw [conj_cpow_eq_ite, if_neg hx]

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
theorem mem_of_mem_toEnumFinset {p : α × ℕ} (h : p ∈ m.toEnumFinset) : p.1 ∈ m :=
  have := (m.mem_toEnumFinset p).mp h; Multiset.count_pos.mp (by omega)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
p : α × ℕ
h : p ∈ m.toEnumFinset
this : p.2 < count p.1 m
⊢ 0 < count p.1 m

Tactic:
omega

Result:
no goals