harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Jensen.lean
/-- Canonical form of the **equality case of Jensen's equality**.

For a strictly convex function `f` and nonnegative weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` with nonzero
weight are all equal (and in fact all equal to their center of mass wrt `w`). -/
lemma StrictConvexOn.map_sum_eq_iff' (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i)
    (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) :
    f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔
      ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i

Tactic:
have hw' (i) (_ : i ∈ t) : w i • f (p i) ≠ 0 → w i ≠ 0 := by aesop

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem div_eq_one' {r : R} (hr : r ∈ S) : r /ₒ ⟨r, hr⟩ = 1

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ⟨r, hr⟩ • 1 = 1 • r

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ↑⟨r, hr⟩ * ↑1 = 1 * ↑⟨r, hr⟩

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ r /ₒ ⟨r, hr⟩ = 1

Tactic:
rw [OreLocalization.one_def, oreDiv_eq_iff]

Result:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ∃ u v, u • 1 = v • r ∧ ↑u * ↑1 = v * ↑⟨r, hr⟩

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ∃ u v, u • 1 = v • r ∧ ↑u * ↑1 = v * ↑⟨r, hr⟩

Tactic:
exact ⟨⟨r, hr⟩, 1, by simp, by simp⟩

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.comp_addHom [Add α] [Add γ] (h : Periodic f c) (g : AddHom γ α) (g_inv : α → γ)
    (hg : RightInverse g_inv g) : Periodic (f ∘ g) (g_inv c) := fun x => by
  simp only [hg c, h (g x), map_add, comp_apply]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝¹ : Add α
inst✝ : Add γ
h : Periodic f c
g : γ →ₙ+ α
g_inv : α → γ
hg : RightInverse g_inv ⇑g
x : γ
⊢ (f ∘ ⇑g) (x + g_inv c) = (f ∘ ⇑g) x

Tactic:
simp only [hg c, h (g x), map_add, comp_apply]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem iterate_derivative_at_1_eq_zero_of_lt (n : ℕ) {ν k : ℕ} :
    k < n - ν → (Polynomial.derivative^[k] (bernsteinPolynomial R n ν)).eval 1 = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < n - ν → eval 1 ((⇑derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
intro w

Result:
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
rw [flip' _ _ _ (tsub_pos_iff_lt.mp (pos_of_gt w)).le]

Result:
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative)^[k] ((bernsteinPolynomial R n (n - ν)).comp (1 - X))) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative)^[k] ((bernsteinPolynomial R n (n - ν)).comp (1 - X))) = 0

Tactic:
simp [Polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
protected lemma mul_nonneg_iff_of_pos_right (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a

Proof state:
a b : ℤ
hb : 0 < b
⊢ 0 ≤ a * b ↔ 0 ≤ a

Tactic:
simpa using (Int.mul_le_mul_iff_of_pos_right hb : 0 * b ≤ a * b ↔ 0 ≤ a)

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem projKerOfRightInverse_comp_inv [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂)
    (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) (y : M₂) :
    f₁.projKerOfRightInverse f₂ h (f₂ y) = 0 :=
  Subtype.ext_iff_val.2 <| by simp [h y]

Proof state:
R : Type u_1
inst✝⁹ : Ring R
R₂ : Type u_2
inst✝⁸ : Ring R₂
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
M₂ : Type u_5
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : IsTopologicalAddGroup M
f₁ : M →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M
h : Function.RightInverse ⇑f₂ ⇑f₁
y : M₂
⊢ ↑((f₁.projKerOfRightInverse f₂ h) (f₂ y)) = ↑0

Tactic:
simp [h y]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem isUnit_iff_ker_eq_bot [FiniteDimensional K V] (f : V →ₗ[K] V) :
    IsUnit f ↔ (LinearMap.ker f) = ⊥

Proof state:
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f → ker f = ⊥

Tactic:
rintro ⟨u, rfl⟩

Result:
case mp.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
u : (V →ₗ[K] V)ˣ
⊢ ker ↑u = ⊥

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ ker f = ⊥ → IsUnit f

Tactic:
intro h_inj

Result:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : ker f = ⊥
⊢ IsUnit f

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f ↔ ker f = ⊥

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f → ker f = ⊥

case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ ker f = ⊥ → IsUnit f

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : ker f = ⊥
⊢ IsUnit f

Tactic:
rw [ker_eq_bot] at h_inj

Result:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective ⇑f
⊢ IsUnit f

Proof state:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective ⇑f
⊢ IsUnit f

Tactic:
exact ⟨⟨f, (LinearEquiv.ofInjectiveEndo f h_inj).symm.toLinearMap,
  LinearEquiv.ofInjectiveEndo_right_inv f h_inj, LinearEquiv.ofInjectiveEndo_left_inv f h_inj⟩,
  rfl⟩

Result:
no goals

Proof state:
case mp.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
u : (V →ₗ[K] V)ˣ
⊢ ker ↑u = ⊥

Tactic:
exact LinearMap.ker_eq_bot_of_inverse u.inv_mul

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem repeat_eq_nil (α : TypeVec 0) : repeatEq α = nilFun

Proof state:
α : TypeVec.{u_1} 0
⊢ α.repeatEq = nilFun

Tactic:
ext i

Result:
case a.h
α : TypeVec.{u_1} 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ α.repeatEq i x✝ = nilFun i x✝

Proof state:
case a.h
α : TypeVec.{u_1} 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ α.repeatEq i x✝ = nilFun i x✝

Tactic:
cases i

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem unit_mateEquiv_symm (α : TwoSquare R₁ H G R₂) (c : C) :
    G.map (adj₁.unit.app c) ≫ α.app _ =
      adj₂.unit.app _ ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app _)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
c : C
⊢ G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c) =
    adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((𝟭 C).obj c))

Tactic:
conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]

Result:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
c : C
⊢ G.map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((𝟭 C).obj c))

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
c : C
⊢ G.map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((𝟭 C).obj c))

Tactic:
exact (unit_mateEquiv adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) c)

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.balance' {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (balance' l x r)

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r
      else if l.size > delta * r.size then l.rotateR x r else l.node' x r).Sized

Tactic:
split_ifs

Result:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).Sized

case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

Tactic:
exact hl.rotateL hr

Result:
no goals

Proof state:
case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
exact hl.node' hr

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.balance' x r).Sized

Tactic:
unfold Ordnode.balance'

Result:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r
      else if l.size > delta * r.size then l.rotateR x r else l.node' x r).Sized

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

Tactic:
exact hl.rotateR hr

Result:
no goals

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).Sized

Tactic:
exact hl.node' hr

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma comap_indep_iff_of_injOn (hf : InjOn f (f ⁻¹' N.E)) :
    (N.comap f).Indep I ↔ N.Indep (f '' I)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I

Tactic:
refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)

Result:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' (f '' I)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I)

Tactic:
rw [comap_indep_iff, and_iff_left_iff_imp]

Result:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I

Proof state:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
hi : N.Indep (f '' I)
⊢ I ⊆ f ⁻¹' (f '' I)

Tactic:
apply subset_preimage_image

Result:
no goals
-- Mathlib/CategoryTheory/Galois/EssSurj.lean
theorem exists_lift_of_continuous (X : Action FintypeCat (Aut F))
    [TopologicalSpace X.V] [DiscreteTopology X.V] [ContinuousSMul (Aut F) X.V] :
    ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Proof state:
C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul (Aut F) X.V.carrier
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Tactic:
obtain ⟨ι, hfin, f, ⟨u⟩⟩ := has_decomp_quotients X

Result:
case intro.intro.intro.intro
C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul (Aut F) X.V.carrier
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i => Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Proof state:
case intro.intro.intro.intro
C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul (Aut F) X.V.carrier
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i => Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Tactic:
choose g gu using (fun i ↦ exists_lift_of_quotient_openSubgroup (f i))

Result:
case intro.intro.intro.intro
C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul (Aut F) X.V.carrier
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i => Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
g : ι → C
gu :
  ∀ (i : ι),
    Nonempty ((functorToAction F).obj (g i) ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i))))
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Proof state:
case intro.intro.intro.intro
C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.carrier
inst✝¹ : DiscreteTopology X.V.carrier
inst✝ : ContinuousSMul (Aut F) X.V.carrier
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i => Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
g : ι → C
gu :
  ∀ (i : ι),
    Nonempty ((functorToAction F).obj (g i) ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i))))
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Tactic:
exact ⟨∐ g, ⟨PreservesCoproduct.iso (functorToAction F) g ≪≫
  Sigma.mapIso (fun i ↦ (gu i).some) ≪≫ u⟩⟩

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem coePNat_prime (v : PrimeMultiset) (p : ℕ+) (h : p ∈ (v : Multiset ℕ+)) : p.Prime

Proof state:
v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
⊢ p.Prime

Tactic:
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩

Result:
case intro.mk.intro
v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : ⟨val✝, hp'⟩ ∈ v
h_eq : Coe.coe ⟨val✝, hp'⟩ = p
⊢ p.Prime

Proof state:
case intro.mk.intro
v : PrimeMultiset
p : ℕ+
h : p ∈ v.toPNatMultiset
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : ⟨val✝, hp'⟩ ∈ v
h_eq : Coe.coe ⟨val✝, hp'⟩ = p
⊢ p.Prime

Tactic:
exact h_eq ▸ hp'

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_insert_insert_of_mem_of_not_mem {s t : Finset α} {x : α} (hxs : x ∈ s) (hxt : x ∉ t) :
    insert x (s \ insert x t) = s \ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
hxs : x ∈ s
hxt : x ∉ t
⊢ insert x (s \ insert x t) = s \ t

Tactic:
rw [sdiff_insert, insert_erase (mem_sdiff.mpr ⟨hxs, hxt⟩)]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Complex.lean
theorem card_primitiveRoots (k : ℕ) : (primitiveRoots k ℂ).card = φ k

Proof state:
k : ℕ
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
by_cases h : k = 0

Result:
case pos
k : ℕ
h : k = 0
⊢ (primitiveRoots k ℂ).card = φ k

case neg
k : ℕ
h : ¬k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Proof state:
case pos
k : ℕ
h : k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
k : ℕ
h : ¬k = 0
⊢ (primitiveRoots k ℂ).card = φ k

Tactic:
exact (isPrimitiveRoot_exp k h).card_primitiveRoots

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem fst_mem_support_of_mem_edges {t u v w : V} (p : G.Walk v w) (he : s(t, u) ∈ p.edges) :
    t ∈ p.support

Proof state:
case intro.intro.inl.intro
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.1, d.toProd.2) ∈ p.edges
⊢ d.toProd.1 ∈ p.support

Tactic:
exact dart_fst_mem_support_of_mem_darts _ hd

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(t, u) ∈ p.edges
⊢ t ∈ p.support

Tactic:
obtain ⟨d, hd, he⟩ := List.mem_map.mp he

Result:
case intro.intro
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he✝ : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.edge = s(t, u)
⊢ t ∈ p.support

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he✝ : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.edge = s(t, u)
⊢ t ∈ p.support

Tactic:
rw [dart_edge_eq_mk'_iff'] at he

Result:
case intro.intro
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he✝ : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t
⊢ t ∈ p.support

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he✝ : s(t, u) ∈ p.edges
d : G.Dart
hd : d ∈ p.darts
he : d.toProd.1 = t ∧ d.toProd.2 = u ∨ d.toProd.1 = u ∧ d.toProd.2 = t
⊢ t ∈ p.support

Tactic:
rcases he with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Result:
case intro.intro.inl.intro
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.1, d.toProd.2) ∈ p.edges
⊢ d.toProd.1 ∈ p.support

case intro.intro.inr.intro
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.2, d.toProd.1) ∈ p.edges
⊢ d.toProd.2 ∈ p.support

Proof state:
case intro.intro.inr.intro
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
d : G.Dart
hd : d ∈ p.darts
he : s(d.toProd.2, d.toProd.1) ∈ p.edges
⊢ d.toProd.2 ∈ p.support

Tactic:
exact dart_snd_mem_support_of_mem_darts _ hd

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
/-- If we reflect colimits of some arbitrary size, then we reflect all finite colimits. -/
lemma ReflectsColimitsOfSize.reflectsFiniteColimits
    (F : C ⥤ D) [ReflectsColimitsOfSize.{w, w₂} F] : ReflectsFiniteColimits F where
  reflects J (sJ : SmallCategory J) fJ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsColimitsOfShape J F

Tactic:
haveI := reflectsSmallestColimits_of_reflectsColimits F

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfShape J F

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfShape J F

Tactic:
exact reflectsColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_eq_pmapImpl : @pmap = @pmapImpl

Proof state:
⊢ @pmap = @List.pmapImpl

Tactic:
funext α β p f L h'

Result:
case h.h.h.h.h.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : List α
h' : ∀ (a : α), a ∈ L → p a
⊢ pmap f L h' = List.pmapImpl f L h'

Proof state:
case h.h.h.h.h.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : List α
h' : ∀ (a : α), a ∈ L → p a
⊢ pmap f L h' = List.pmapImpl f L h'

Tactic:
exact go L h'

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
lemma Topology.IsInducing.specializingMap (hf : IsInducing f)
    (h : StableUnderSpecialization (range f)) : SpecializingMap f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (Set.range f)
⊢ SpecializingMap f

Tactic:
intros x y e

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (Set.range f)
x : X
y : Y
e : flip (fun x1 x2 => x1 ⤳ x2) y (f x)
⊢ ∃ a', flip (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = y

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (Set.range f)
x : X
y : Y
e : flip (fun x1 x2 => x1 ⤳ x2) y (f x)
⊢ ∃ a', flip (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (Set.range f)
x y : X
e : flip (fun x1 x2 => x1 ⤳ x2) (f y) (f x)
⊢ ∃ a', flip (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = f y

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (Set.range f)
x y : X
e : flip (fun x1 x2 => x1 ⤳ x2) (f y) (f x)
⊢ ∃ a', flip (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
exact ⟨_, hf.specializes_iff.mp e, rfl⟩

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem not_summable_iff_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ n, 0 ≤ f n) :
    ¬Summable f ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop

Proof state:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ Tendsto (fun n => ∑ i ∈ range n, f i) atTop atTop

Tactic:
lift f to ℕ → ℝ≥0 using hf

Result:
case intro
f : ℕ → ℝ≥0
⊢ (¬Summable fun i => ↑(f i)) ↔ Tendsto (fun n => ∑ i ∈ range n, (fun i => ↑(f i)) i) atTop atTop

Proof state:
case intro
f : ℕ → ℝ≥0
⊢ (¬Summable fun i => ↑(f i)) ↔ Tendsto (fun n => ∑ i ∈ range n, (fun i => ↑(f i)) i) atTop atTop

Tactic:
simpa using mod_cast NNReal.not_summable_iff_tendsto_nat_atTop

Result:
no goals