harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
theorem toSplittingField_coeff {s : Finset (Monics k)} {f} (h : f ∈ s) (n) :
    toSplittingField s ((subProdXSubC f).coeff n) = 0

Proof state:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f -
          (Multiset.map (fun x => X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Tactic:
conv in map _ _ => rw [eq_prod_roots_of_splits (Monics.splits_finsetProd h)]

Result:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (C ((algebraMap k (∏ f ∈ s, ↑f).SplittingField) (↑f).leadingCoeff) *
            (Multiset.map (fun a => X - C a) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod -
          (Multiset.map (fun x => X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Proof state:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (C ((algebraMap k (∏ f ∈ s, ↑f).SplittingField) (↑f).leadingCoeff) *
            (Multiset.map (fun a => X - C a) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod -
          (Multiset.map (fun x => X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Tactic:
rw [f.2, map_one, C_1, one_mul, sub_self, coeff_zero]

Result:
no goals

Proof state:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (toSplittingField s) ((subProdXSubC f).coeff n) = 0

Tactic:
simp_rw [← AlgHom.coe_toRingHom, ← coeff_map, subProdXSubC, Polynomial.map_sub,
  Polynomial.map_prod, Polynomial.map_sub, map_X, map_C, toSplittingField,
  AlgHom.coe_toRingHom, MvPolynomial.aeval_X, dif_pos h,
  ← (finEquivRoots (Monics.splits_finsetProd h)).symm.prod_comp, Equiv.apply_symm_apply]

Result:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(MvPolynomial.aeval fun fi => if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37))
            (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ x : { x // x ∈ (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots.toEnumFinset },
            (X - C (↑x).1)).coeff
      n =
    0
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_eq_empty_iff [DenselyOrdered α] : Ioo a b = ∅ ↔ ¬a < b

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b

Tactic:
rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]

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

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

Tactic:
simp [Filter.Frequently]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem getElem_eraseIdx_of_lt (l : Array α) (i : Nat) (w : i < l.size) (j : Nat) (h : j < (l.eraseIdx i).size) (h' : j < i) :
    (l.eraseIdx i)[j] = l[j]

Proof state:
case mk
α : Type u_1
i j : Nat
h' : j < i
l : List α
w : i < { toList := l }.size
h : j < ({ toList := l }.eraseIdx i w).size
⊢ ({ toList := l }.eraseIdx i w)[j] = { toList := l }[j]

Tactic:
simp [List.getElem_eraseIdx_of_lt, *]

Result:
no goals

Proof state:
α : Type u_1
l : Array α
i : Nat
w : i < l.size
j : Nat
h : j < (l.eraseIdx i w).size
h' : j < i
⊢ (l.eraseIdx i w)[j] = l[j]

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i j : Nat
h' : j < i
l : List α
w : i < { toList := l }.size
h : j < ({ toList := l }.eraseIdx i w).size
⊢ ({ toList := l }.eraseIdx i w)[j] = { toList := l }[j]
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftProp_id (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
    LiftProp Q (id : M → M)

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
⊢ ∀ (x : M), Q (↑(chartAt H (id x)) ∘ id ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
exact fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
⊢ LiftProp Q id

Tactic:
simp_rw [liftProp_iff, continuous_id, true_and]

Result:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
⊢ ∀ (x : M), Q (↑(chartAt H (id x)) ∘ id ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)
-- Mathlib/Algebra/Group/Center.lean
@[to_additive subset_addCentralizer_addCentralizer]
lemma subset_centralizer_centralizer : S ⊆ S.centralizer.centralizer

Proof state:
M : Type u_1
S : Set M
inst✝ : Mul M
x : M
hx : x ∈ S
⊢ ∀ (m : M), (∀ m_1 ∈ S, m_1 * m = m * m_1) → m * x = x * m

Tactic:
exact fun y hy => (hy x hx).symm

Result:
no goals

Proof state:
M : Type u_1
S : Set M
inst✝ : Mul M
⊢ S ⊆ S.centralizer.centralizer

Tactic:
intro x hx

Result:
M : Type u_1
S : Set M
inst✝ : Mul M
x : M
hx : x ∈ S
⊢ x ∈ S.centralizer.centralizer

Proof state:
M : Type u_1
S : Set M
inst✝ : Mul M
x : M
hx : x ∈ S
⊢ x ∈ S.centralizer.centralizer

Tactic:
simp only [Set.mem_centralizer_iff]

Result:
M : Type u_1
S : Set M
inst✝ : Mul M
x : M
hx : x ∈ S
⊢ ∀ (m : M), (∀ m_1 ∈ S, m_1 * m = m * m_1) → m * x = x * m
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_zero : (0 : MvPowerSeries σ R).weightedOrder w = ⊤

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
⊢ weightedOrder w 0 = ⊤

Tactic:
rw [weightedOrder, dif_pos rfl]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_iff {U : Set E} :
    U ∈ p.basisSets ↔ ∃ (i : Finset ι) (r : ℝ), 0 < r ∧ U = ball (i.sup p) 0 r

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
⊢ U ∈ p.basisSets ↔ ∃ i r, 0 < r ∧ U = (i.sup p).ball 0 r

Tactic:
simp only [basisSets, mem_iUnion, exists_prop, mem_singleton_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem mem_L1_toReal_of_lintegral_ne_top {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ)
    (hfi : ∫⁻ x, f x ∂μ ≠ ∞) : MemLp (fun x ↦ (f x).toReal) 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ MemLp (fun x => (f x).toReal) 1 μ

Tactic:
rw [MemLp, eLpNorm_one_eq_lintegral_enorm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ AEStronglyMeasurable (fun x => (f x).toReal) μ ∧ ∫⁻ (x : α), ‖(f x).toReal‖ₑ ∂μ < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ AEStronglyMeasurable (fun x => (f x).toReal) μ ∧ ∫⁻ (x : α), ‖(f x).toReal‖ₑ ∂μ < ⊤

Tactic:
exact ⟨(AEMeasurable.ennreal_toReal hfm).aestronglyMeasurable,
  hasFiniteIntegral_toReal_of_lintegral_ne_top hfi⟩

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma posFittingComp_le_iInf_lowerCentralSeries :
    posFittingComp R L M ≤ ⨅ k, lowerCentralSeries R L M k

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
⊢ posFittingComp R L M ≤ ⨅ k, lowerCentralSeries R L M k

Tactic:
simp [posFittingComp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem _root_.Polynomial.toLaurent_X_pow (n : ℕ) : toLaurent (X ^ n : R[X]) = T n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ toLaurent (X ^ n) = T ↑n

Tactic:
simp only [map_pow, Polynomial.toLaurent_X, T_pow, mul_one]

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem Finset.univ_map_embedding {α : Type*} [Fintype α] (e : α ↪ α) : univ.map e = univ

Proof state:
α : Type u_4
inst✝ : Fintype α
e : α ↪ α
⊢ map e univ = univ

Tactic:
rw [← e.toEmbedding_equivOfFiniteSelfEmbedding, univ_map_equiv_to_embedding]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem fundamentalDomain_integerLattice :
    MeasureTheory.IsAddFundamentalDomain (mixedEmbedding.integerLattice K)
      (ZSpan.fundamentalDomain (latticeBasis K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑(latticeBasis K))))
    (ZSpan.fundamentalDomain (latticeBasis K)) MeasureTheory.volume

Tactic:
exact ZSpan.isAddFundamentalDomain (latticeBasis K) _

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasureTheory.IsAddFundamentalDomain (↥(mixedEmbedding.integerLattice K)) (ZSpan.fundamentalDomain (latticeBasis K))
    MeasureTheory.volume

Tactic:
rw [← span_latticeBasis]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑(latticeBasis K))))
    (ZSpan.fundamentalDomain (latticeBasis K)) MeasureTheory.volume
-- Mathlib/Data/Finset/Insert.lean
theorem singleton_subset_set_iff {s : Set α} {a : α} : ↑({a} : Finset α) ⊆ s ↔ a ∈ s

Proof state:
α : Type u_1
s : Set α
a : α
⊢ ↑{a} ⊆ s ↔ a ∈ s

Tactic:
rw [coe_singleton, Set.singleton_subset_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_insert [inst : @OrientedCmp α cmp] {t : RBNode α} :
    (insert cmp t x).reverse = insert (flip cmp) t.reverse x

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
inst : OrientedCmp cmp
t : RBNode α
⊢ (insert cmp t x).reverse = insert (flip cmp) t.reverse x

Tactic:
simp [insert] <;> split <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_add_two {n : ℕ} : fib (n + 2) = fib n + fib (n + 1)

Proof state:
n : ℕ
⊢ fib (n + 2) = fib n + fib (n + 1)

Tactic:
simp [fib, Function.iterate_succ_apply']

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem prime_five : Prime 5

Proof state:
⊢ Prime 5

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_inv_naturality_right (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
    X ◁ Y ◁ f ≫ (α_ X Y Z').inv = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ X ◁ Y ◁ f ≫ (α_ X Y Z').inv = (α_ X Y Z).inv ≫ (X ⊗ Y) ◁ f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
@[simp]
lemma count_attach (a : {x // x ∈ s}) : s.attach.count a = s.count ↑a :=
  Eq.trans (countP_congr rfl fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ s.attach
⊢ (a = x✝¹) = (↑a = ↑x✝¹)

Tactic:
simp [Subtype.ext_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem zero_divByMonic (p : R[X]) : 0 /ₘ p = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).1
    else 0) =
    0

Tactic:
by_cases hp : Monic p

Result:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).1
    else 0) =
    0

case neg
R : Type u
inst✝ : Ring R
p : R[X]
hp : ¬p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).1
    else 0) =
    0

Proof state:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
hp : ¬p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).1
    else 0) =
    0

Tactic:
rw [dif_neg hp]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ 0 /ₘ p = 0

Tactic:
unfold divByMonic divModByMonicAux

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if h_1 : p.degree ≤ degree 0 ∧ 0 ≠ 0 then
          let z := C (leadingCoeff 0) * X ^ (natDegree 0 - p.natDegree);
          let_fun _wf := ⋯;
          let dm := (0 - p * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, 0)).1
    else 0) =
    0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if h_1 : p.degree ≤ degree 0 ∧ 0 ≠ 0 then
          let z := C (leadingCoeff 0) * X ^ (natDegree 0 - p.natDegree);
          let_fun _wf := ⋯;
          let dm := (0 - p * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, 0)).1
    else 0) =
    0

Tactic:
dsimp

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).1
    else 0) =
    0

Proof state:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).1
    else 0) =
    0

Tactic:
rw [dif_pos hp, if_neg (mt And.right (not_not_intro rfl)), Prod.fst_zero]

Result:
no goals
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma implicitDeriv_C (v : A[X]) (b : A) :
    implicitDeriv v (C b) = C b′

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
v : A[X]
b : A
⊢ (implicitDeriv v) (C b) = C b′

Tactic:
simp [implicitDeriv]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
lemma norm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖ = n • ‖x‖

Proof state:
K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖ = n • ‖x‖

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using norm_smul (n : K) x

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- A subset `s` is σ-compact iff `s` (with the subspace topology) is a σ-compact space. -/
lemma isSigmaCompact_iff_isSigmaCompact_univ {s : Set X} :
    IsSigmaCompact s ↔ IsSigmaCompact (univ : Set s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ IsSigmaCompact univ

Tactic:
rw [Subtype.isSigmaCompact_iff, image_univ, Subtype.range_coe]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma extendMap_f_eq_zero (i' : ι') (hi' : ∀ i, e.f i ≠ i') :
    (extendMap φ e).f i' = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ (extendMap φ e).f i' = 0

Tactic:
dsimp [extendMap]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ extend.mapX φ (e.r i') = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ extend.mapX φ (e.r i') = 0

Tactic:
rw [extend.mapX_none φ (e.r_eq_none i' hi')]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_boole {α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
    (a * if P then 1 else 0) = if P then a else 0

Proof state:
α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (a * if P then 1 else 0) = if P then a else 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
    foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n)

Proof state:
case zero
α : Sort u_1
f : α → Fin (0 + 1) → α
x : α
⊢ foldl 0 (fun x i => f x i.succ) (f x 0) = f (foldl 0 (fun x1 x2 => f x1 x2.castSucc) x) (last 0)

Tactic:
simp [foldl_succ, Fin.last]

Result:
no goals

Proof state:
case succ
α : Sort u_1
n : Nat
ih :
  ∀ (f : α → Fin (n + 1) → α) (x : α),
    foldl n (fun x i => f x i.succ) (f x 0) = f (foldl n (fun x1 x2 => f x1 x2.castSucc) x) (last n)
f : α → Fin (n + 1 + 1) → α
x : α
⊢ f (foldl n (fun x1 x2 => f x1 x2.castSucc.succ) (f x 0)) (last n).succ =
    f (foldl n (fun x i => f x i.succ.castSucc) (f x (castSucc 0))) (last (n + 1))

Tactic:
simp [succ_castSucc]

Result:
no goals

Proof state:
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
⊢ foldl (n + 1) f x = f (foldl n (fun x1 x2 => f x1 x2.castSucc) x) (last n)

Tactic:
rw [foldl_succ]

Result:
α : Sort u_1
n : Nat
f : α → Fin (n + 1) → α
x : α
⊢ foldl n (fun x i => f x i.succ) (f x 0) = f (foldl n (fun x1 x2 => f x1 x2.castSucc) x) (last n)
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma coeSubgraph_restrict_eq {H : G.Subgraph} (H' : G.Subgraph) :
    Subgraph.coeSubgraph (H.restrict H') = H ⊓ H'

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (∃ (_ : x✝¹ ∈ H.verts) (_ : x✝ ∈ H.verts), H.Adj x✝¹ x✝ ∧ H'.Adj x✝¹ x✝) ↔ (H ⊓ H').Adj x✝¹ x✝

Tactic:
simp only [exists_and_left, exists_prop, inf_adj, and_congr_right_iff]

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ → (x✝ ∈ H.verts ∧ x✝¹ ∈ H.verts ∧ H'.Adj x✝¹ x✝ ↔ H'.Adj x✝¹ x✝)

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ → (x✝ ∈ H.verts ∧ x✝¹ ∈ H.verts ∧ H'.Adj x✝¹ x✝ ↔ H'.Adj x✝¹ x✝)

Tactic:
intro h

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
h : H.Adj x✝¹ x✝
⊢ x✝ ∈ H.verts ∧ x✝¹ ∈ H.verts ∧ H'.Adj x✝¹ x✝ ↔ H'.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
h : H.Adj x✝¹ x✝
⊢ x✝ ∈ H.verts ∧ x✝¹ ∈ H.verts ∧ H'.Adj x✝¹ x✝ ↔ H'.Adj x✝¹ x✝

Tactic:
simp [H.edge_vert h, H.edge_vert h.symm]

Result:
no goals

Proof state:
case verts.h
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.coeSubgraph (Subgraph.restrict H')).verts ↔ x✝ ∈ (H ⊓ H').verts

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Subgraph.coeSubgraph (Subgraph.restrict H') = H ⊓ H'

Tactic:
ext

Result:
case verts.h
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.coeSubgraph (Subgraph.restrict H')).verts ↔ x✝ ∈ (H ⊓ H').verts

case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.coeSubgraph (Subgraph.restrict H')).Adj x✝¹ x✝ ↔ (H ⊓ H').Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.coeSubgraph (Subgraph.restrict H')).Adj x✝¹ x✝ ↔ (H ⊓ H').Adj x✝¹ x✝

Tactic:
simp_rw [coeSubgraph_adj, restrict_adj]

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (∃ (_ : x✝¹ ∈ H.verts) (_ : x✝ ∈ H.verts), H.Adj x✝¹ x✝ ∧ H'.Adj x✝¹ x✝) ↔ (H ⊓ H').Adj x✝¹ x✝
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_right_Ioc (a b c : α) : (Ioc a b).image (· + c) = Ioc (a + c) (b + c)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
rw [← map_add_right_Ioc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Algebra/Free.lean
theorem lift_of_mul (x y) : lift f (of x * y) = f x * lift f y

Proof state:
α : Type u
β : Type v
inst✝ : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ (lift f) (of x * y) = f x * (lift f) y

Tactic:
rw [map_mul, lift_of]

Result:
no goals
-- Mathlib/Data/Nat/Set.lean
theorem range_succ : range succ = { i | 0 < i }

Proof state:
⊢ range succ = {i | 0 < i}

Tactic:
ext (_ | i) <;> simp [succ_pos, succ_ne_zero, Set.mem_setOf]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Corner/Defs.lean
@[simp] lemma Set.Subsingleton.isCornerFree (hA : A.Subsingleton) : IsCornerFree A :=
  fun _x₁ _y₁ _x₂ _y₂ hxyd ↦ by simpa using hA hxyd.fst_fst_mem hxyd.snd_fst_mem

Proof state:
G : Type u_1
inst✝ : AddCommMonoid G
A : Set (G × G)
hA : A.Subsingleton
_x₁ _y₁ _x₂ _y₂ : G
hxyd : IsCorner A _x₁ _y₁ _x₂ _y₂
⊢ _x₁ = _x₂

Tactic:
simpa using hA hxyd.fst_fst_mem hxyd.snd_fst_mem

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem memberSubfamily_memberSubfamily : (𝒜.memberSubfamily a).memberSubfamily a = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (memberSubfamily a 𝒜) = ∅

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ ∅

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sOppSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) :
    s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rw [or_iff_right hx]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rw [SOppSide, and_comm, wOppSide_iff_exists_left h, and_assoc, and_congr_right_iff]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))

Tactic:
intro hx

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)