harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem fillNones_eq_fillNonesTR : @fillNones = @fillNonesTR

Proof state:
⊢ @fillNones = @fillNonesTR

Tactic:
funext α as as'

Result:
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ as.fillNones as' = as.fillNonesTR as'

Proof state:
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ as.fillNones as' = fillNonesTR.go as as' #[]

Tactic:
simp [fillNonesTR, go]

Result:
no goals

Proof state:
α : Type u_1
as✝ : List (Option α)
as' : List α
acc : Array α
as : List (Option α)
⊢ fillNonesTR.go (none :: as) [] acc = acc.toList ++ (none :: as).fillNones []

Tactic:
simp [fillNonesTR.go, reduceOption, filterMap_eq_filterMapTR.go]

Result:
no goals

Proof state:
α : Type u_1
as✝ : List (Option α)
as'✝ : List α
acc : Array α
as : List (Option α)
a : α
as' : List α
⊢ fillNonesTR.go (none :: as) (a :: as') acc = acc.toList ++ (none :: as).fillNones (a :: as')

Tactic:
simp [fillNonesTR.go, go _ as as']

Result:
no goals

Proof state:
α : Type u_1
as : List (Option α)
as' : List α
acc : Array α
x✝ : List α
⊢ fillNonesTR.go [] x✝ acc = acc.toList ++ [].fillNones x✝

Tactic:
simp [fillNonesTR.go]

Result:
no goals

Proof state:
α : Type u_1
as✝ : List (Option α)
as'✝ : List α
acc : Array α
a : α
as : List (Option α)
as' : List α
⊢ fillNonesTR.go (some a :: as) as' acc = acc.toList ++ (some a :: as).fillNones as'

Tactic:
simp [fillNonesTR.go, go _ as as']

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ as.fillNones as' = as.fillNonesTR as'

Tactic:
simp [fillNonesTR]

Result:
case h.h.h
α : Type u_1
as : List (Option α)
as' : List α
⊢ as.fillNones as' = fillNonesTR.go as as' #[]
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma rTensor_reflects_triviality
    [FaithfullyFlat R M] (N : Type*) [AddCommGroup N] [Module R N]
    [h : Subsingleton (N ⊗[R] M)] : Subsingleton N

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
contrapose

Result:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Tactic:
revert h

Result:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ∀ [h : Subsingleton (N ⊗[R] M)], Subsingleton N

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ∀ [h : Subsingleton (N ⊗[R] M)], Subsingleton N

Tactic:
change _ → _

Result:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Subsingleton (N ⊗[R] M) → Subsingleton N

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : Nontrivial N
⊢ Nontrivial (N ⊗[R] M)

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)

Tactic:
simp only [not_subsingleton_iff_nontrivial]

Result:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Nontrivial N → Nontrivial (N ⊗[R] M)

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Nontrivial N → Nontrivial (N ⊗[R] M)

Tactic:
intro h

Result:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : Nontrivial N
⊢ Nontrivial (N ⊗[R] M)
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem fst_eq_of_dist_lt_one (x y : Σi, E i) (h : dist x y < 1) : x.1 = y.1

Proof state:
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : ⟨fst✝¹, snd✝¹⟩.fst ≠ ⟨fst✝, snd✝⟩.fst
⊢ 1 ≤ dist ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩

Tactic:
apply one_le_dist_of_ne h

Result:
no goals

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
x y : (i : ι) × E i
h : dist x y < 1
⊢ x.fst = y.fst

Tactic:
cases x

Result:
case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y : (i : ι) × E i
fst✝ : ι
snd✝ : E fst✝
h : dist ⟨fst✝, snd✝⟩ y < 1
⊢ ⟨fst✝, snd✝⟩.fst = y.fst

Proof state:
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : dist ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩ < 1
⊢ ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst

Tactic:
contrapose! h

Result:
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : ⟨fst✝¹, snd✝¹⟩.fst ≠ ⟨fst✝, snd✝⟩.fst
⊢ 1 ≤ dist ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩

Proof state:
case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y : (i : ι) × E i
fst✝ : ι
snd✝ : E fst✝
h : dist ⟨fst✝, snd✝⟩ y < 1
⊢ ⟨fst✝, snd✝⟩.fst = y.fst

Tactic:
cases y

Result:
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : dist ⟨fst✝¹, snd✝¹⟩ ⟨fst✝, snd✝⟩ < 1
⊢ ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst
-- Mathlib/RingTheory/Spectrum/Prime/Module.lean
lemma Module.support_subset_preimage_comap [IsScalarTower R A M] :
    Module.support A M ⊆ PrimeSpectrum.comap (algebraMap R A) ⁻¹' Module.support R M

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ support A M ⊆ ⇑(PrimeSpectrum.comap (algebraMap R A)) ⁻¹' support R M

Tactic:
intro x hx

Result:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
hx : x ∈ support A M
⊢ x ∈ ⇑(PrimeSpectrum.comap (algebraMap R A)) ⁻¹' support R M

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
hx : ∃ m, ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ m, ∀ (r : R), r • m = 0 → (algebraMap R A) r ∈ x.asIdeal

Tactic:
obtain ⟨m, hm⟩ := hx

Result:
case intro
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ m, ∀ (r : R), r • m = 0 → (algebraMap R A) r ∈ x.asIdeal

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
hx : x ∈ support A M
⊢ x ∈ ⇑(PrimeSpectrum.comap (algebraMap R A)) ⁻¹' support R M

Tactic:
simp only [Set.mem_preimage, mem_support_iff', PrimeSpectrum.comap_asIdeal, Ideal.mem_comap,
  ne_eq, not_imp_not] at hx ⊢

Result:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
hx : ∃ m, ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ m, ∀ (r : R), r • m = 0 → (algebraMap R A) r ∈ x.asIdeal

Proof state:
case intro
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ m, ∀ (r : R), r • m = 0 → (algebraMap R A) r ∈ x.asIdeal

Tactic:
exact ⟨m, fun r e ↦ hm _ (by simpa)⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
r : R
e : r • m = 0
⊢ (algebraMap R A) r • m = 0

Tactic:
simpa

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- The intersection of two blocks is a block. -/
@[to_additive "The intersection of two blocks is a block."]
lemma IsBlock.inter {B₁ B₂ : Set X} (h₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) :
    IsBlock G (B₁ ∩ B₂)

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
⊢ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₁ • B₂ ∩ (g₂ • B₁ ∩ g₂ • B₂)).Nonempty → g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂

Tactic:
rintro g₁ g₂ ⟨a, ha₁, ha₂⟩

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
g₁ g₂ : G
a : X
ha₁ : a ∈ g₁ • B₁ ∩ g₁ • B₂
ha₂ : a ∈ g₂ • B₁ ∩ g₂ • B₂
⊢ g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
g₁ g₂ : G
a : X
ha₁ : a ∈ g₁ • B₁ ∩ g₁ • B₂
ha₂ : a ∈ g₂ • B₁ ∩ g₂ • B₂
⊢ g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂

Tactic:
rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
⊢ IsBlock G (B₁ ∩ B₂)

Tactic:
simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
⊢ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₁ • B₂ ∩ (g₂ • B₁ ∩ g₂ • B₂)).Nonempty → g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
-- Mathlib/Data/Seq/Seq.lean
theorem get?_zero_eq_none {s : Seq α} : s.get? 0 = none ↔ s = nil

Proof state:
α : Type u
s : Seq α
h : s.get? 0 = none
⊢ s = nil

Tactic:
ext1 n

Result:
case h
α : Type u
s : Seq α
h : s.get? 0 = none
n : ℕ
⊢ s.get? n = nil.get? n

Proof state:
case h
α : Type u
s : Seq α
h : s.get? 0 = none
n : ℕ
⊢ s.get? n = nil.get? n

Tactic:
exact le_stable s (Nat.zero_le _) h

Result:
no goals

Proof state:
α : Type u
s : Seq α
⊢ s.get? 0 = none ↔ s = nil

Tactic:
refine ⟨fun h => ?_, fun h => h ▸ rfl⟩

Result:
α : Type u
s : Seq α
h : s.get? 0 = none
⊢ s = nil
-- Mathlib/NumberTheory/MulChar/Basic.lean
/-- A multiplicative character on a commutative monoid with finitely many units
has finite (= positive) order. -/
lemma orderOf_pos [Finite Mˣ] (χ : MulChar M R) : 0 < orderOf χ

Proof state:
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
⊢ 0 < orderOf χ

Tactic:
cases nonempty_fintype Mˣ

Result:
case intro
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
val✝ : Fintype Mˣ
⊢ 0 < orderOf χ

Proof state:
case intro
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
val✝ : Fintype Mˣ
⊢ 0 < orderOf χ

Tactic:
apply IsOfFinOrder.orderOf_pos

Result:
case intro.h
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
val✝ : Fintype Mˣ
⊢ IsOfFinOrder χ

Proof state:
case intro.h
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
val✝ : Fintype Mˣ
⊢ IsOfFinOrder χ

Tactic:
exact isOfFinOrder_iff_pow_eq_one.2 ⟨_, Fintype.card_pos, χ.pow_card_eq_one⟩

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma associator_inv_fst_snd (X Y Z : C) :
    (α_ X Y Z).inv ≫ fst _ _ ≫ snd _ _ = snd _ _ ≫ fst _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ fst (X ⊗ Y) Z ≫ snd X Y = snd X (Y ⊗ Z) ≫ fst Y Z

Tactic:
erw [lift_fst_assoc, lift_snd]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.snd (product X (product Y Z).cone.pt).cone ≫ Limits.BinaryFan.fst (product Y Z).cone =
    snd X (Y ⊗ Z) ≫ fst Y Z

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.snd (product X (product Y Z).cone.pt).cone ≫ Limits.BinaryFan.fst (product Y Z).cone =
    snd X (Y ⊗ Z) ≫ fst Y Z

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_abs (x : ℝ) : logb b |x| = logb b x

Proof state:
b x : ℝ
⊢ logb b |x| = logb b x

Tactic:
rw [logb, logb, log_abs]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_one_eq_self_iff_eq_replicate [Nonempty α] {l : List α} :
    l.rotate 1 = l ↔ ∃ a : α, l = List.replicate l.length a :=
  ⟨fun h =>
    rotate_eq_self_iff_eq_replicate.mp fun n =>
      Nat.rec l.rotate_zero (fun n hn => by rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]) n,
    fun h => rotate_eq_self_iff_eq_replicate.mpr h 1⟩

Proof state:
α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate n.succ = l

Tactic:
rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem rank_le_one_of_commute_of_flat_of_self (H : M.LinearDisjoint M) [Module.Flat R M]
    (hc : ∀ (m n : M), Commute m.1 n.1) : Module.rank R M ≤ 1

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst✝ : Module.Flat R ↥M
hc : ∀ (m n : ↥M), Commute ↑m ↑n
⊢ Module.rank R ↥M ≤ 1

Tactic:
rw [← inf_of_le_left (le_refl M)] at hc ⊢

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst✝ : Module.Flat R ↥M
hc : ∀ (m n : ↥(M ⊓ M)), Commute ↑m ↑n
⊢ Module.rank R ↥(M ⊓ M) ≤ 1

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M : Submodule R S
H : M.LinearDisjoint M
inst✝ : Module.Flat R ↥M
hc : ∀ (m n : ↥(M ⊓ M)), Commute ↑m ↑n
⊢ Module.rank R ↥(M ⊓ M) ≤ 1

Tactic:
exact H.rank_inf_le_one_of_commute_of_flat_left hc

Result:
no goals
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem mul_nonpos {α} [OrderedRing α] {a b : α} (ha : a ≤ 0) (hb : 0 < b) : b * a ≤ 0 :=
  have : (-b)*a ≥ 0 := mul_nonneg_of_nonpos_of_nonpos (le_of_lt (neg_neg_of_pos hb)) ha
  by simpa

Proof state:
α : Type u_1
inst✝ : OrderedRing α
a b : α
ha : a ≤ 0
hb : 0 < b
this : -b * a ≥ 0
⊢ b * a ≤ 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma natDegree_eq_of_natDegree_add_lt_left (p q : R[X])
    (H : natDegree (p + q) < natDegree p) : natDegree p = natDegree q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h : ¬p.natDegree = q.natDegree
⊢ False

Tactic:
cases Nat.lt_or_lt_of_ne h with
| inl h => exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)
| inr h =>
  rw [natDegree_add_eq_left_of_natDegree_lt h] at H
  exact LT.lt.false H

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
⊢ False

Tactic:
exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)

Result:
no goals

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
H : p.natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ False

Tactic:
exact LT.lt.false H

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
⊢ q.natDegree < p.natDegree

Tactic:
rwa [natDegree_add_eq_right_of_natDegree_lt h] at H

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
by_contra h

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h : ¬p.natDegree = q.natDegree
⊢ False

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ False

Tactic:
rw [natDegree_add_eq_left_of_natDegree_lt h] at H

Result:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
H : p.natDegree < p.natDegree
h✝ : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ False
-- Mathlib/Algebra/Tropical/Basic.lean
theorem add_eq_right_iff {x y : Tropical R} : x + y = y ↔ y ≤ x

Proof state:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = y ↔ y ≤ x

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem offDiag_univ : (univ : Set α).offDiag = (diagonal α)ᶜ :=
  ext <| by simp

Proof state:
α : Type u_1
⊢ ∀ (x : α × α), x ∈ univ.offDiag ↔ x ∈ (diagonal α)ᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_sq_add_areaForm_sq (a b : E) : ⟪a, b⟫ ^ 2 + ω a b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a b : E
⊢ inner a b ^ 2 + (o.areaForm a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2

Tactic:
simpa [sq, real_inner_self_eq_norm_sq] using o.inner_mul_inner_add_areaForm_mul_areaForm a b b

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_multiset_prod [DecidableEq ι] [Fintype ι] {u : Multiset ι} {x : ι → 𝔸'} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (u.map x).prod)
      (u.map (fun i ↦ ((u.erase i).map x).prod • proj i)).sum x :=
  u.inductionOn fun l ↦ by simpa using hasStrictFDerivAt_list_prod

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
u : Multiset ι
x : ι → 𝔸'
l : List ι
⊢ HasStrictFDerivAt (fun x => (Multiset.map x ⟦l⟧).prod)
    (Multiset.map (fun i => (Multiset.map x (Multiset.erase ⟦l⟧ i)).prod • proj i) ⟦l⟧).sum x

Tactic:
simpa using hasStrictFDerivAt_list_prod

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem size_pop (a : Array α) : a.pop.size = a.size - 1

Proof state:
α : Type u
a : Array α
⊢ { toList := List.nil }.pop.size = { toList := List.nil }.size - 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a : Array α
⊢ a.pop.size = a.size - 1

Tactic:
match a with
| ⟨[]⟩ => rfl
| ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]

Result:
no goals

Proof state:
α : Type u
a✝ : Array α
a : α
as : List α
⊢ { toList := a :: as }.pop.size = { toList := a :: as }.size - 1

Tactic:
simp [pop, Nat.succ_sub_succ_eq_sub, size]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem unitization_injective (h1 : (1 : A) ∉ s) : Function.Injective (unitization s) :=
  AlgHomClass.unitization_injective s h1 (unitization s) fun _ ↦ by simp

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
x✝ : ↥s
⊢ (unitization s) ↑x✝ = ↑x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/CountableSeparatingOn.lean
theorem exists_seq_separating (α : Type*) {p : Set α → Prop} {s₀} (hp : p s₀) (t : Set α)
    [HasCountableSeparatingOn α p t] :
    ∃ S : ℕ → Set α, (∀ n, p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ n, x ∈ S n ↔ y ∈ S n) → x = y

Proof state:
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
rcases exists_nonempty_countable_separating α hp t with ⟨S, hSne, hSc, hS⟩

Result:
case intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : Set (Set α)
hSne : S.Nonempty
hSc : S.Countable
hS : (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Proof state:
case h
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
simpa only [forall_mem_range] using hS

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
use S

Result:
case h
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Proof state:
case intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : Set (Set α)
hSne : S.Nonempty
hSc : S.Countable
hS : (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y

Tactic:
rcases hSc.exists_eq_range hSne with ⟨S, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
p : Set α → Prop
s₀ : Set α
hp : p s₀
t : Set α
inst✝ : HasCountableSeparatingOn α p t
S : ℕ → Set α
hSne : (range S).Nonempty
hSc : (range S).Countable
hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem le_glueDist_inr_inl (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (x y) :
    ε ≤ glueDist Φ Ψ ε (.inr x) (.inl y)

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)

Tactic:
rw [glueDist_comm]

Result:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inl y) (Sum.inr x)

Proof state:
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inl y) (Sum.inr x)

Tactic:
apply le_glueDist_inl_inr

Result:
no goals