harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k : α} :
    get! (m.erase k) k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
k : α
⊢ get! (m.erase k) k = default

Tactic:
simp_to_model [erase] using List.getValue!_eraseKey_self

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_eq_empty {f g : α →₀ N} : f.neLocus g = ∅ ↔ f = g :=
  ⟨fun h =>
    ext fun a => not_not.mp (mem_neLocus.not.mp (Finset.eq_empty_iff_forall_not_mem.mp h a)),
    fun h => h ▸ by simp only [neLocus, Ne, eq_self_iff_true, not_true, Finset.filter_False]⟩

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
h : f = g
⊢ f.neLocus f = ∅

Tactic:
simp only [neLocus, Ne, eq_self_iff_true, not_true, Finset.filter_False]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma one_lt_pow_iff {n : ℕ} (hn : n ≠ 0) : ∀ {a}, 1 < a ^ n ↔ 1 < a
 | 0 => by simp [Nat.zero_pow (Nat.pos_of_ne_zero hn)]
 | 1 => by simp
 | a + 2 => by simp [one_lt_pow hn]

Proof state:
n : ℕ
hn : n ≠ 0
⊢ 1 < 1 ^ n ↔ 1 < 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
⊢ 1 < 0 ^ n ↔ 1 < 0

Tactic:
simp [Nat.zero_pow (Nat.pos_of_ne_zero hn)]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ 1 < (a + 2) ^ n ↔ 1 < a + 2

Tactic:
simp [one_lt_pow hn]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_sdiff_eq_prod_sdiff_iff :
    ∏ i ∈ s \ t, f i = ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i = ∏ i ∈ t, f i :=
  eq_comm.trans <| eq_iff_eq_of_mul_eq_mul <| by
    rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid α
s t : Finset ι
f : ι → α
⊢ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i = (∏ i ∈ s \ t, f i) * ∏ i ∈ t, f i

Tactic:
rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
  sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/NatCast.lean
lemma zero_le_four [Preorder α] [ZeroLEOneClass α] [AddLeftMono α] :
    (0 : α) ≤ 4

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 3 + 1

Tactic:
exact add_nonneg zero_le_three zero_le_one

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 4

Tactic:
rw [← three_add_one_eq_four]

Result:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 3 + 1
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem norm_one [Nontrivial E] : ‖(1 : E)‖ = 1

Proof state:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1

Tactic:
rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
⊢ ‖1‖ = 1

Tactic:
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero

Result:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
this : 0 < ‖1‖
⊢ ‖1‖ = 1
-- Mathlib/Order/FixedPoints.lean
theorem lfp_induction {p : α → Prop} (step : ∀ a, p a → a ≤ f.lfp → p (f a))
    (hSup : ∀ s, (∀ a ∈ s, p a) → p (sSup s)) : p f.lfp

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ lfp f
⊢ sSup s = lfp f

Tactic:
have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ lfp f
hmem : f (sSup s) ∈ s
⊢ sSup s = lfp f

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ lfp f
hmem : f (sSup s) ∈ s
⊢ sSup s = lfp f

Tactic:
exact h.antisymm (f.lfp_le <| le_sSup hmem)

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)
s : Set α := {a | a ≤ lfp f ∧ p a}
⊢ p (lfp f)

Tactic:
specialize hSup s fun a => And.right

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
⊢ p (lfp f)

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = lfp f

Tactic:
have h : sSup s ≤ f.lfp := sSup_le fun b => And.left

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ lfp f
⊢ sSup s = lfp f

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
⊢ p (lfp f)

Tactic:
suffices sSup s = f.lfp from this ▸ hSup

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = lfp f

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)
⊢ p (lfp f)

Tactic:
set s := { a | a ≤ f.lfp ∧ p a }

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)
s : Set α := {a | a ≤ lfp f ∧ p a}
⊢ p (lfp f)
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem isOpen_extChartAt_preimage (x : M) {s : Set E} (hs : IsOpen s) :
    IsOpen ((chartAt H x).source ∩ extChartAt I x ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
s : Set E
hs : IsOpen s
⊢ IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' s)

Tactic:
exact isOpen_extChartAt_preimage' x hs

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
s : Set E
hs : IsOpen s
⊢ IsOpen ((chartAt H x).source ∩ ↑(extChartAt I x) ⁻¹' s)

Tactic:
rw [← extChartAt_source I]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
s : Set E
hs : IsOpen s
⊢ IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' s)
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_lt_iff_le_mul' : a * b⁻¹ < c ↔ a < b * c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a * b⁻¹ < c ↔ a < b * c

Tactic:
rw [← inv_mul_lt_iff_lt_mul, mul_comm]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem pi_eq_bot : pi f = ⊥ ↔ ∃ i, f i = ⊥

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ pi f = ⊥ ↔ ∃ i, f i = ⊥

Tactic:
simpa using @pi_inf_principal_univ_pi_eq_bot ι α f fun _ => univ

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosed_sum_iff {s : Set (X ⊕ Y)} :
    IsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X ⊕ Y)
⊢ IsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_sum_iff, preimage_compl]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
@[simp, mfld_simps]
lemma lift_openEmbedding_symm_target (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
    (e.lift_openEmbedding hf).symm.target = f '' e.source

Proof state:
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : PartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ (e.lift_openEmbedding hf).symm.target = f '' e.source

Tactic:
rw [PartialHomeomorph.symm_target, e.lift_openEmbedding_source]

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma sub {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    MeromorphicAt (f - g) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f - g) x

Tactic:
convert hf.add hg.neg using 1

Result:
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ f - g = f + -g

Proof state:
case h.e'_6.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
z : 𝕜
⊢ (f - g) z = (f + -g) z

Tactic:
simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]

Result:
no goals

Proof state:
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ f - g = f + -g

Tactic:
ext1 z

Result:
case h.e'_6.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
z : 𝕜
⊢ (f - g) z = (f + -g) z
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ball_eq_ball' (ε : ℝ) (x : α) :
    UniformSpace.ball x { p | dist p.1 p.2 < ε } = Metric.ball x ε

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
ε : ℝ
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x {p | dist p.1 p.2 < ε} ↔ x✝ ∈ ball x ε

Tactic:
simp [dist_comm, UniformSpace.ball]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
ε : ℝ
x : α
⊢ UniformSpace.ball x {p | dist p.1 p.2 < ε} = ball x ε

Tactic:
ext

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
ε : ℝ
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x {p | dist p.1 p.2 < ε} ↔ x✝ ∈ ball x ε
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.finset_prod (hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x) :
    HasDerivAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
⊢ HasDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x

Tactic:
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
  (HasFDerivAt.finset_prod (fun i hi ↦ (hf i hi).hasFDerivAt)).hasDerivAt

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_pos_rat_lt {x : α} (x0 : 0 < x) : ∃ q : ℚ, 0 < q ∧ (q : α) < x

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x : α
x0 : 0 < x
⊢ ∃ q, 0 < q ∧ ↑q < x

Tactic:
simpa only [Rat.cast_pos] using exists_rat_btwn x0

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_mono (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
    (h : LiftPropWithinAt P g s x) (hts : t ⊆ s) : LiftPropWithinAt P g t x

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
⊢ LiftPropWithinAt P g t x

Tactic:
refine ⟨h.1.mono hts, mono (fun y hy ↦ ?_) h.2⟩

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : y ∈ ↑(chartAt H x).symm ⁻¹' t
⊢ y ∈ ↑(chartAt H x).symm ⁻¹' s

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : y ∈ ↑(chartAt H x).symm ⁻¹' t
⊢ y ∈ ↑(chartAt H x).symm ⁻¹' s

Tactic:
simp only [mfld_simps] at hy

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : ↑(chartAt H x).symm y ∈ t
⊢ y ∈ ↑(chartAt H x).symm ⁻¹' s

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : ↑(chartAt H x).symm y ∈ t
⊢ y ∈ ↑(chartAt H x).symm ⁻¹' s

Tactic:
simp only [hy, hts _, mfld_simps]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma eval_polynomialX_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    eval P W.polynomialX / P z ^ 4 =
      W.toAffine.polynomialX.evalEval (P x / P z ^ 2) (P y / P z ^ 3)

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialX / P z ^ 4 +
        (W.a₁ * P y / P z ^ 3 * 1 + 2 * W.a₂ * P x / P z ^ 2 * (P z ^ 2 / P z ^ 2) + W.a₄ * (P z ^ 4 / P z ^ 4)) -
      (Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) (toAffine W).polynomialX +
        (W.a₁ * P y / P z ^ 3 * (P z / P z) + 2 * W.a₂ * P x / P z ^ 2 * 1 + W.a₄ * 1)) =
    0

Tactic:
rw [eval_polynomialX, Affine.evalEval_polynomialX]

Result:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4)) / P z ^ 4 +
        (W.a₁ * P y / P z ^ 3 * 1 + 2 * W.a₂ * P x / P z ^ 2 * (P z ^ 2 / P z ^ 2) + W.a₄ * (P z ^ 4 / P z ^ 4)) -
      ((toAffine W).a₁ * (P y / P z ^ 3) -
          (3 * (P x / P z ^ 2) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z ^ 2) + (toAffine W).a₄) +
        (W.a₁ * P y / P z ^ 3 * (P z / P z) + 2 * W.a₂ * P x / P z ^ 2 * 1 + W.a₄ * 1)) =
    0

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4)) / P z ^ 4 +
        (W.a₁ * P y / P z ^ 3 * 1 + 2 * W.a₂ * P x / P z ^ 2 * (P z ^ 2 / P z ^ 2) + W.a₄ * (P z ^ 4 / P z ^ 4)) -
      ((toAffine W).a₁ * (P y / P z ^ 3) -
          (3 * (P x / P z ^ 2) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z ^ 2) + (toAffine W).a₄) +
        (W.a₁ * P y / P z ^ 3 * (P z / P z) + 2 * W.a₂ * P x / P z ^ 2 * 1 + W.a₄ * 1)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialX / P z ^ 4 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) (toAffine W).polynomialX

Tactic:
linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
  W.a₁ * P y / P z ^ 3 * div_self hPz - 2 * W.a₂ * P x / P z ^ 2 * div_self (pow_ne_zero 2 hPz)
    - W.a₄ * div_self (pow_ne_zero 4 hPz)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem chain'_dartAdj_darts {u v : V} : ∀ (p : G.Walk u v), List.Chain' G.DartAdj p.darts
  | nil => trivial
  -- Porting note: needed to defer `rfl` to help elaboration
  | cons h p => chain_dartAdj_darts (by rfl) p

Proof state:
V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ { toProd := (u, v✝), adj := h }.toProd.2 = v✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma isCircuit_iff_dep_forall_diff_singleton_indep :
    M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Proof state:
case inr
α : Type u_1
M : Matroid α
C : Set α
this : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, C ⊆ M.E → (M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
hCE : ¬C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
exact iff_of_false (hCE ∘ IsCircuit.subset_ground) (fun h ↦ hCE h.1.subset_ground)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
wlog hCE : C ⊆ M.E

Result:
case inr
α : Type u_1
M : Matroid α
C : Set α
this : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, C ⊆ M.E → (M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
hCE : ¬C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

α✝ : Type u_1
M✝ : Matroid α✝
C✝ : Set α✝
α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
-- Mathlib/Algebra/BigOperators/Finsupp.lean
lemma sum_cons' [AddCommMonoid M] [AddCommMonoid N] (n : ℕ) (σ : Fin n →₀ M) (i : M)
    (f : Fin (n+1) → M → N) (h : ∀ x, f x 0 = 0) :
    (sum (Finsupp.cons i σ) f) = f 0 i + sum σ (Fin.tail f)

Proof state:
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1 : Fin (n + 1), f i_1 ((cons i σ) i_1) = f 0 i + ∑ i : Fin n, Fin.tail f i (σ i)

Tactic:
simp_rw [Fin.sum_univ_succ, cons_zero, cons_succ]

Result:
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ f 0 i + ∑ x : Fin n, f x.succ (σ x) = f 0 i + ∑ i : Fin n, Fin.tail f i (σ i)

Proof state:
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
x✝ : Fin n
⊢ Fin.tail f x✝ 0 = 0

Tactic:
apply h

Result:
no goals

Proof state:
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ f 0 i + ∑ x : Fin n, f x.succ (σ x) = f 0 i + ∑ i : Fin n, Fin.tail f i (σ i)

Tactic:
congr

Result:
no goals

Proof state:
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
x✝ : Fin (n + 1)
⊢ f x✝ 0 = 0

Tactic:
apply h

Result:
no goals

Proof state:
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ (cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)

Tactic:
rw [sum_fintype _ _ (fun _ => by apply h), sum_fintype _ _ (fun _ => by apply h)]

Result:
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1 : Fin (n + 1), f i_1 ((cons i σ) i_1) = f 0 i + ∑ i : Fin n, Fin.tail f i (σ i)
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem span {i j j' : C} (f : i ⟶ j) (f' : i ⟶ j') :
    ∃ (k : C) (g : j ⟶ k) (g' : j' ⟶ k), f ≫ g = f' ≫ g' :=
  let ⟨K, G, G', _⟩ := IsFilteredOrEmpty.cocone_objs j j'
  let ⟨k, e, he⟩ := IsFilteredOrEmpty.cocone_maps (f ≫ G) (f' ≫ G')
  ⟨k, G ≫ e, G' ≫ e, by simpa only [← Category.assoc] ⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
i j j' : C
f : i ⟶ j
f' : i ⟶ j'
K : C
G : j ⟶ K
G' : j' ⟶ K
h✝ : True
k : C
e : K ⟶ k
he : (f ≫ G) ≫ e = (f' ≫ G') ≫ e
⊢ f ≫ G ≫ e = f' ≫ G' ≫ e

Tactic:
simpa only [← Category.assoc]

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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

Tactic:
by_cases hnm : n + 1 = m

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

Tactic:
simp [δ_comp_zero_cochain _ _ _ hnm]

Result:
no goals

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (z₁.comp ↑z₂ ⋯) = (δ n m z₁).comp ↑z₂ ⋯

Tactic:
simp [δ_shape _ _ hnm]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_pos_iff_of_neg_left (ha : a < 0) : 0 < a • b ↔ b < 0

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ 0 < a • b ↔ b < 0

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_neg_left ha (b₁ := (0 : β))

Result:
no goals