harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndepOn_iffₛ : LinearIndepOn R v s ↔
      ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s,
        Finsupp.linearCombination R v f = Finsupp.linearCombination R v g → f = g

Proof state:
case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype s) l₂).support, x ∈ s

case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype s) l₁).sum fun i a => a • v i) =
    (Finsupp.embDomain (Embedding.subtype s) l₂).sum fun i a => a • v i

Tactic:
simpa using fun _ h _ ↦ h

Result:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype s) l₁).sum fun i a => a • v i) =
    (Finsupp.embDomain (Embedding.subtype s) l₂).sum fun i a => a • v i
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
lemma LFunction_isBigO_horizontal {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) :
    (fun x : ℝ ↦ LFunction χ (1 + x + I * y)) =O[𝓝[>] 0] fun _ ↦ (1 : ℂ)

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (1 + I * ↑y)
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x => 1

Tactic:
rw [← zero_add (1 + _)] at this

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x => 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ ContinuousAt (fun x => ↑x + (1 + I * ↑y)) 0

Tactic:
fun_prop

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ (fun x => LFunction χ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1

Tactic:
simp_rw [add_comm (1 : ℂ), add_assoc]

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x => 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x => 1

Tactic:
exact this.comp (f := fun x : ℝ ↦ x + (1 + I * y)) (x := 0) (by fun_prop) |>.tendsto.isBigO_one ℂ

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x => 1

Tactic:
have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).continuousAt

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (1 + I * ↑y)
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x => 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ (fun x => LFunction χ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => 1

Tactic:
refine IsBigO.mono ?_ nhdsWithin_le_nhds

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ (fun x => LFunction χ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_pi [Finite η] : Module.rank R (∀ i, φ i) =
    Cardinal.sum fun i => Module.rank R (φ i)

Proof state:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i => chooseBasis R (φ i)
⊢ Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)

Tactic:
let b : Basis _ R (∀ i, φ i) := Pi.basis fun i => B i

Result:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i => chooseBasis R (φ i)
b : Basis ((j : η) × ChooseBasisIndex R (φ j)) R ((i : η) → φ i) := Pi.basis fun i => B i
⊢ Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)

Proof state:
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
⊢ Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)

Tactic:
cases nonempty_fintype η

Result:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
⊢ Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)

Proof state:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i => chooseBasis R (φ i)
b : Basis ((j : η) × ChooseBasisIndex R (φ j)) R ((i : η) → φ i) := Pi.basis fun i => B i
⊢ Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)

Tactic:
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']

Result:
no goals

Proof state:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
⊢ Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)

Tactic:
let B i := chooseBasis R (φ i)

Result:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i => chooseBasis R (φ i)
⊢ Module.rank R ((i : η) → φ i) = sum fun i => Module.rank R (φ i)
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_equiv {f g : PadicSeq p} (hfg : f ≈ g) : f.norm = g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
⊢ f.norm = g.norm

Tactic:
classical
exact if hf : f ≈ 0 then by
  have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
  simp [norm, hf, hg]
else by
  have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
  unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
⊢ f.norm = g.norm

Tactic:
exact if hf : f ≈ 0 then by
  have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
  simp [norm, hf, hg]
else by
  have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
  unfold norm; split_ifs; exact norm_eq_of_equiv hf hg hfg

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
⊢ f.norm = g.norm

Tactic:
have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.norm = g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))

Tactic:
exact norm_eq_of_equiv hf hg hfg

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
⊢ f.norm = g.norm

Tactic:
have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ f.norm = g.norm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.norm = g.norm

Tactic:
unfold norm

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) =
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) =
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))

Tactic:
split_ifs

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ f.norm = g.norm

Tactic:
simp [norm, hf, hg]

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[simp]
lemma specTensorTo_base_snd (p : Spec T.tensor) :
    (pullback.snd f g).base (T.SpecTensorTo.base p) = T.y

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom
        (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯ ≫
            pullback.snd f g).base)
      p =
    T.y

Tactic:
simp

Result:
no goals

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.snd f g).base)
      ((ConcreteCategory.hom
          (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯).base)
        p) =
    T.y

Tactic:
rw [← Scheme.comp_base_apply]

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom
        (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯ ≫
            pullback.snd f g).base)
      p =
    T.y

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.snd f g).base) ((ConcreteCategory.hom T.SpecTensorTo.base) p) = T.y

Tactic:
simp only [SpecTensorTo, residueFieldCongr_inv]

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.snd f g).base)
      ((ConcreteCategory.hom
          (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯).base)
        p) =
    T.y
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ici_diff_left : Ici a \ {a} = Ioi a :=
  ext fun x => by simp [lt_iff_le_and_ne, eq_comm]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a x : α
⊢ x ∈ Ici a \ {a} ↔ x ∈ Ioi a

Tactic:
simp [lt_iff_le_and_ne, eq_comm]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_uniqueElim [Unique δ] :
    Measurable (uniqueElim : π (default : δ) → ∀ i, π i)

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : Unique δ
⊢ Measurable uniqueElim

Tactic:
simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]

Result:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : Unique δ
⊢ Measurable fun x => x

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : Unique δ
⊢ Measurable fun x => x

Tactic:
exact measurable_id

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eqRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
        {motive : (x : α) → a = x → Sort u_1} (v : motive a (Eq.refl a)) {b : α} (h : a = b)
        : HEq (@Eq.rec α a motive v b h) v

Proof state:
α : Sort u_2
a : α
motive : (x : α) → a = x → Sort u_1
v : motive a ⋯
⊢ HEq (⋯ ▸ v) v

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_2
a : α
motive : (x : α) → a = x → Sort u_1
v : motive a ⋯
b : α
h : a = b
⊢ HEq (h ▸ v) v

Tactic:
subst h

Result:
α : Sort u_2
a : α
motive : (x : α) → a = x → Sort u_1
v : motive a ⋯
⊢ HEq (⋯ ▸ v) v
-- Mathlib/Data/Finset/Filter.lean
theorem filter_filter (s : Finset α) : (s.filter p).filter q = s.filter fun a => p a ∧ q a :=
  ext fun a => by
    simp only [mem_filter, and_assoc, Bool.decide_and, Bool.decide_coe, Bool.and_eq_true]

Proof state:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
a : α
⊢ a ∈ filter q (filter p s) ↔ a ∈ filter (fun a => p a ∧ q a) s

Tactic:
simp only [mem_filter, and_assoc, Bool.decide_and, Bool.decide_coe, Bool.and_eq_true]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma lt_self_pow₀ (h : 1 < a) (hm : 1 < m) : a < a ^ m

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
m : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
h : 1 < a
hm : 1 < m
⊢ a < a ^ m

Tactic:
simpa only [pow_one] using pow_lt_pow_right₀ h hm

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_preimage_of_injective (f : α → β) (s : Set β) (h : Injective f) :
    #(f ⁻¹' s) ≤ #s

Proof state:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ #↑(f ⁻¹' s) ≤ #↑s

Tactic:
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]

Result:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #↑(f ⁻¹' s) ≤ lift.{u, u} #↑s

Proof state:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #↑(f ⁻¹' s) ≤ lift.{u, u} #↑s

Tactic:
exact mk_preimage_of_injective_lift f s h

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
lemma add_scaleRoots_of_natDegree_eq (p q : R[X]) (r : R) (h : natDegree p = natDegree q) :
    r ^ (natDegree p - natDegree (p + q)) • (p + q).scaleRoots r =
      p.scaleRoots r + q.scaleRoots r

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n

Tactic:
simp only [coeff_smul, coeff_scaleRoots, coeff_add, smul_eq_mul,
mul_comm (r ^ _), ← pow_add, ← h, ← add_mul, add_comm (_ - n)]

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Proof state:
case a.inl
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : (p + q).natDegree < n
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
simp only [← coeff_add, coeff_eq_zero_of_natDegree_lt hn, zero_mul]

Result:
no goals

Proof state:
case a.inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : n ≤ (p + q).natDegree
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
rw [add_comm (_ - n), tsub_add_tsub_cancel (natDegree_add_le_of_degree_le le_rfl h.ge) hn]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
⊢ r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r

Tactic:
ext n

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
rw [mul_assoc, ← pow_add]

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
cases lt_or_le (natDegree (p + q)) n with
| inl hn => simp only [← coeff_add, coeff_eq_zero_of_natDegree_lt hn, zero_mul]
| inr hn =>
    rw [add_comm (_ - n), tsub_add_tsub_cancel (natDegree_add_le_of_degree_le le_rfl h.ge) hn]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_injective (n : ℕ) : Function.Injective fun l : List α => l.rotate n

Proof state:
α : Type u
n : ℕ
⊢ Injective fun l => l.rotate n

Tactic:
rintro l l' (h : l.rotate n = l'.rotate n)

Result:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
⊢ l = l'

Proof state:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
⊢ l = l'

Tactic:
have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)

Result:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
hle : l.length = l'.length
⊢ l = l'

Proof state:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
hle : l.length = l'.length
⊢ l = l'

Tactic:
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h

Result:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ l = l'

Proof state:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ l = l'

Tactic:
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)

Result:
case intro
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l = l'

Proof state:
case intro
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l = l'

Tactic:
rw [← take_append_drop _ l, ht, hd, take_append_drop]

Result:
no goals

Proof state:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ (drop (n % l.length) l).length = (drop (n % l'.length) l').length

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem isCoprime_X_sub_C_of_isUnit_sub {R} [CommRing R] {a b : R} (h : IsUnit (a - b)) :
    IsCoprime (X - C a) (X - C b) :=
  ⟨-C h.unit⁻¹.val, C h.unit⁻¹.val, by
    rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]
    rw [← C_1]
    congr
    exact h.val_inv_mul⟩

Proof state:
case h.e_6.h
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ ↑h.unit⁻¹ * (a - b) = 1

Tactic:
exact h.val_inv_mul

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = C 1

Tactic:
congr

Result:
case h.e_6.h
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ ↑h.unit⁻¹ * (a - b) = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ -C ↑h.unit⁻¹ * (X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1

Tactic:
rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]

Result:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = 1

Tactic:
rw [← C_1]

Result:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = C 1
-- Mathlib/Data/List/SplitLengths.lean
theorem take_splitLength (i : ℕ) : (sz.splitLengths l).take i = (sz.take i).splitLengths l

Proof state:
case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l

Tactic:
simp only [splitLengths_cons, take_succ_cons, cons.injEq, true_and, hi]

Result:
no goals

Proof state:
case nil
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) ([].splitLengths l) = (take (i + 1) []).splitLengths l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
⊢ take i (sz.splitLengths l) = (take i sz).splitLengths l

Tactic:
induction i generalizing sz l

Result:
case zero
α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

case succ
α : Type u_1
n✝ : ℕ
a✝ : ∀ (l : List α) (sz : List ℕ), take n✝ (sz.splitLengths l) = (take n✝ sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (n✝ + 1) (sz.splitLengths l) = (take (n✝ + 1) sz).splitLengths l

Proof state:
case zero
α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

case succ
α : Type u_1
n✝ : ℕ
a✝ : ∀ (l : List α) (sz : List ℕ), take n✝ (sz.splitLengths l) = (take n✝ sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (n✝ + 1) (sz.splitLengths l) = (take (n✝ + 1) sz).splitLengths l

Tactic:
case zero => simp

Result:
case succ
α : Type u_1
n✝ : ℕ
a✝ : ∀ (l : List α) (sz : List ℕ), take n✝ (sz.splitLengths l) = (take n✝ sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (n✝ + 1) (sz.splitLengths l) = (take (n✝ + 1) sz).splitLengths l

Proof state:
α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (i + 1) (sz.splitLengths l) = (take (i + 1) sz).splitLengths l

Tactic:
cases sz

Result:
case nil
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
⊢ take (i + 1) ([].splitLengths l) = (take (i + 1) []).splitLengths l

case cons
α : Type u_1
i : ℕ
hi : ∀ (l : List α) (sz : List ℕ), take i (sz.splitLengths l) = (take i sz).splitLengths l
l : List α
head✝ : ℕ
tail✝ : List ℕ
⊢ take (i + 1) ((head✝ :: tail✝).splitLengths l) = (take (i + 1) (head✝ :: tail✝)).splitLengths l
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem map_of_not_measurable (κ : Kernel α β) {f : β → γ} (hf : ¬(Measurable f)) :
    map κ f = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : ¬Measurable f
⊢ κ.map f = 0

Tactic:
simp [map, hf]

Result:
no goals