harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as

Proof state:
α : Type u_1
x : α
as : List α
⊢ x ∈ as.reverse ↔ x ∈ as

Tactic:
simp [reverse, mem_reverseAux]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem heq_cast_iff_heq {α β γ : Sort _} (e : β = γ) (a : α) (b : β) :
    HEq a (cast e b) ↔ HEq a b

Proof state:
α β : Sort u_1
a : α
b : β
⊢ HEq a (cast ⋯ b) ↔ HEq a b

Tactic:
rfl

Result:
no goals

Proof state:
α β γ : Sort u_1
e : β = γ
a : α
b : β
⊢ HEq a (cast e b) ↔ HEq a b

Tactic:
subst e

Result:
α β : Sort u_1
a : α
b : β
⊢ HEq a (cast ⋯ b) ↔ HEq a b
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_eq_zero_iff' {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    ∫⁻ a, f a ∂μ = 0 ↔ f =ᵐ[μ] 0 :=
  have : ∫⁻ _ : α, 0 ∂μ ≠ ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α), 0 ∂μ ≠ ⊤

Tactic:
simp [lintegral_zero, zero_ne_top]

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem newton_seq_dist_aux (n : ℕ) :
    ∀ k : ℕ, ‖newton_seq (n + k) - newton_seq n‖ ≤ ‖F.derivative.eval a‖ * T ^ 2 ^ n
  | 0 => by simp [T_pow_nonneg, mul_nonneg]
  | k + 1 =>
    have : 2 ^ n ≤ 2 ^ (n + k)

Proof state:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ 1 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ 2 ^ n ≤ 2 ^ (n + k)

Tactic:
apply pow_right_mono₀

Result:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ 1 ≤ 2

case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ n ≤ n + k

Proof state:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ n ≤ n + k

Tactic:
apply Nat.le_add_right

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖newton_seq (n + 0) - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n

Tactic:
simp [T_pow_nonneg, mul_nonneg]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
this : 2 ^ n ≤ 2 ^ (n + k)
⊢ ‖newton_seq (n + k + 1) - newton_seq n‖ =
    ‖newton_seq (n + k + 1) - newton_seq (n + k) + (newton_seq (n + k) - newton_seq n)‖

Tactic:
rw [← sub_add_sub_cancel]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
n k : ℕ
this : 2 ^ n ≤ 2 ^ (n + k)
⊢ ‖newton_seq (n + (k + 1)) - newton_seq n‖ = ‖newton_seq (n + k + 1) - newton_seq n‖

Tactic:
rw [add_assoc]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
@[simp]
lemma mem_mk' (carrier : Set R) (zero_mem add_mem neg_mem mul_mem_left mul_mem_right) (x : R) :
    x ∈ mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ (mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right).ringCon x 0 ↔ x ∈ carrier

Tactic:
simp [mk']

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ x ∈ mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier

Tactic:
rw [mem_iff]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ (mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right).ringCon x 0 ↔ x ∈ carrier
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem mul_eq_sum_sum :
    p * q = ∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a)

Proof state:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a)).toFinsupp

Tactic:
rcases p with ⟨⟩

Result:
case a.ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } * q).toFinsupp =
    (∑ i ∈ { toFinsupp := toFinsupp✝ }.support,
        q.sum fun j a => (monomial (i + j)) ({ toFinsupp := toFinsupp✝ }.coeff i * a)).toFinsupp

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p * q = ∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a)

Tactic:
apply toFinsupp_injective

Result:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a)).toFinsupp

Proof state:
case a.ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } * q).toFinsupp =
    (∑ i ∈ { toFinsupp := toFinsupp✝ }.support,
        q.sum fun j a => (monomial (i + j)) ({ toFinsupp := toFinsupp✝ }.coeff i * a)).toFinsupp

Tactic:
rcases q with ⟨⟩

Result:
case a.ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    (∑ i ∈ { toFinsupp := toFinsupp✝¹ }.support,
        { toFinsupp := toFinsupp✝ }.sum fun j a =>
          (monomial (i + j)) ({ toFinsupp := toFinsupp✝¹ }.coeff i * a)).toFinsupp

Proof state:
case a.ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    (∑ i ∈ { toFinsupp := toFinsupp✝¹ }.support,
        { toFinsupp := toFinsupp✝ }.sum fun j a =>
          (monomial (i + j)) ({ toFinsupp := toFinsupp✝¹ }.coeff i * a)).toFinsupp

Tactic:
simp_rw [sum, coeff, toFinsupp_sum, support, toFinsupp_mul, toFinsupp_monomial,
  AddMonoidAlgebra.mul_def, Finsupp.sum]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Tower.lean
theorem aeval_algebraMap_eq_zero_iff_of_injective {x : σ → A} {p : MvPolynomial σ R}
    (h : Function.Injective (algebraMap A B)) :
    aeval (algebraMap A B ∘ x) p = 0 ↔ aeval x p = 0

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem le_sup_inf (a b c : α) : (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)

Tactic:
rw [le_sup_inf_aux, add_self, mul_self, zero_add]

Result:
no goals
-- Mathlib/Data/NNRat/Lemmas.lean
lemma toNNRat_div' (hq : 0 ≤ q) : toNNRat (p / q) = toNNRat p / toNNRat q

Proof state:
p q : ℚ
hq : 0 ≤ q
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_indicator₀ {s : Set α} (hs : NullMeasurableSet s μ) (f : α → ℝ≥0∞) :
    ∫⁻ a, s.indicator f a ∂μ = ∫⁻ a in s, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
  lintegral_indicator (measurableSet_toMeasurable _ _),
  Measure.restrict_congr_set hs.toMeasurable_ae_eq]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem prev_ne_cons_cons (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x ≠ z) :
    prev (y :: z :: l) x h = prev (z :: l) x (by simpa [hy] using h)

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = (z :: head✝ :: tail✝).prev x ⋯

Tactic:
rw [prev, dif_neg hy, if_neg hz]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
h : x ∈ [y, z]
⊢ [y, z].prev x h = [z].prev x ⋯

Tactic:
simp [hy, hz] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ x ∈ z :: l

Tactic:
simpa [hy] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ (y :: z :: l).prev x h = (z :: l).prev x ⋯

Tactic:
cases l

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
h : x ∈ [y, z]
⊢ [y, z].prev x h = [z].prev x ⋯

case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = (z :: head✝ :: tail✝).prev x ⋯
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem eq_withDensity_rnDeriv₀ {s : Measure α} {f : α → ℝ≥0∞}
    (hf : AEMeasurable f ν) (hs : s ⟂ₘ ν) (hadd : μ = s + ν.withDensity f) :
    ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [withDensity_congr_ae hf.ae_eq_mk] at hadd ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity (AEMeasurable.mk f hf)
⊢ ν.withDensity (AEMeasurable.mk f hf) = ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f ν
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity (AEMeasurable.mk f hf)
⊢ ν.withDensity (AEMeasurable.mk f hf) = ν.withDensity (μ.rnDeriv ν)

Tactic:
exact eq_withDensity_rnDeriv hf.measurable_mk hs hadd

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem ext_component_iff {f g : ⨁ i, M i} :
    f = g ↔ ∀ i, component R ι M i f = component R ι M i g :=
  ⟨fun h _ ↦ by rw [h], ext_component R⟩

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ (component R ι M x✝) f = (component R ι M x✝) g

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem intermediate_value_univ₂ [PreconnectedSpace X] {a b : X} {f g : X → α} (hf : Continuous f)
    (hg : Continuous g) (ha : f a ≤ g a) (hb : g b ≤ f b) : ∃ x, f x = g x

Proof state:
case intro.intro.intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous f
hg : Continuous g
ha : f a ≤ g a
hb : g b ≤ f b
x : X
left✝ : x ∈ univ
hfg : f x ≤ g x
hgf : g x ≤ f x
⊢ ∃ x, f x = g x

Tactic:
exact ⟨x, le_antisymm hfg hgf⟩

Result:
no goals

Proof state:
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous f
hg : Continuous g
ha : f a ≤ g a
hb : g b ≤ f b
⊢ ∃ x, f x = g x

Tactic:
obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty :=
  isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg)
    (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩

Result:
case intro.intro.intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous f
hg : Continuous g
ha : f a ≤ g a
hb : g b ≤ f b
x : X
left✝ : x ∈ univ
hfg : f x ≤ g x
hgf : g x ≤ f x
⊢ ∃ x, f x = g x
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
lemma continuous_counit : Continuous (counit : _ → X)

Proof state:
X : Type u_1
tX : TopologicalSpace X
⊢ Continuous counit

Tactic:
rw [continuous_iff_coinduced_le]

Result:
X : Type u_1
tX : TopologicalSpace X
⊢ coinduced counit instTopologicalSpaceOf ≤ tX

Proof state:
X : Type u_1
tX : TopologicalSpace X
⊢ coinduced counit instTopologicalSpaceOf ≤ tX

Tactic:
exact deltaGenerated_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_sub_cancel (x : Int) (n : Nat) : Int.bmod (x - n) n = Int.bmod x n

Proof state:
x : Int
n : Nat
⊢ (x - ↑n).bmod n = x.bmod n

Tactic:
simp [bmod_def]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem treesOfNumNodesEq_zero : treesOfNumNodesEq 0 = {nil}

Proof state:
⊢ treesOfNumNodesEq 0 = {nil}

Tactic:
rw [treesOfNumNodesEq]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma contravariant_sequence_exact₁ {n₀ : ℕ} (x₁ : Ext S.X₁ Y n₀) {n₁ : ℕ} (hn₁ : 1 + n₀ = n₁)
    (hx₁ : hS.extClass.comp x₁ hn₁ = 0) :
    ∃ (x₂ : Ext S.X₂ Y n₀), (mk₀ S.f).comp x₂ (zero_add n₀) = x₁

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁)) ⋯).Exact
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Tactic:
have := contravariant_sequence_exact₁' hS Y n₀ n₁ hn₁

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁)) ⋯).Exact
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y hn₁))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Tactic:
exact this x₁ hx₁

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a ∈ s, f a = g a) : f '' s = g '' s

Proof state:
case h
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ a ∈ s, f a = g a
x : β
⊢ x ∈ f '' s ↔ x ∈ g '' s

Tactic:
exact exists_congr fun a ↦ and_congr_right fun ha ↦ by rw [h a ha]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ a ∈ s, f a = g a
⊢ f '' s = g '' s

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ a ∈ s, f a = g a
x : β
⊢ x ∈ f '' s ↔ x ∈ g '' s

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ a ∈ s, f a = g a
x : β
a : α
ha : a ∈ s
⊢ f a = x ↔ g a = x

Tactic:
rw [h a ha]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem add_zero (x : X[S⁻¹]) : x + 0 = x

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ x + 0 = x

Tactic:
induction x

Result:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ r✝ /ₒ s✝ + 0 = r✝ /ₒ s✝

Proof state:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ (r✝ + 0) /ₒ s✝ = r✝ /ₒ s✝

Tactic:
simp

Result:
no goals

Proof state:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ r✝ /ₒ s✝ + 0 = r✝ /ₒ s✝

Tactic:
rw [← zero_oreDiv, add_oreDiv]

Result:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ (r✝ + 0) /ₒ s✝ = r✝ /ₒ s✝
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem nonunits_injective : Function.Injective (nonunits : ValuationSubring K → Subsemigroup _) :=
  fun A B h => by simpa only [le_antisymm_iff, nonunits_le_nonunits] using h.symm

Proof state:
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.nonunits = B.nonunits
⊢ A = B

Tactic:
simpa only [le_antisymm_iff, nonunits_le_nonunits] using h.symm

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithBot.ofDual_lt_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    WithBot.ofDual x < y ↔ y.toDual < x

Proof state:
α : Type u_1
inst✝ : LT α
x : WithBot αᵒᵈ
y : WithTop α
⊢ WithBot.ofDual x < y ↔ WithTop.toDual y < x

Tactic:
cases x <;> cases y <;> simp [toDual_lt]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma eqToHom_domain_lift_id {p : 𝒳 ⥤ 𝒮} {a b : 𝒳} (hab : a = b) {R : 𝒮} (hR : p.obj a = R) :
    p.IsHomLift (𝟙 R) (eqToHom hab)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
hab : a = b
R : 𝒮
hR : p.obj a = R
⊢ p.IsHomLift (𝟙 R) (eqToHom hab)

Tactic:
subst hR hab

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_pUnit [AddCommMonoid α] [Mul α] (v w : PUnit → α) : v ⬝ᵥ w = v ⟨⟩ * w ⟨⟩

Proof state:
α : Type v
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
v w : PUnit.{u_10 + 1} → α
⊢ v ⬝ᵥ w = v PUnit.unit * w PUnit.unit

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1
  | 0 => by decide
  | 1 => by decide
  | n + 2 => by omega

Proof state:
⊢ 1 < 1 ↔ 1 ≠ 0 ∧ 1 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
⊢ 1 < n + 2 ↔ n + 2 ≠ 0 ∧ n + 2 ≠ 1

Tactic:
omega

Result:
no goals

Proof state:
⊢ 1 < 0 ↔ 0 ≠ 0 ∧ 0 ≠ 1

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem le_emultiplicity_map {F : Type*} [FunLike F α β] [MonoidHomClass F α β]
    (f : F) {a b : α} :
    emultiplicity a b ≤ emultiplicity (f a) (f b) :=
  emultiplicity_le_emultiplicity_iff.2 fun n ↦ by rw [← map_pow]; exact map_dvd f

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → f (a ^ n) ∣ f b

Tactic:
exact map_dvd f

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → f a ^ n ∣ f b

Tactic:
rw [← map_pow]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → f (a ^ n) ∣ f b
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.sub_odd (ha : Odd a) (hb : Odd b) : Even (a - b)

Proof state:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a + -b)

Tactic:
exact ha.add_odd hb.neg

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a - b)

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a + -b)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_eq_self : toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b = b + 0 • p

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ z, b = b + z • p

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b = b ↔ b ∈ Set.Ico a (a + p)

Tactic:
rw [toIcoMod_eq_iff, and_iff_left]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ z, b = b + z • p
-- Mathlib/Topology/Compactness/Compact.lean
theorem Topology.IsInducing.isCompact_preimage (hf : IsInducing f) (hf' : IsClosed (range f))
    {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed (range f)
K : Set Y
hK : IsCompact (K ∩ range f)
⊢ IsCompact (f ⁻¹' K)

Tactic:
rwa [hf.isCompact_iff, image_preimage_eq_inter_range]

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed (range f)
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
replace hK := hK.inter_right hf'

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed (range f)
K : Set Y
hK : IsCompact (K ∩ range f)
⊢ IsCompact (f ⁻¹' K)