harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem ne_zero (h : v₁.IsEquiv v₂) {r : R} : v₁ r ≠ 0 ↔ v₂ r ≠ 0

Proof state:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
⊢ v₁ r ≠ 0 ↔ v₂ r ≠ 0

Tactic:
have : v₁ r ≠ v₁ 0 ↔ v₂ r ≠ v₂ 0 := not_congr h.val_eq

Result:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
this : v₁ r ≠ v₁ 0 ↔ v₂ r ≠ v₂ 0
⊢ v₁ r ≠ 0 ↔ v₂ r ≠ 0

Proof state:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
this : v₁ r ≠ v₁ 0 ↔ v₂ r ≠ v₂ 0
⊢ v₁ r ≠ 0 ↔ v₂ r ≠ 0

Tactic:
rwa [v₁.map_zero, v₂.map_zero] at this

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem IsLowerSet.image (hs : IsLowerSet s) (f : α ≃o β) : IsLowerSet (f '' s : Set β)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsLowerSet s
f : α ≃o β
⊢ IsLowerSet (⇑↑f '' s)

Tactic:
rw [Set.image_equiv_eq_preimage_symm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsLowerSet s
f : α ≃o β
⊢ IsLowerSet (⇑(↑f).symm ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsLowerSet s
f : α ≃o β
⊢ IsLowerSet (⇑f '' s)

Tactic:
change IsLowerSet ((f : α ≃ β) '' s)

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsLowerSet s
f : α ≃o β
⊢ IsLowerSet (⇑↑f '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsLowerSet s
f : α ≃o β
⊢ IsLowerSet (⇑(↑f).symm ⁻¹' s)

Tactic:
exact hs.preimage f.symm.monotone

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem fold_bind {ι : Type*} (s : Multiset ι) (t : ι → Multiset α) (b : ι → α) (b₀ : α) :
    (s.bind t).fold op ((s.map b).fold op b₀) =
    (s.map fun i => (t i).fold op (b i)).fold op b₀

Proof state:
case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i => fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha))

Tactic:
rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]

Result:
no goals

Proof state:
case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)

Tactic:
rw [zero_bind, map_zero, map_zero, fold_zero]

Result:
no goals

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun i => fold op (b i) (t i)) s)

Tactic:
induction' s using Multiset.induction_on with a ha ih

Result:
case empty
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)

case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i => fold op (b i) (t i)) ha)
⊢ fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) =
    fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha))
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
/-- A version of `Complex.cpow_int_mul` with RHS that matches `Complex.cpow_mul`.

The assumptions on the arguments are needed
because the equality fails, e.g., for `x = -I`, `n = 2`, `y = 1/2`. -/
lemma cpow_int_mul' {x : ℂ} {n : ℤ} (hlt : -π < n * x.arg) (hle : n * x.arg ≤ π) (y : ℂ) :
    x ^ (n * y) = (x ^ n) ^ y

Proof state:
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y

Tactic:
rw [cpow_mul, cpow_intCast] <;> simpa [log_im]

Result:
no goals

Proof state:
x : ℂ
n : ℤ
hlt : -π < ↑n * x.arg
hle : ↑n * x.arg ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y

Tactic:
rw [mul_comm] at hlt hle

Result:
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y
-- Mathlib/Data/DFinsupp/Order.lean
theorem support_sup : (f ⊔ g).support = f.support ∪ g.support

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support

Tactic:
simp only [Finset.mem_union, mem_support_iff, sup_apply, Ne, ← bot_eq_zero]

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬f a✝ ⊔ g a✝ = ⊥ ↔ ¬f a✝ = ⊥ ∨ ¬g a✝ = ⊥

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬f a✝ ⊔ g a✝ = ⊥ ↔ ¬f a✝ = ⊥ ∨ ¬g a✝ = ⊥

Tactic:
rw [_root_.sup_eq_bot_iff, not_and_or]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp]
lemma leftHomologyMap'_op
    (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
let γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
simp only [γ.leftHomologyMap'_eq, γ.op.rightHomologyMap'_eq,
  LeftHomologyMapData.op_φH]

Result:
no goals
-- Mathlib/Analysis/Fourier/ZMod.lean
private lemma auxDFT_smul (c : ℂ) (Φ : ZMod N → E) :
    auxDFT (c • Φ) = c • auxDFT Φ

Proof state:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ ZMod.auxDFT (c • Φ) x✝ = (c • ZMod.auxDFT Φ) x✝

Tactic:
simp only [Pi.smul_def, auxDFT, smul_sum, smul_comm c]

Result:
no goals

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
⊢ ZMod.auxDFT (c • Φ) = c • ZMod.auxDFT Φ

Tactic:
ext

Result:
case h
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ ZMod.auxDFT (c • Φ) x✝ = (c • ZMod.auxDFT Φ) x✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem intCast_mul (a b : Int) :
    ((a * b : Int) : Rat) = (a : Rat) * (b : Rat)

Proof state:
a b : Int
⊢ ↑(a * b) = ↑a * ↑b

Tactic:
rw [mul_def]

Result:
a b : Int
⊢ ↑(a * b) = normalize ((↑a).num * (↑b).num) ((↑a).den * (↑b).den) ⋯

Proof state:
a b : Int
⊢ ↑(a * b) = normalize ((↑a).num * (↑b).num) ((↑a).den * (↑b).den) ⋯

Tactic:
simp [normalize_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vsub_left_mem_direction_iff_mem {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) :
    p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub_left hp]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ (∃ p₂_1 ∈ s, p -ᵥ p₂ = p -ᵥ p₂_1) ↔ p₂ ∈ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ (∃ p₂_1 ∈ s, p -ᵥ p₂ = p -ᵥ p₂_1) ↔ p₂ ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem IsEulerian.card_odd_degree [Fintype V] [DecidableRel G.Adj] {u v : V} {p : G.Walk u v}
    (ht : p.IsEulerian) : Fintype.card { v : V | Odd (G.degree v) } = 0 ∨
      Fintype.card { v : V | Odd (G.degree v) } = 2

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ {v | Odd (G.degree v)}.toFinset = Finset.filter (fun v => Odd (G.degree v)) Finset.univ

Tactic:
ext v

Result:
case h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v✝ : V
p : G.Walk u v✝
ht : p.IsEulerian
v : V
⊢ v ∈ {v | Odd (G.degree v)}.toFinset ↔ v ∈ Finset.filter (fun v => Odd (G.degree v)) Finset.univ

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ {v | Odd (G.degree v)}.toFinset.card = 0 ∨ {v | Odd (G.degree v)}.toFinset.card = 2

Tactic:
apply IsEulerian.card_filter_odd_degree ht

Result:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ {v | Odd (G.degree v)}.toFinset = Finset.filter (fun v => Odd (G.degree v)) Finset.univ

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Fintype.card ↑{v | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v | Odd (G.degree v)} = 2

Tactic:
rw [← Set.toFinset_card]

Result:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ {v | Odd (G.degree v)}.toFinset.card = 0 ∨ {v | Odd (G.degree v)}.toFinset.card = 2

Proof state:
case h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v✝ : V
p : G.Walk u v✝
ht : p.IsEulerian
v : V
⊢ v ∈ {v | Odd (G.degree v)}.toFinset ↔ v ∈ Finset.filter (fun v => Odd (G.degree v)) Finset.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebraFin_succ_le : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1

Proof state:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ ¬n.succ = 0

Tactic:
exact Nat.succ_ne_zero _

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) m‖ ≤ 1 * ∏ i : Fin n.succ, ‖m i‖

Tactic:
simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
  Fin.prod_univ_def, Multiset.map_coe, Multiset.prod_coe]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ ‖(List.map m (List.finRange n.succ)).prod‖ ≤ (List.map (fun i => ‖m i‖) (List.finRange n.succ)).prod

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ ‖(List.map m (List.finRange n.succ)).prod‖ ≤ (List.map (fun i => ‖m i‖) (List.finRange n.succ)).prod

Tactic:
refine (List.norm_prod_le' ?_).trans_eq ?_

Result:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ List.map m (List.finRange n.succ) ≠ []

case refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ (List.map norm (List.map m (List.finRange n.succ))).prod = (List.map (fun i => ‖m i‖) (List.finRange n.succ)).prod

Proof state:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ List.map m (List.finRange n.succ) ≠ []

Tactic:
rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil]

Result:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ ¬n.succ = 0

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1

Tactic:
refine opNorm_le_bound zero_le_one fun m => ?_

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) m‖ ≤ 1 * ∏ i : Fin n.succ, ‖m i‖

Proof state:
case refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
m : Fin n.succ → A
⊢ (List.map norm (List.map m (List.finRange n.succ))).prod = (List.map (fun i => ‖m i‖) (List.finRange n.succ)).prod

Tactic:
rw [List.map_map, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropInfix?_nil [BEq α] {s : List α} : dropInfix? s [] = some ([], s)

Proof state:
α : Type u_1
inst✝ : BEq α
s : List α
⊢ s.dropInfix? [] = some ([], s)

Tactic:
simp [dropInfix?_eq_some_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem neighborSet_compl (G : SimpleGraph V) (v : V) :
    Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}

Tactic:
ext w

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∈ Gᶜ.neighborSet v ↔ w ∈ (G.neighborSet v)ᶜ \ {v}

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∈ Gᶜ.neighborSet v ↔ w ∈ (G.neighborSet v)ᶜ \ {v}

Tactic:
simp [and_comm, eq_comm]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem rel_zero_left {b : Multiset β} : Rel r 0 b ↔ b = 0

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ Rel r 0 b ↔ b = 0

Tactic:
rw [rel_iff]

Result:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem coeff_heval_zero (f : PowerSeries R) :
    (heval hx f).coeff 0 = PowerSeries.constantCoeff R f

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
⊢ ((powerSeriesFamily hx f).coeff 0) 0 = (coeff R 0) f

Tactic:
simp_all

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
⊢ ((heval hx) f).coeff 0 = (constantCoeff R) f

Tactic:
rw [coeff_heval, finsum_eq_single (fun n => ((powerSeriesFamily hx f).coeff 0) n) 0,
  ← PowerSeries.coeff_zero_eq_constantCoeff_apply]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
⊢ ((powerSeriesFamily hx f).coeff 0) 0 = (coeff R 0) f

Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily hx f).coeff 0) x_1 = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
n : ℕ
hn : ¬n = 0
⊢ (coeff R n) f * (x ^ n).coeff 0 = 0

Tactic:
exact mul_eq_zero_of_right ((PowerSeries.coeff R n) f) (coeff_eq_zero_of_lt_orderTop
  (lt_of_lt_of_le ((nsmul_pos_iff hn).mpr hx) orderTop_nsmul_le_orderTop_pow))

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
⊢ ∀ (x_1 : ℕ), x_1 ≠ 0 → ((powerSeriesFamily hx f).coeff 0) x_1 = 0

Tactic:
intro n hn

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ ((powerSeriesFamily hx f).coeff 0) n = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ ((powerSeriesFamily hx f).coeff 0) n = 0

Tactic:
simp_all only [ne_eq, coeff_toFun, smulFamily_toFun, powers_toFun, HahnSeries.coeff_smul,
  smul_eq_mul]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
n : ℕ
hn : ¬n = 0
⊢ (coeff R n) f * (x ^ n).coeff 0 = 0
-- Mathlib/Data/Rat/Lemmas.lean
theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprime a.natAbs b.natAbs)
    (h2 : Nat.Coprime c.natAbs d.natAbs) (h : (a : ℚ) / b = (c : ℚ) / d) : a = c ∧ b = d

Proof state:
case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c

Tactic:
rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]

Result:
no goals

Proof state:
case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d

Tactic:
rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]

Result:
no goals

Proof state:
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c ∧ b = d

Tactic:
apply And.intro

Result:
case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c

case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma sub_comp {n₁ n₂ n₁₂ : ℤ} (z₁ z₁' : Cochain F G n₁) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : (z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((z₁ - z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h - z₁'.comp z₂ h).v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((z₁ - z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h - z₁'.comp z₂ h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), sub_v, sub_comp]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
lemma ext {e e' : Pretrivialization F proj} (h₁ : ∀ x, e x = e' x)
    (h₂ : ∀ x, e.toPartialEquiv.symm x = e'.toPartialEquiv.symm x) (h₃ : e.baseSet = e'.baseSet) :
    e = e'

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
ext1 <;> [ext1; exact h₃]

Result:
case h₁.h
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
x✝ : Z
⊢ ↑e.toPartialEquiv x✝ = ↑e'.toPartialEquiv x✝

case h₁.hsymm
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
x✝ : B × F
⊢ ↑e.symm x✝ = ↑e'.symm x✝

case h₁.hs
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ e.source = e'.source

Proof state:
case h₁.h
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
x✝ : Z
⊢ ↑e.toPartialEquiv x✝ = ↑e'.toPartialEquiv x✝

Tactic:
apply h₁

Result:
no goals

Proof state:
case h₁.hsymm
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
x✝ : B × F
⊢ ↑e.symm x✝ = ↑e'.symm x✝

Tactic:
apply h₂

Result:
no goals

Proof state:
case h₁.hs
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ e.source = e'.source

Tactic:
rw [e.source_eq, e'.source_eq, h₃]

Result:
no goals