harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem card_interedges_finpartition [DecidableEq α] [DecidableEq β] (P : Finpartition s)
    (Q : Finpartition t) :
    #(interedges r s t) = ∑ ab ∈ P.parts ×ˢ Q.parts, #(interedges r ab.1 ab.2)

Proof state:
case e_f
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ (fun a => #(interedges r a t)) = fun x => ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)

Tactic:
ext

Result:
case e_f.h
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
x✝ : Finset α
⊢ #(interedges r x✝ t) = ∑ y ∈ Q.parts, #(interedges r (x✝, y).1 (x✝, y).2)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ #(interedges r s t) = ∑ ab ∈ P.parts ×ˢ Q.parts, #(interedges r ab.1 ab.2)

Tactic:
rw [card_interedges_finpartition_left _ P, sum_product]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a ∈ P.parts, #(interedges r a t) = ∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)

Proof state:
case e_f.h
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
x✝ : Finset α
⊢ #(interedges r x✝ t) = ∑ y ∈ Q.parts, #(interedges r (x✝, y).1 (x✝, y).2)

Tactic:
rw [card_interedges_finpartition_right]

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a ∈ P.parts, #(interedges r a t) = ∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)

Tactic:
congr

Result:
case e_f
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ (fun a => #(interedges r a t)) = fun x => ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_sub_of_degree_lt' (h : Polynomial.degree p < Polynomial.degree q) :
    (p - q).leadingCoeff = -q.leadingCoeff

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff

Tactic:
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff

Tactic:
rw [← q.degree_neg] at h

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff
-- Mathlib/FieldTheory/Separable.lean
theorem not_separable_zero [Nontrivial R] : ¬Separable (0 : R[X])

Proof state:
case intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x y : R[X]
h : x * 0 + y * derivative 0 = 1
⊢ False

Tactic:
simp only [derivative_zero, mul_zero, add_zero, zero_ne_one] at h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬Separable 0

Tactic:
rintro ⟨x, y, h⟩

Result:
case intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x y : R[X]
h : x * 0 + y * derivative 0 = 1
⊢ False
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem DifferentiableWithinAt.finset_prod (hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) :
    DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i ·) s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt 𝕜 (fun x => ∏ i ∈ u, f i x) s x

Tactic:
exact (HasDerivWithinAt.finset_prod (fun i hi ↦
  DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt 𝕜 (fun x => ∏ i ∈ u, f i x) s x

Tactic:
classical
exact (HasDerivWithinAt.finset_prod (fun i hi ↦
  DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem ListBlank.nth_map {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ')
    (l : ListBlank Γ) (n : ℕ) : (l.map f).nth n = f (l.nth n)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = f.f (l.getD n default)

Tactic:
rw [← List.getD_map _ _ f]

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)

Tactic:
simp

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (map f ⟦l⟧).nth n = f.f (nth ⟦l⟧ n)

Tactic:
suffices ((mk l).map f).nth n = f ((mk l).nth n) by exact this

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (map f (mk l)).nth n = f.f ((mk l).nth n)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
n : ℕ
⊢ (map f l).nth n = f.f (l.nth n)

Tactic:
refine l.inductionOn fun l ↦ ?_

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (map f ⟦l⟧).nth n = f.f (nth ⟦l⟧ n)

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
this : (map f (mk l)).nth n = f.f ((mk l).nth n)
⊢ (map f ⟦l⟧).nth n = f.f (nth ⟦l⟧ n)

Tactic:
exact this

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (map f (mk l)).nth n = f.f ((mk l).nth n)

Tactic:
simp only [ListBlank.map_mk, ListBlank.nth_mk, ← List.getD_default_eq_getI]

Result:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l✝ : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = f.f (l.getD n default)
-- Mathlib/Data/Matroid/Closure.lean
lemma indep_iff_forall_closure_ssubset_of_ssubset (hI : I ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
rw [show I = insert e (I \ {e}) by simp [heI], ← closure_insert_closure_eq_closure_insert,
  insert_eq_of_mem hecl]

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (M.closure (I \ {e}))

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (M.closure (I \ {e}))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I

Tactic:
refine ⟨fun h _ ↦ h.closure_ssubset_closure,
  fun h ↦ (indep_iff_forall_not_mem_closure_diff hI).2 fun e heI hecl ↦ ?_⟩

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ False

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ I = insert e (I \ {e})

Tactic:
simp [heI]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ False

Tactic:
refine (h (diff_singleton_sSubset.2 heI)).ne ?_

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I
-- Mathlib/Data/Matrix/Mul.lean
theorem transpose_mul [AddCommMonoid α] [CommSemigroup α] [Fintype n] (M : Matrix m n α)
    (N : Matrix n l α) : (M * N)ᵀ = Nᵀ * Mᵀ

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommMonoid α
inst✝¹ : CommSemigroup α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
i✝ : l
j✝ : m
⊢ (M * N)ᵀ i✝ j✝ = (Nᵀ * Mᵀ) i✝ j✝

Tactic:
apply dotProduct_comm

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommMonoid α
inst✝¹ : CommSemigroup α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
⊢ (M * N)ᵀ = Nᵀ * Mᵀ

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommMonoid α
inst✝¹ : CommSemigroup α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n l α
i✝ : l
j✝ : m
⊢ (M * N)ᵀ i✝ j✝ = (Nᵀ * Mᵀ) i✝ j✝
-- Mathlib/Data/Sym/Sym2.lean
theorem map_map {g : β → γ} {f : α → β} (x : Sym2 α) : map g (map f x) = map (g ∘ f) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x : Sym2 α
⊢ map g (map f x) = map (g ∘ f) x

Tactic:
induction x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ y✝ : α
⊢ map g (map f s(x✝, y✝)) = map (g ∘ f) s(x✝, y✝)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝ y✝ : α
⊢ map g (map f s(x✝, y✝)) = map (g ∘ f) s(x✝, y✝)

Tactic:
aesop

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem contMDiffWithinAt_prod_module_iff (f : M → F₁ × F₂) :
    ContMDiffWithinAt I 𝓘(𝕜, F₁ × F₂) n f s x ↔
      ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧
      ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffWithinAt I 𝓘(𝕜, F₁ × F₂) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffWithinAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffWithinAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f s x ↔
    ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x

Tactic:
exact contMDiffWithinAt_prod_iff f

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem derivWithin_comp_of_eq (hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y)
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s s')
    (hy : h x = y) :
    derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
y : 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hy : h x = y
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
subst hy

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
exact derivWithin_comp x hh₂ hh hs

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma δ_eq_zero {n : ℤ} (z : Cocycle F G n) (m : ℤ) : δ n m (z : Cochain F G n) = 0

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ ↑z ∈ cocycle F G n

Tactic:
exact z.2

Result:
no goals

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m ↑z = 0

Tactic:
exact δ_shape n m h _

Result:
no goals

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ δ n m ↑z = 0

Tactic:
rw [← mem_iff n m h]

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ ↑z ∈ cocycle F G n

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
⊢ δ n m ↑z = 0

Tactic:
by_cases h : n + 1 = m

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ δ n m ↑z = 0

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m ↑z = 0
-- Mathlib/Data/Rat/Floor.lean
theorem isNat_intFloor {R} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℕ) :
    IsNat r m → IsNat ⌊r⌋ m

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ ⌊↑m⌋ = ↑m

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌊r⌋ m

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌊↑m⌋ m

Proof state:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌊↑m⌋ m

Tactic:
exact ⟨by simp⟩

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma homologyMap'_op : (homologyMap' φ h₁ h₂).op =
    h₂.iso.inv.op ≫ homologyMap' (opMap φ) h₂.op h₁.op ≫ h₁.iso.hom.op :=
  Quiver.Hom.unop_inj (by
    dsimp
    have γ : HomologyMapData φ h₁ h₂ := default
    simp only [γ.homologyMap'_eq, γ.op.homologyMap'_eq, HomologyData.op_left,
      HomologyMapData.op_left, RightHomologyMapData.op_φH, Quiver.Hom.unop_op, assoc,
      ← γ.comm_assoc, Iso.hom_inv_id, comp_id])

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ (homologyMap' φ h₁ h₂).op.unop = (h₂.iso.inv.op ≫ homologyMap' (opMap φ) h₂.op h₁.op ≫ h₁.iso.hom.op).unop

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ (homologyMap' (opMap φ) h₂.op h₁.op).unop) ≫ h₂.iso.inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ (homologyMap' (opMap φ) h₂.op h₁.op).unop) ≫ h₂.iso.inv

Tactic:
have γ : HomologyMapData φ h₁ h₂ := default

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
γ : HomologyMapData φ h₁ h₂
⊢ homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ (homologyMap' (opMap φ) h₂.op h₁.op).unop) ≫ h₂.iso.inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
γ : HomologyMapData φ h₁ h₂
⊢ homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ (homologyMap' (opMap φ) h₂.op h₁.op).unop) ≫ h₂.iso.inv

Tactic:
simp only [γ.homologyMap'_eq, γ.op.homologyMap'_eq, HomologyData.op_left,
  HomologyMapData.op_left, RightHomologyMapData.op_φH, Quiver.Hom.unop_op, assoc,
  ← γ.comm_assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem toMul_list_sum (s : List (Additive α)) : s.sum.toMul = (s.map toMul).prod

Proof state:
α : Type u_3
inst✝ : Monoid α
s : List (Additive α)
⊢ toMul s.sum = (List.map (⇑toMul) s).prod

Tactic:
simp [toMul, ofMul]

Result:
α : Type u_3
inst✝ : Monoid α
s : List (Additive α)
⊢ s.sum = s.prod

Proof state:
α : Type u_3
inst✝ : Monoid α
s : List (Additive α)
⊢ s.sum = s.prod

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isStronglyAtomic_dual_iff_is_stronglyCoatomic :
    IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α

Proof state:
α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α

Tactic:
simpa [isStronglyAtomic_iff, OrderDual.exists, OrderDual.forall,
  OrderDual.toDual_le_toDual, and_comm, isStronglyCoatomic_iff] using forall_comm

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem opNorm_zero : ‖(0 : NormedAddGroupHom V₁ V₂)‖ = 0 :=
  le_antisymm
    (csInf_le bounds_bddBelow
      ⟨ge_of_eq rfl, fun _ =>
        le_of_eq
          (by
            rw [zero_mul]
            exact norm_zero)⟩)
    (opNorm_nonneg _)

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0 * ‖x✝‖

Tactic:
rw [zero_mul]

Result:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0

Tactic:
exact norm_zero

Result:
no goals
-- Mathlib/Tactic/Sat/FromLRAT.lean
theorem Fmla.reify_or {f₁ : Fmla} {a : Prop} {f₂ : Fmla} {b : Prop}
    (h₁ : Fmla.reify v f₁ a) (h₂ : Fmla.reify v f₂ b) : Fmla.reify v (f₁.and f₂) (a ∨ b)

Proof state:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
⊢ reify v (f₁.and f₂) (a ∨ b)

Tactic:
refine ⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩

Result:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
⊢ False

Proof state:
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False

Tactic:
exact hn <| Or.inl <| h₁.1 fun Hc ↦ hn' <| Hc.1 _ h

Result:
no goals

Proof state:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
⊢ False

Tactic:
rcases List.mem_append.1 h with h | h

Result:
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False

case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Proof state:
case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Tactic:
exact hn <| Or.inr <| h₂.1 fun Hc ↦ hn' <| Hc.1 _ h

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem coe_iInf {ι : Sort*} {S : ι → Subfield K} : (↑(⨅ i, S i) : Set K) = ⋂ i, S i

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
S : ι → Subfield K
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem length_cyclicPermutations_of_ne_nil (l : List α) (h : l ≠ []) :
    length (cyclicPermutations l) = length l

Proof state:
α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations.length = l.length

Tactic:
simp [cyclicPermutations_of_ne_nil _ h]

Result:
no goals