harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem add {x y : K_hat R K} (hx : x.IsFiniteAdele) (hy : y.IsFiniteAdele) :
    (x + y).IsFiniteAdele

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : Valued.v (x v) ⊔ Valued.v (y v) ≤ 1
⊢ (x + y) v ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers, Pi.add_apply]

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x y : K_hat R K
hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite
hy : {x | y x ∉ adicCompletionIntegers K x}.Finite
v : HeightOneSpectrum R
hv : Valued.v (x v) ⊔ Valued.v (y v) ≤ 1
⊢ Valued.v (x v + y v) ≤ 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
    (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
    (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
    (htrue : ⟦aig, trueRef, assign⟧ = true)
      :
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx

Proof state:
case hx
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
lhs rhs : BitVec w
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
qbv rbv : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
idx✝ : Nat
hidx✝ : idx✝ < w
hdiscr : rbv.shiftConcat (lhs.getLsbD (wn - 1)) < rhs
idx : Nat
hidx : idx < w
⊢ ({ lhs := q.cast ⋯, bit := { gate := falseRef.gate, hgate := ⋯ } }.lhs.get idx hidx).gate < aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
    (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
    (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
    (htrue : ⟦aig, trueRef, assign⟧ = true)
      :
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx

Proof state:
case hright
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
lhs rhs : BitVec w
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
qbv rbv : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
idx✝ : Nat
hidx✝ : idx✝ < w
idx : Nat
hidx : idx < w
⊢ ({ lhs := (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast ⋯,
              rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }.rhs.get
        idx hidx).gate <
    aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d : AIG.RefVec aig w) (wn wr : Nat)
    (q r : AIG.RefVec aig w) (qbv rbv : BitVec w)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
    (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
    (htrue : ⟦aig, trueRef, assign⟧ = true)
      :
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx

Proof state:
case hb
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
lhs rhs : BitVec w
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
qbv rbv : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
idx : Nat
hidx : idx < w
hdiscr : rbv.shiftConcat (lhs.getLsbD (wn - 1)) < rhs
⊢ falseRef.gate < aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurableRec_omega1 (s : Set (Set α)) :
    generateMeasurableRec s (ω₁ : Ordinal.{v}) =
      ⋃ i < (ω₁ : Ordinal.{v}), generateMeasurableRec s i

Proof state:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ t ∈ ⋃ i, ⋃ (_ : i < ω_ 1), generateMeasurableRec s i

Tactic:
rw [mem_iUnion₂]

Result:
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i
-- Mathlib/Algebra/Polynomial/Div.lean
theorem rootMultiplicity_C (r a : R) : rootMultiplicity a (C r) = 0

Proof state:
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
⊢ (C r).natDegree < (X - C a).natDegree

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a (C r) = 0

Tactic:
rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
r a : R
⊢ rootMultiplicity a (C r) = 0

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a (C r) = 0

case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ rootMultiplicity a (C r) = 0

Proof state:
case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
⊢ multiplicity (X - C a) (C r) = 0

Tactic:
have h : natDegree (C r) < natDegree (X - C a) := by simp

Result:
case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
h : (C r).natDegree < (X - C a).natDegree
⊢ multiplicity (X - C a) (C r) = 0

Proof state:
case pos
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : C r = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ (if C r = 0 then 0 else multiplicity (X - C a) (C r)) = 0

Tactic:
split_ifs with hr

Result:
case pos
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : C r = 0
⊢ 0 = 0

case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
⊢ multiplicity (X - C a) (C r) = 0

Proof state:
case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
h : (C r).natDegree < (X - C a).natDegree
⊢ multiplicity (X - C a) (C r) = 0

Tactic:
simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ rootMultiplicity a (C r) = 0

Tactic:
rw [rootMultiplicity_eq_multiplicity]

Result:
case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ (if C r = 0 then 0 else multiplicity (X - C a) (C r)) = 0
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_re_eq_norm (x : E) : re ⟪x, x⟫ = ‖⟪x, x⟫‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫_𝕜 = ‖↑(re ⟪x, x⟫_𝕜)‖

Tactic:
symm

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ‖↑(re ⟪x, x⟫_𝕜)‖ = re ⟪x, x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ‖↑(re ⟪x, x⟫_𝕜)‖ = re ⟪x, x⟫_𝕜

Tactic:
exact norm_of_nonneg inner_self_nonneg

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫_𝕜 = ‖⟪x, x⟫_𝕜‖

Tactic:
conv_rhs => rw [← inner_self_ofReal_re]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫_𝕜 = ‖↑(re ⟪x, x⟫_𝕜)‖
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma LSeriesHasSum_congr {f g : ℕ → ℂ} (s a : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
    LSeriesHasSum f s a ↔ LSeriesHasSum g s a

Proof state:
f g : ℕ → ℂ
s a : ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
⊢ LSeriesHasSum f s a ↔ LSeriesHasSum g s a

Tactic:
simp [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr s h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem cauchySeq_tendsto_of_isComplete [Preorder β] {K : Set α} (h₁ : IsComplete K)
    {u : β → α} (h₂ : ∀ n, u n ∈ K) (h₃ : CauchySeq u) : ∃ v ∈ K, Tendsto u atTop (𝓝 v) :=
  h₁ _ h₃ <| le_principal_iff.2 <| mem_map_iff_exists_image.2
    ⟨univ, univ_mem, by rwa [image_univ, range_subset_iff]⟩

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ u '' univ ⊆ K

Tactic:
rwa [image_univ, range_subset_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean
theorem ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' (hm : m ≤ m0) [SigmaFinite (μ.trim hm)]
    {f g : α → F'} (hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn f s μ)
    (hg_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn g s μ)
    (hfg_eq : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ)
    (hfm : AEStronglyMeasurable[m] f μ) (hgm : AEStronglyMeasurable[m] g μ) : f =ᵐ[μ] g

Proof state:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : (μ.trim hm) s < ⊤
⊢ IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)

Tactic:
rw [trim_measurableSet_eq hm hs] at hμs

Result:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma image_coe_edgeSet_coe (G' : G.Subgraph) : Sym2.map (↑) '' G'.coe.edgeSet = G'.edgeSet

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)

Tactic:
rintro e he

Result:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
⊢ e ∈ Set.range (Sym2.map Subtype.val)

Proof state:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : s(a, b) ∈ G'.edgeSet
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)

Tactic:
rw [Subgraph.mem_edgeSet] at he

Result:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)

Proof state:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
a b : V
he : G'.Adj a b
⊢ s(a, b) ∈ Set.range (Sym2.map Subtype.val)

Tactic:
exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_pair_eq ..⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
he : e ∈ G'.edgeSet
⊢ e ∈ Set.range (Sym2.map Subtype.val)

Tactic:
induction e using Sym2.ind with | h a b =>
rw [Subgraph.mem_edgeSet] at he
exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_pair_eq ..⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet

Tactic:
rw [edgeSet_coe, Set.image_preimage_eq_iff]

Result:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.edgeSet ⊆ Set.range (Sym2.map Subtype.val)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem append_eq_appendTR : @List.append = @appendTR

Proof state:
case h.h
α : Type u_1
as : List α
⊢ as.append = as.appendTR

Tactic:
apply funext

Result:
case h.h.h
α : Type u_1
as : List α
⊢ ∀ (x : List α), as.append x = as.appendTR x

Proof state:
case h.h.h
α : Type u_1
as bs : List α
⊢ as.append bs = (as.reverseAux nil).reverseAux bs

Tactic:
induction as with
| nil  => rfl
| cons a as ih =>
  rw [reverseAux, reverseAux_reverseAux]
  simp [List.append, ih, reverseAux]

Result:
no goals

Proof state:
case h.h
α : Type u_1
⊢ ∀ (x : List α), x.append = x.appendTR

Tactic:
intro as

Result:
case h.h
α : Type u_1
as : List α
⊢ as.append = as.appendTR

Proof state:
case h.h.h.nil
α : Type u_1
bs : List α
⊢ nil.append bs = (nil.reverseAux nil).reverseAux bs

Tactic:
rfl

Result:
no goals

Proof state:
⊢ @List.append = @appendTR

Tactic:
apply funext

Result:
case h

⊢ ∀ (x : Type u_1), List.append = appendTR

Proof state:
case h
α : Type u_1
⊢ List.append = appendTR

Tactic:
apply funext

Result:
case h.h
α : Type u_1
⊢ ∀ (x : List α), x.append = x.appendTR

Proof state:
case h.h.h.cons
α : Type u_1
bs : List α
a : α
as : List α
ih : as.append bs = (as.reverseAux nil).reverseAux bs
⊢ (a :: as).append bs = ((a :: as).reverseAux nil).reverseAux bs

Tactic:
rw [reverseAux, reverseAux_reverseAux]

Result:
case h.h.h.cons
α : Type u_1
bs : List α
a : α
as : List α
ih : as.append bs = (as.reverseAux nil).reverseAux bs
⊢ (a :: as).append bs = (a :: nil).reverseAux ((as.reverseAux nil).reverseAux bs)

Proof state:
case h

⊢ ∀ (x : Type u_1), List.append = appendTR

Tactic:
intro α

Result:
case h
α : Type u_1
⊢ List.append = appendTR

Proof state:
case h.h.h
α : Type u_1
as bs : List α
⊢ as.append bs = as.appendTR bs

Tactic:
simp [appendTR, reverse]

Result:
case h.h.h
α : Type u_1
as bs : List α
⊢ as.append bs = (as.reverseAux nil).reverseAux bs

Proof state:
case h.h.h.cons
α : Type u_1
bs : List α
a : α
as : List α
ih : as.append bs = (as.reverseAux nil).reverseAux bs
⊢ (a :: as).append bs = (a :: nil).reverseAux ((as.reverseAux nil).reverseAux bs)

Tactic:
simp [List.append, ih, reverseAux]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
as : List α
⊢ ∀ (x : List α), as.append x = as.appendTR x

Tactic:
intro bs

Result:
case h.h.h
α : Type u_1
as bs : List α
⊢ as.append bs = as.appendTR bs
-- Mathlib/Algebra/Module/Basic.lean
theorem map_inv_natCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*)
    [DivisionSemiring R] [DivisionSemiring S] [Module R M]
    [Module S M₂] (n : ℕ) (x : M) : f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x

Proof state:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), f y = 0

Tactic:
intro x

Result:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ f x = 0

Proof state:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ (↑n)⁻¹ • f (↑n • x) = 0

Tactic:
simp [hR, map_zero f]

Result:
no goals

Proof state:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), f y = 0

Tactic:
clear x

Result:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), f y = 0

Proof state:
case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
suffices ∀ y, f y = 0 by simp [this]

Result:
case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), f y = 0
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
lemma inv_mulVec_eq_vec {A : Matrix n n α} [Invertible A]
    {u v : n → α} (hM : u = A.mulVec v) : A⁻¹.mulVec u = v

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
u v : n → α
hM : u = A *ᵥ v
⊢ A⁻¹ *ᵥ u = v

Tactic:
rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]

Result:
no goals
-- Mathlib/RingTheory/EisensteinCriterion.lean
theorem isUnit_of_natDegree_eq_zero_of_isPrimitive {p q : R[X]}
    -- Porting note: stated using `IsPrimitive` which is defeq to old statement.
    (hu : IsPrimitive (p * q)) (hpm : p.natDegree = 0) : IsUnit p

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : (p * q).IsPrimitive
hpm : p.natDegree = 0
⊢ p ∣ p * q

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : (p * q).IsPrimitive
hpm : p.natDegree = 0
⊢ IsUnit p

Tactic:
rw [eq_C_of_degree_le_zero (natDegree_eq_zero_iff_degree_le_zero.1 hpm), isUnit_C]

Result:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : (p * q).IsPrimitive
hpm : p.natDegree = 0
⊢ IsUnit (p.coeff 0)

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : (p * q).IsPrimitive
hpm : p.natDegree = 0
⊢ C (p.coeff 0) ∣ p * q

Tactic:
rw [← eq_C_of_degree_le_zero (natDegree_eq_zero_iff_degree_le_zero.1 hpm)]

Result:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : (p * q).IsPrimitive
hpm : p.natDegree = 0
⊢ p ∣ p * q

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : (p * q).IsPrimitive
hpm : p.natDegree = 0
⊢ IsUnit (p.coeff 0)

Tactic:
refine hu _ ?_

Result:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : (p * q).IsPrimitive
hpm : p.natDegree = 0
⊢ C (p.coeff 0) ∣ p * q
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem lt_mul_iff_one_lt_left' [MulRightStrictMono α]
    [MulRightReflectLT α] (a : α) {b : α} : a < b * a ↔ 1 < b :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_iff_right a)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a < b * a ↔ 1 * a < b * a

Tactic:
rw [one_mul]

Result:
no goals