harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem IsMultiplicative.prodPrimeFactors_one_add_of_squarefree [CommSemiring R]
    {f : ArithmeticFunction R} (h_mult : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) :
    ∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ (ArithmeticFunction.prodPrimeFactors fun p => (↑ζ + f) p) n = ∑ d ∈ n.divisors, f d

Tactic:
rw [isMultiplicative_zeta.natCast.prodPrimeFactors_add_of_squarefree h_mult hn,
  coe_zeta_mul_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = (ArithmeticFunction.prodPrimeFactors fun p => (↑ζ + f) p) n

Tactic:
simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]

Result:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = ∏ x ∈ n.primeFactors, (↑(ζ x) + f x)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d

Tactic:
trans (∏ᵖ p ∣ n, ((ζ : ArithmeticFunction R) + f) p)

Result:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = (ArithmeticFunction.prodPrimeFactors fun p => (↑ζ + f) p) n

R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ (ArithmeticFunction.prodPrimeFactors fun p => (↑ζ + f) p) n = ∑ d ∈ n.divisors, f d

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors, 1 + f x = ↑(ζ x) + f x

Tactic:
intro p hp

Result:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 + f p = ↑(ζ p) + f p

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = ∏ x ∈ n.primeFactors, (↑(ζ x) + f x)

Tactic:
apply Finset.prod_congr rfl

Result:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∀ x ∈ n.primeFactors, 1 + f x = ↑(ζ x) + f x

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 + f p = ↑(ζ p) + f p

Tactic:
rw [zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero, cast_one]

Result:
no goals
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toMultiset_lt_toMultiset : toMultiset f < toMultiset g ↔ f < g

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f < toMultiset g ↔ f < g

Tactic:
simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem ker_unitGroupToResidueFieldUnits :
    A.unitGroupToResidueFieldUnits.ker = A.principalUnitGroup.comap A.unitGroup.subtype

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ x✝ ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup

Tactic:
rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff]

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ A.unitGroupMulEquiv x✝ ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup

Tactic:
ext

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ x✝ ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : ↥A.unitGroup
⊢ x✝ ∈ A.unitGroupToResidueFieldUnits.ker ↔ A.unitGroupMulEquiv x✝ ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_push (a b : α) (l : Vector α n) :
    count a (l.push b) = count a l + if b == a then 1 else 0

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ count a ({ toArray := l, size_toArray := ⋯ }.push b) =
    count a { toArray := l, size_toArray := ⋯ } + if (b == a) = true then 1 else 0

Tactic:
simp [Array.count_push]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a b : α
l : Vector α n
⊢ count a (l.push b) = count a l + if (b == a) = true then 1 else 0

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ count a ({ toArray := l, size_toArray := ⋯ }.push b) =
    count a { toArray := l, size_toArray := ⋯ } + if (b == a) = true then 1 else 0
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem numeric_def {x : PGame} :
    Numeric x ↔
      (∀ i j, x.moveLeft i < x.moveRight j) ∧
        (∀ i, Numeric (x.moveLeft i)) ∧ ∀ j, Numeric (x.moveRight j)

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝).Numeric ↔
    (∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).RightMoves),
        (mk α✝ β✝ a✝¹ a✝).moveLeft i < (mk α✝ β✝ a✝¹ a✝).moveRight j) ∧
      (∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves), ((mk α✝ β✝ a✝¹ a✝).moveLeft i).Numeric) ∧
        ∀ (j : (mk α✝ β✝ a✝¹ a✝).RightMoves), ((mk α✝ β✝ a✝¹ a✝).moveRight j).Numeric

Tactic:
rfl

Result:
no goals

Proof state:
x : PGame
⊢ x.Numeric ↔
    (∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j) ∧
      (∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) ∧ ∀ (j : x.RightMoves), (x.moveRight j).Numeric

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝).Numeric ↔
    (∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).RightMoves),
        (mk α✝ β✝ a✝¹ a✝).moveLeft i < (mk α✝ β✝ a✝¹ a✝).moveRight j) ∧
      (∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves), ((mk α✝ β✝ a✝¹ a✝).moveLeft i).Numeric) ∧
        ∀ (j : (mk α✝ β✝ a✝¹ a✝).RightMoves), ((mk α✝ β✝ a✝¹ a✝).moveRight j).Numeric
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofMkLE_comp_ofLEMk {B A₁ A₂ : C} (f : A₁ ⟶ B) [Mono f] (X : Subobject B) (g : A₂ ⟶ B)
    [Mono g] (h₁ : mk f ≤ X) (h₂ : X ≤ mk g) :
    ofMkLE f X h₁ ≫ ofLEMk X g h₂ = ofMkLEMk f g (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
X : Subobject B
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : mk f ≤ X
h₂ : X ≤ mk g
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso g).hom =
    (underlyingIso f).inv ≫ underlying.map ⋯.hom ≫ (underlyingIso g).hom

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
X : Subobject B
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : mk f ≤ X
h₂ : X ≤ mk g
⊢ ofMkLE f X h₁ ≫ X.ofLEMk g h₂ = ofMkLEMk f g ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
X : Subobject B
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : mk f ≤ X
h₂ : X ≤ mk g
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso g).hom =
    (underlyingIso f).inv ≫ underlying.map ⋯.hom ≫ (underlyingIso g).hom
-- Mathlib/CategoryTheory/WithTerminal.lean
theorem lift_map_liftStar {D : Type*} [Category D] {Z : D} (F : C ⥤ D) (M : ∀ x : C, F.obj x ⟶ Z)
    (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (x : C) :
    (lift F M hM).map (starTerminal.from (incl.obj x)) ≫ (liftStar F M hM).hom =
      (inclLift F M hM).hom.app x ≫ M x

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (starTerminal.from (incl.obj x)) = M x

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (starTerminal.from (incl.obj x)) ≫ (liftStar F M hM).hom = (inclLift F M hM).hom.app x ≫ M x

Tactic:
erw [Category.id_comp, Category.comp_id]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (starTerminal.from (incl.obj x)) = M x
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean
@[simp] lemma flip_mul : (ContinuousLinearMap.mul 𝕜 R).flip = .mul 𝕜 R

Proof state:
case h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
R : Type u_3
inst✝³ : NonUnitalSeminormedCommRing R
inst✝² : NormedSpace 𝕜 R
inst✝¹ : IsScalarTower 𝕜 R R
inst✝ : SMulCommClass 𝕜 R R
x✝¹ x✝ : R
⊢ ((mul 𝕜 R).flip x✝¹) x✝ = ((mul 𝕜 R) x✝¹) x✝

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
R : Type u_3
inst✝³ : NonUnitalSeminormedCommRing R
inst✝² : NormedSpace 𝕜 R
inst✝¹ : IsScalarTower 𝕜 R R
inst✝ : SMulCommClass 𝕜 R R
⊢ (mul 𝕜 R).flip = mul 𝕜 R

Tactic:
ext

Result:
case h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
R : Type u_3
inst✝³ : NonUnitalSeminormedCommRing R
inst✝² : NormedSpace 𝕜 R
inst✝¹ : IsScalarTower 𝕜 R R
inst✝ : SMulCommClass 𝕜 R R
x✝¹ x✝ : R
⊢ ((mul 𝕜 R).flip x✝¹) x✝ = ((mul 𝕜 R) x✝¹) x✝
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma ceilRoot_one_left (a : ℕ) : ceilRoot 1 a = a

Proof state:
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k => p ^ k) = a

Tactic:
split_ifs <;> simp [*]

Result:
no goals

Proof state:
a : ℕ
⊢ ceilRoot 1 a = a

Tactic:
simp [ceilRoot]

Result:
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k => p ^ k) = a
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem sup'_eq_csSup_image (s : Finset ι) (H : s.Nonempty) (f : ι → α) :
    s.sup' H f = sSup (f '' s) :=
  eq_of_forall_ge_iff fun a => by
    simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f ≤ a ↔ sSup (f '' ↑s) ≤ a

Tactic:
simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_smul_left (hc : c ≠ 0) (s : Set E) (x : E) :
    egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ c ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ₑ ≠ 0 ∨ egauge 𝕜 s x ≠ 0

Tactic:
simp [*]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c⁻¹ • c • s) x = egauge 𝕜 s x

Tactic:
rw [inv_smul_smul₀ hc]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ

Tactic:
rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ

Tactic:
refine le_antisymm ?_ (le_egauge_smul_left _ _ _)

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ egauge 𝕜 s x

Tactic:
calc
  egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by
    rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
  _ ≤ egauge 𝕜 (c⁻¹ • c • s) x := le_egauge_smul_left _ _ _
  _ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ ‖c‖ₑ ≠ ⊤ ∨ egauge 𝕜 s x ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x ≤ egauge 𝕜 s x / ‖c‖ₑ

Tactic:
rw [ENNReal.le_div_iff_mul_le (by simp [*]) (by simp)]

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x * ‖c‖ₑ ≤ egauge 𝕜 s x
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_toDeleteEdges_eq (s : Set (Sym2 V)) {p : G.Walk v w} (hp) :
    Walk.map (Hom.mapSpanningSubgraphs (G.deleteEdges_le s)) (p.toDeleteEdges s hp) = p

Proof state:
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ Walk.map (Hom.mapSpanningSubgraphs ⋯) (toDeleteEdges s p hp) = p

Tactic:
rw [← transfer_eq_map_of_le, transfer_transfer, transfer_self]

Result:
case hp'
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (p.transfer (G.deleteEdges s) ⋯).edges, e ∈ G.edgeSet

Proof state:
case hp'
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (p.transfer (G.deleteEdges s) ⋯).edges, e ∈ G.edgeSet

Tactic:
intros e

Result:
case hp'
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
e : Sym2 V
⊢ e ∈ (p.transfer (G.deleteEdges s) ⋯).edges → e ∈ G.edgeSet

Proof state:
case hp'
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
e : Sym2 V
⊢ e ∈ (p.transfer (G.deleteEdges s) ⋯).edges → e ∈ G.edgeSet

Tactic:
rw [edges_transfer]

Result:
case hp'
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
e : Sym2 V
⊢ e ∈ p.edges → e ∈ G.edgeSet

Proof state:
case hp'
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
e : Sym2 V
⊢ e ∈ p.edges → e ∈ G.edgeSet

Tactic:
apply edges_subset_edgeSet p

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhds_top_basis [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α]
    [Nontrivial α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) fun a : α => Ioi a

Proof state:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTop α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
this : ∃ x, x < ⊤
⊢ (𝓝 ⊤).HasBasis (fun a => a < ⊤) fun a => Ioi a

Tactic:
simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsLE_basis_of_exists_lt this

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTop α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
⊢ (𝓝 ⊤).HasBasis (fun a => a < ⊤) fun a => Ioi a

Tactic:
have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top

Result:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTop α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
this : ∃ x, x < ⊤
⊢ (𝓝 ⊤).HasBasis (fun a => a < ⊤) fun a => Ioi a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_append {K L : List α} {f : (i : Nat) → α → (h : i < (K ++ L).length) → β} :
    (K ++ L).mapFinIdx f =
      K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
        L.mapFinIdx (fun i a h => f (i + K.length) a (by simp; omega))

Proof state:
case h.isFalse
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
h✝ : ¬i < K.length
h : K.length ≤ i
⊢ f i (K ++ L)[i] ⋯ = f (i - K.length + K.length) L[i - K.length] ⋯

Tactic:
rw [getElem_append_right h]

Result:
case h.isFalse
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
h✝ : ¬i < K.length
h : K.length ≤ i
⊢ f i L[i - K.length] ⋯ = f (i - K.length + K.length) L[i - K.length] ⋯

Proof state:
case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
⊢ ∀ (i : Nat) (h₁ : i < ((K ++ L).mapFinIdx f).length)
    (h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length),
    ((K ++ L).mapFinIdx f)[i] = ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯)[i]

Tactic:
intro i h₁ h₂

Result:
case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
⊢ ((K ++ L).mapFinIdx f)[i] = ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯)[i]
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma even_finrank_of_not_isUnramifiedIn
    [IsGalois k K] {w : InfinitePlace k} (hw : ¬ w.IsUnramifiedIn K) :
    Even (finrank k K)

Proof state:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (finrank k K)

Tactic:
exact even_finrank_of_not_isUnramified hw

Result:
no goals

Proof state:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x => x.comap (algebraMap k K)) v)
⊢ Even (finrank k K)

Tactic:
rw [isUnramifiedIn_comap] at hw

Result:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (finrank k K)

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace k
hw : ¬IsUnramifiedIn K w
⊢ Even (finrank k K)

Tactic:
obtain ⟨v, rfl⟩ := comap_surjective (K := K) w

Result:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
v : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x => x.comap (algebraMap k K)) v)
⊢ Even (finrank k K)
-- Mathlib/Algebra/Module/Injective.lean
lemma Module.injective_of_ulift_injective
    (inj : Module.Injective R (ULift.{v'} M)) :
    Module.Injective R M where
  out X Y _ _ _ _ f hf g :=
    let eX := ULift.moduleEquiv.{_,_,v'} (R := R) (M := X)
    have ⟨g', hg'⟩ := inj.out (ULift.moduleEquiv.{_,_,v'}.symm.toLinearMap ∘ₗ f ∘ₗ eX.toLinearMap)
      (by exact ULift.moduleEquiv.symm.injective.comp <| hf.comp eX.injective)
      (ULift.moduleEquiv.symm.toLinearMap ∘ₗ g ∘ₗ eX.toLinearMap)
    ⟨ULift.moduleEquiv.toLinearMap ∘ₗ g' ∘ₗ ULift.moduleEquiv.symm.toLinearMap,
      fun x ↦ by exact congr(ULift.down $(hg' ⟨x⟩))⟩

Proof state:
R : Type u
inst✝² : Ring R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
⊢ Function.Injective ⇑(↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑eX)

Tactic:
exact ULift.moduleEquiv.symm.injective.comp <| hf.comp eX.injective

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
g' : ULift.{v', v} Y →ₗ[R] ULift.{v', v} M
hg' : ∀ (x : ULift.{v', v} X), g' ((↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑eX) x) = (↑ULift.moduleEquiv.symm ∘ₗ g ∘ₗ ↑eX) x
x : X
⊢ (↑ULift.moduleEquiv ∘ₗ g' ∘ₗ ↑ULift.moduleEquiv.symm) (f x) = g x

Tactic:
exact congr(ULift.down $(hg' ⟨x⟩))

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem orElse_eq_none (o o' : Option α) : (o <|> o') = none ↔ o = none ∧ o' = none

Proof state:
α : Type u_1
o o' : Option α
⊢ (o <|> o') = none ↔ o = none ∧ o' = none

Tactic:
cases o

Result:
case none
α : Type u_1
o' : Option α
⊢ (none <|> o') = none ↔ none = none ∧ o' = none

case some
α : Type u_1
o' : Option α
val✝ : α
⊢ (some val✝ <|> o') = none ↔ some val✝ = none ∧ o' = none

Proof state:
case some
α : Type u_1
o' : Option α
val✝ : α
⊢ (some val✝ <|> o') = none ↔ some val✝ = none ∧ o' = none

Tactic:
simp only [some_orElse, reduceCtorEq, false_and]

Result:
no goals

Proof state:
case none
α : Type u_1
o' : Option α
⊢ (none <|> o') = none ↔ none = none ∧ o' = none

Tactic:
simp only [true_and, none_orElse, eq_self_iff_true]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_subset_iff_left : image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun b => f a b) '' t ⊆ u

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun b => f a b) '' t ⊆ u

Tactic:
simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]

Result:
no goals