harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem orbit_smul (g : G) (a : α) : orbit G (g • a) = orbit G a :=
  (orbit_smul_subset g a).antisymm <|
    calc
      orbit G a = orbit G (g⁻¹ • g • a)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ orbit G a = orbit G (g⁻¹ • g • a)

Tactic:
rw [inv_smul_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EpiMono.lean
theorem reflects_epi_of_reflectsColimit {X Y : C} (f : X ⟶ Y) [ReflectsColimit (span f f) F]
    [Epi (F.map f)] : Epi f

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
⊢ Epi f

Tactic:
have := PushoutCocone.isColimitMkIdId (F.map f)

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi f

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi f

Tactic:
apply
  PushoutCocone.epi_of_isColimitMkIdId _
    (isColimitOfIsColimitPushoutCoconeMap F _ this)

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi f

Tactic:
simp_rw [← F.map_id] at this

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi f
-- Mathlib/Data/Complex/Norm.lean
theorem sq_norm_sub_sq_im (z : ℂ) : ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2

Proof state:
z : ℂ
⊢ ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2

Tactic:
rw [← sq_norm_sub_sq_re, sub_sub_cancel]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_le_map_iff {f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ≤ K ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K ⊔ f.ker

Tactic:
rw [map_le_iff_le_comap, comap_map_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_mul_right_right (m n : Nat) : gcd n (n * m) = n

Proof state:
m n : Nat
⊢ n.gcd (n * m) = n

Tactic:
rw [gcd_comm, gcd_mul_right_left]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
theorem inclusionOfMooreComplexMap_comp_PInfty (X : SimplicialObject A) :
    inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X

Proof state:
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (inclusionOfMooreComplexMap X ≫ PInfty).f 0 = (inclusionOfMooreComplexMap X).f 0

Tactic:
dsimp

Result:
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (inclusionOfMooreComplexMap X).f 0 ≫ 𝟙 (X.obj (Opposite.op (SimplexCategory.mk 0))) =
    (inclusionOfMooreComplexMap X).f 0

Proof state:
case h.succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (inclusionOfMooreComplexMap X ≫ PInfty).f (n + 1) = (inclusionOfMooreComplexMap X).f (n + 1)

Tactic:
exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self

Result:
no goals

Proof state:
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (inclusionOfMooreComplexMap X).f 0 ≫ 𝟙 (X.obj (Opposite.op (SimplexCategory.mk 0))) =
    (inclusionOfMooreComplexMap X).f 0

Tactic:
simp only [comp_id]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X

Tactic:
ext (_|n)

Result:
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (inclusionOfMooreComplexMap X ≫ PInfty).f 0 = (inclusionOfMooreComplexMap X).f 0

case h.succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (inclusionOfMooreComplexMap X ≫ PInfty).f (n + 1) = (inclusionOfMooreComplexMap X).f (n + 1)
-- Mathlib/Probability/Independence/Conditional.lean
theorem condIndepFun_iff_condIndepSet_preimage {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
    (hf : Measurable f) (hg : Measurable g) :
    CondIndepFun m' hm' f g μ ↔
      ∀ s t, MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ

Proof state:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ

Tactic:
simp only [CondIndepFun, CondIndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_simple_mul_ne (w : W) (i : B) : ℓ (s i * w) ≠ ℓ w

Proof state:
case h.e'_2
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) = cs.length (w⁻¹ * cs.simple i)

Tactic:
convert cs.length_inv ?_ using 2

Result:
case h.e'_2.h.e'_6
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.simple i * w = (w⁻¹ * cs.simple i)⁻¹

Proof state:
case h.e'_3
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length w = cs.length w⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.e'_6
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.simple i * w = (w⁻¹ * cs.simple i)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) ≠ cs.length w

Tactic:
convert cs.length_mul_simple_ne w⁻¹ i using 1

Result:
case h.e'_2
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) = cs.length (w⁻¹ * cs.simple i)

case h.e'_3
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length w = cs.length w⁻¹
-- Mathlib/RingTheory/RingHom/Finite.lean
theorem multiple_mem_adjoin_of_mem_localization_adjoin [Algebra R' S] [Algebra R S]
    [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S) (x : S)
    (hx : x ∈ Algebra.adjoin R' s) : ∃ t : M, t • x ∈ Algebra.adjoin R s

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s)
⊢ ∃ t, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)

Tactic:
simp_rw [Algebra.adjoin_eq_span] at hx ⊢

Result:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Submodule.span R' ↑(Submonoid.closure s)
⊢ ∃ t, t • x ∈ Submodule.span R ↑(Submonoid.closure s)

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Algebra.adjoin R' s
⊢ ∃ t, t • x ∈ Algebra.adjoin R s

Tactic:
change ∃ t : M, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)

Result:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Algebra.adjoin R' s
⊢ ∃ t, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Submodule.span R' ↑(Submonoid.closure s)
⊢ ∃ t, t • x ∈ Submodule.span R ↑(Submonoid.closure s)

Tactic:
exact multiple_mem_span_of_mem_localization_span M R' _ _ hx

Result:
no goals

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Algebra.adjoin R' s
⊢ ∃ t, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)

Tactic:
change x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s) at hx

Result:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s)
⊢ ∃ t, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem mk_eq (f : Arrow T) : Arrow.mk f.hom = f

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f : Arrow T
⊢ mk f.hom = f

Tactic:
cases f

Result:
case mk
T : Type u
inst✝ : Category.{v, u} T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk { left := left✝, right := right✝, hom := hom✝ }.hom = { left := left✝, right := right✝, hom := hom✝ }

Proof state:
case mk
T : Type u
inst✝ : Category.{v, u} T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk { left := left✝, right := right✝, hom := hom✝ }.hom = { left := left✝, right := right✝, hom := hom✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_reProdIm (s t : Set ℝ) :
    frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t

Proof state:
s t : Set ℝ
⊢ frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t

Tactic:
simpa only [← preimage_eq_preimage equivRealProdCLM.symm.toHomeomorph.surjective,
  equivRealProdCLM.symm.toHomeomorph.preimage_frontier] using frontier_prod_eq s t

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
/-- Check that indeed any uniform random variable has the uniformPDF. -/
lemma uniformPDF_eq_pdf {s : Set E} (hs : MeasurableSet s) (hu : pdf.IsUniform X s ℙ μ) :
    (fun x ↦ uniformPDF s x μ) =ᵐ[μ] pdf X ℙ μ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hs : MeasurableSet s
hu : IsUniform X s ℙ μ
⊢ (fun x => s.indicator ((μ s)⁻¹ • 1) x) =ᶠ[ae μ] pdf X ℙ μ

Tactic:
exact Filter.EventuallyEq.trans (pdf.IsUniform.pdf_eq hs hu).symm (ae_eq_refl _)

Result:
no goals

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hs : MeasurableSet s
hu : IsUniform X s ℙ μ
⊢ (fun x => uniformPDF s x μ) =ᶠ[ae μ] pdf X ℙ μ

Tactic:
unfold uniformPDF

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hs : MeasurableSet s
hu : IsUniform X s ℙ μ
⊢ (fun x => s.indicator ((μ s)⁻¹ • 1) x) =ᶠ[ae μ] pdf X ℙ μ
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem subset_total (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ⊆ y ∨ y ⊆ x

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ∨ y ⊆ x

Tactic:
obtain h | h := mem_or_subset hx hy

Result:
case inl
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y ∨ y ⊆ x

case inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : y ⊆ x
⊢ x ⊆ y ∨ y ⊆ x

Proof state:
case inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : y ⊆ x
⊢ x ⊆ y ∨ y ⊆ x

Tactic:
exact Or.inr h

Result:
no goals

Proof state:
case inl
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y ∨ y ⊆ x

Tactic:
exact Or.inl (hy.subset_of_mem h)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- No polynomial in the sequence is zero. -/
@[simp]
lemma ne_zero (i : ℕ) : S i ≠ 0 := degree_ne_bot.mp <| by simp [S.degree_eq i]

Proof state:
R : Type u_1
inst✝ : Semiring R
S : Sequence R
i : ℕ
⊢ (↑S i).degree ≠ ⊥

Tactic:
simp [S.degree_eq i]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top (p : ℝ≥0∞) (f : α → E) {φ : α → 𝕜}
    (hφ : AEStronglyMeasurable φ μ) : eLpNorm (φ • f) p μ ≤ eLpNorm φ p μ * eLpNorm f ∞ μ

Proof state:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : BoundedSMul 𝕜 E
p : ℝ≥0∞
f : α → E
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
x✝ : α
⊢ ‖(fun x1 x2 => x1 • x2) (φ x✝) (f x✝)‖₊ ≤ 1 * ‖φ x✝‖₊ * ‖f x✝‖₊

Tactic:
simpa using nnnorm_smul_le _ _

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_eq_bot' {f : F} : ker f = ⊥ ↔ ∀ m, f m = 0 → m = 0

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
⊢ ker f = ⊥ ↔ ∀ (m : M), f m = 0 → m = 0

Tactic:
simpa [disjoint_iff_inf_le] using disjoint_ker (f := f) (p := ⊤)

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
lemma cons_sub_cons (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
    vecCons x v - vecCons y w = vecCons (x - y) (v - w)

Proof state:
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v - vecCons y w = vecCons (x - y) (v - w)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_add_not (s : Multiset α) : filter p s + filter (fun a => ¬p a) s = s

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ a ∈ s, p a ∨ ¬p a

Tactic:
simp only [Bool.not_eq_true, decide_eq_true_eq, Bool.eq_false_or_eq_true,
  decide_true, implies_true, Decidable.em]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s

Tactic:
simp only [Multiset.add_zero]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ a ∈ s, ¬(p a ∧ ¬p a)

Tactic:
simp [Decidable.em, -Bool.not_eq_true, -not_and, not_and_or, or_comm]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ filter p s + filter (fun a => ¬p a) s = s

Tactic:
rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s

α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ a ∈ s, ¬(p a ∧ ¬p a)

α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ a ∈ s, p a ∨ ¬p a
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsUniversalColimit.whiskerEquivalence {K : Type*} [Category K] (e : J ≌ K)
    {F : K ⥤ C} {c : Cocone F} (hc : IsUniversalColimit c) :
    IsUniversalColimit (c.whisker e.functor)

Proof state:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ Nonempty (IsColimit c')

Tactic:
convert hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
  ((hα.whiskerLeft _).comp (NatTrans.equifibered_of_isIso _)) ?_ using 1

Result:
case a
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))

case convert_1
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ (Functor.const K).map f

case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ ∀ (j : K),
    IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom).app j) f
      (c.ι.app j)
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
@[simp]
lemma lTensor_surjective_iff_surjective [Module.FaithfullyFlat R M] :
    Function.Surjective (f.lTensor M) ↔ Function.Surjective f

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑f ⇑0

Tactic:
conv_rhs => rw [← lTensor_exact_iff_exact R M]

Result:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M 0)

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

Tactic:
rw [← LinearMap.exact_zero_iff_surjective (M ⊗[R] Unit),
  ← LinearMap.exact_zero_iff_surjective Unit]

Result:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑f ⇑0

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M 0)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem idxOf_eq_idxOf? [BEq α] (a : α) (l : List α) :
    l.idxOf a = (match l.idxOf? a with | some i => i | none => l.length)

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ idxOf a l =
    match idxOf? a l with
    | some i => i
    | none => l.length

Tactic:
simp [idxOf, idxOf?, findIdx_eq_findIdx?]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ici_erase [DecidableEq α] (a : α) : (Ici a).erase a = Ioi a

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ (Ici a).erase a = Ioi a

Tactic:
ext

Result:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (Ici a).erase a ↔ a✝ ∈ Ioi a

Proof state:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (Ici a).erase a ↔ a✝ ∈ Ioi a

Tactic:
simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subring R} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subring R) : Set R) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Proof state:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_hom_inv_id' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
    (g ⊗ f) ≫ (h ⊗ inv f) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ f) ≫ (h ⊗ inv f) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Tactic:
rw [← tensor_comp, IsIso.hom_inv_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 V = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 V = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Tactic:
simp [tensorHom_id]

Result:
no goals