harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem drop_modify_of_lt (f : α → α) (n m) (l : List α) (h : n < m) :
    (modify f n l).drop m = l.drop m

Proof state:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
⊢ ∀ (i : Nat) (h₁ : i < (drop m (modify f n l)).length) (h₂ : i < (drop m l).length),
    (drop m (modify f n l))[i] = (drop m l)[i]

Tactic:
intro m' h₁ h₂

Result:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (drop m l).length
⊢ (drop m (modify f n l))[m'] = (drop m l)[m']

Proof state:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (drop m l).length
⊢ (drop m (modify f n l))[m'] = (drop m l)[m']

Tactic:
simp only [getElem_drop, getElem_modify, ite_eq_right_iff]

Result:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (drop m l).length
⊢ n = m + m' → f l[m + m'] = l[m + m']

Proof state:
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
⊢ drop m (modify f n l) = drop m l

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
⊢ (drop m (modify f n l)).length = (drop m l).length

case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
⊢ ∀ (i : Nat) (h₁ : i < (drop m (modify f n l)).length) (h₂ : i < (drop m l).length),
    (drop m (modify f n l))[i] = (drop m l)[i]

Proof state:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (drop m l).length
⊢ n = m + m' → f l[m + m'] = l[m + m']

Tactic:
intro h'

Result:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (drop m l).length
h' : n = m + m'
⊢ f l[m + m'] = l[m + m']

Proof state:
case hl
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
⊢ (drop m (modify f n l)).length = (drop m l).length

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n < m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (drop m l).length
h' : n = m + m'
⊢ f l[m + m'] = l[m + m']

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.preimage_add_right (hs : StrictConvex 𝕜 s) (z : E) :
    StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ interior s
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s

Tactic:
rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior ((fun x => z + x) ⁻¹' s)

Tactic:
refine preimage_interior_subset_interior_preimage (continuous_add_left _) ?_

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s

Tactic:
have h := hs hx hy ((add_right_injective _).ne hxy) ha hb hab

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ interior s
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s)

Tactic:
intro x hx y hy hxy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior ((fun x => z + x) ⁻¹' s)
-- Mathlib/NumberTheory/FactorisationProperties.lean
lemma perfect_iff_not_abundant_and_not_deficient (hn : 0 ≠ n) :
    Perfect n ↔ ¬ Abundant n ∧ ¬ Deficient n

Proof state:
n : ℕ
hn : 0 ≠ n
⊢ ∑ i ∈ n.properDivisors, i = n ∧ 0 < n ↔ ¬n < ∑ i ∈ n.properDivisors, i ∧ ¬∑ i ∈ n.properDivisors, i < n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
hn : 0 ≠ n
⊢ n.Perfect ↔ ¬n.Abundant ∧ ¬n.Deficient

Tactic:
dsimp only [Perfect, Abundant, Deficient]

Result:
n : ℕ
hn : 0 ≠ n
⊢ ∑ i ∈ n.properDivisors, i = n ∧ 0 < n ↔ ¬n < ∑ i ∈ n.properDivisors, i ∧ ¬∑ i ∈ n.properDivisors, i < n
-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem fourierIntegral_continuous [FirstCountableTopology W] (he : Continuous e)
    (hL : Continuous fun p : V × W ↦ L p.1 p.2) {f : V → E} (hf : Integrable f μ) :
    Continuous (fourierIntegral e μ L f)

Proof state:
case h_cont
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : IsTopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : FirstCountableTopology W
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f : V → E
hf : Integrable f μ
⊢ ∀ᵐ (a : V) ∂μ, Continuous fun x => e (-(L a) x) • f a

Tactic:
refine ae_of_all _ fun v ↦ (he.comp ?_).smul continuous_const

Result:
case h_cont
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : IsTopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : FirstCountableTopology W
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f : V → E
hf : Integrable f μ
v : V
⊢ Continuous fun x => -(L v) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat)

Proof state:
n : Nat
x y : BitVec n
⊢ x / y = BitVec.ofNat n (x.toNat / y.toNat)

Tactic:
have h : x.toNat / y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)

Result:
n : Nat
x y : BitVec n
h : x.toNat / y.toNat < 2 ^ n
⊢ x / y = BitVec.ofNat n (x.toNat / y.toNat)

Proof state:
n : Nat
x y : BitVec n
h : x.toNat / y.toNat < 2 ^ n
⊢ x.udiv y = BitVec.ofNat n (x.toNat / y.toNat)

Tactic:
simp [udiv, bv_toNat, h, Nat.mod_eq_of_lt]

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
h : x.toNat / y.toNat < 2 ^ n
⊢ x / y = BitVec.ofNat n (x.toNat / y.toNat)

Tactic:
rw [← udiv_eq]

Result:
n : Nat
x y : BitVec n
h : x.toNat / y.toNat < 2 ^ n
⊢ x.udiv y = BitVec.ofNat n (x.toNat / y.toNat)

Proof state:
n : Nat
x y : BitVec n
⊢ x.toNat < 2 ^ n

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem exists_mem_factors {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) : ∃ p, p ∈ factors x

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ factors x
right✝ : p' ~ᵤ p
⊢ ∃ p, p ∈ factors x

Tactic:
exact ⟨p, hp⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
⊢ ∃ p, p ∈ factors x

Tactic:
obtain ⟨p, hp, _⟩ := exists_mem_factors_of_dvd hx hp' hp'x

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ factors x
right✝ : p' ~ᵤ p
⊢ ∃ p, p ∈ factors x

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ ∃ p, p ∈ factors x

Tactic:
obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx

Result:
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
⊢ ∃ p, p ∈ factors x
-- Mathlib/Data/Real/Basic.lean
theorem mk_one : mk 1 = 1

Proof state:
⊢ mk 1 = { cauchy := 1 }

Tactic:
rfl

Result:
no goals

Proof state:
⊢ mk 1 = 1

Tactic:
rw [← ofCauchy_one]

Result:
⊢ mk 1 = { cauchy := 1 }
-- Mathlib/Data/Set/Insert.lean
lemma insert_diff_self_of_mem (ha : a ∈ s) : insert a (s \ {a}) = s

Proof state:
α : Type u
s : Set α
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
ext

Result:
case h
α : Type u
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ insert a (s \ {a}) ↔ x✝ ∈ s

Proof state:
case h
α : Type u
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ insert a (s \ {a}) ↔ x✝ ∈ s

Tactic:
simp +contextual [or_and_left, em, ha]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_div₀ (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [le_div_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/Probability/Kernel/WithDensity.lean
theorem withDensity_apply (κ : Kernel α β) [IsSFiniteKernel κ]
    (hf : Measurable (Function.uncurry f)) (a : α) :
    withDensity κ f a = (κ a).withDensity (f a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ (κ.withDensity f) a = (κ a).withDensity (f a)

Tactic:
rw [withDensity, dif_pos hf]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ { toFun := fun a => (κ a).withDensity (f a), measurable' := ⋯ } a = (κ a).withDensity (f a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ (κ.withDensity f) a = (κ a).withDensity (f a)

Tactic:
classical
rw [withDensity, dif_pos hf]
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ { toFun := fun a => (κ a).withDensity (f a), measurable' := ⋯ } a = (κ a).withDensity (f a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformGroup_inf {u₁ u₂ : UniformSpace β} (h₁ : @UniformGroup β u₁ _)
    (h₂ : @UniformGroup β u₂ _) : @UniformGroup β (u₁ ⊓ u₂) _

Proof state:
β : Type u_2
inst✝ : Group β
u₁ u₂ : UniformSpace β
h₁ : UniformGroup β
h₂ : UniformGroup β
⊢ UniformGroup β

Tactic:
refine uniformGroup_iInf fun b => ?_

Result:
β : Type u_2
inst✝ : Group β
u₁ u₂ : UniformSpace β
h₁ : UniformGroup β
h₂ : UniformGroup β
b : Bool
⊢ UniformGroup β

Proof state:
β : Type u_2
inst✝ : Group β
u₁ u₂ : UniformSpace β
h₁ : UniformGroup β
h₂ : UniformGroup β
b : Bool
⊢ UniformGroup β

Tactic:
cases b <;> assumption

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem formPerm_reverse (s : Cycle α) (h : Nodup s) :
    formPerm s.reverse (nodup_reverse_iff.mpr h) = (formPerm s h)⁻¹

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α)) a✝)).formPerm ⋯ = (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h)⁻¹

Tactic:
simpa using formPerm_reverse _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Nodup
⊢ s.reverse.formPerm ⋯ = (s.formPerm h)⁻¹

Tactic:
induction s using Quot.inductionOn

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α)) a✝)).formPerm ⋯ = (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h)⁻¹
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCard_zero_left (s : Multiset α) : powersetCard 0 s = {0} :=
  Quotient.inductionOn s fun l => by simp [powersetCard_coe']

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ powersetCard 0 ⟦l⟧ = {0}

Tactic:
simp [powersetCard_coe']

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.mono_g (hS : S.Exact) (hf : S.f = 0) : Mono S.g

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
⊢ ∀ {P : C} (g : P ⟶ S.X₂), g ≫ S.g = 0 → g = 0

Tactic:
intro A x₂ hx₂

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ x₂ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝ : S.HasHomology
this : Epi S.toCycles
⊢ Mono S.g

Tactic:
have : S.iCycles = 0 := by rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
⊢ Mono S.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
⊢ Mono S.g

Tactic:
have := hS.hasHomology

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this : S.HasHomology
⊢ Mono S.g

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ x₂ = 0

Tactic:
rw [← S.liftCycles_i x₂ hx₂, this, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
⊢ Mono S.g

Tactic:
apply Preadditive.mono_of_cancel_zero

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
⊢ ∀ {P : C} (g : P ⟶ S.X₂), g ≫ S.g = 0 → g = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝ : S.HasHomology
this : Epi S.toCycles
⊢ S.iCycles = 0

Tactic:
rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this : S.HasHomology
⊢ Mono S.g

Tactic:
have := hS.epi_toCycles

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝ : S.HasHomology
this : Epi S.toCycles
⊢ Mono S.g
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem liftAux.smul (r : R) (x) : liftAux f (r • x) = r • liftAux f x :=
  TensorProduct.induction_on x (smul_zero _).symm
    (fun p q => by simp_rw [← tmul_smul, liftAux_tmul, (f p).map_smul])
    fun p q ih1 ih2 => by simp_rw [smul_add, (liftAux f).map_add, ih1, ih2, smul_add]

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
r : R
x : M ⊗[R] N
p : M
q : N
⊢ (liftAux f) (r • p ⊗ₜ[R] q) = r • (liftAux f) (p ⊗ₜ[R] q)

Tactic:
simp_rw [← tmul_smul, liftAux_tmul, (f p).map_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
r : R
x p q : M ⊗[R] N
ih1 : (liftAux f) (r • p) = r • (liftAux f) p
ih2 : (liftAux f) (r • q) = r • (liftAux f) q
⊢ (liftAux f) (r • (p + q)) = r • (liftAux f) (p + q)

Tactic:
simp_rw [smul_add, (liftAux f).map_add, ih1, ih2, smul_add]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_eq_one_of_le (h : B ≤ A) : relrank A B = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : B ≤ A
⊢ A.relrank B = 1

Tactic:
rw [← inf_relrank_right, inf_eq_right.2 h, relrank_self]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem tails_append :
    ∀ s t : List α, tails (s ++ t) = (s.tails.map fun l => l ++ t) ++ t.tails.tail
  | [], [] => by simp
  | [], a :: t => by simp
  | a :: s, t => by simp [tails_append s t]

Proof state:
α : Type u_1
⊢ ([] ++ []).tails = map (fun l => l ++ []) [].tails ++ [].tails.tail

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).tails = map (fun l => l ++ a :: t) [].tails ++ (a :: t).tails.tail

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
s t : List α
⊢ (a :: s ++ t).tails = map (fun l => l ++ t) (a :: s).tails ++ t.tails.tail

Tactic:
simp [tails_append s t]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
lemma lookup_graph (f : α → β) {a : α} {as : List α} (h : a ∈ as) :
    lookup a (as.map fun x => (x, f x)) = some (f a)

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

Tactic:
by_cases ha : a = a'

Result:
case pos
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
ha : a = a'
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

case neg
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
ha : ¬a = a'
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a : α
as : List α
h : a ∈ as
⊢ lookup a (map (fun x => (x, f x)) as) = some (f a)

Tactic:
induction' as with a' as ih

Result:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x => (x, f x)) []) = some (f a)

case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

Proof state:
case neg
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
ha : ¬a = a'
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

Tactic:
simpa [lookup_cons, beq_false_of_ne ha] using ih (List.mem_of_ne_of_mem ha h)

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x => (x, f x)) []) = some (f a)

Tactic:
exact (List.not_mem_nil _ h).elim

Result:
no goals

Proof state:
case pos
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
ha : a = a'
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

Tactic:
simp [ha, lookup_cons]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
lemma permutations_take_two (x y : α) (s : List α) :
    (x :: y :: s).permutations.take 2 = [x :: y :: s, y :: x :: s]

Proof state:
α : Type u_1
x y : α
s : List α
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]

Tactic:
induction s <;> simp [permutations, permutationsAux.rec]

Result:
no goals