harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_splits_mul' {f g : K[X]} (hfg : (f * g).map i ≠ 0) (h : Splits i (f * g)) :
    Splits i f ∧ Splits i g :=
  ⟨Or.inr @fun g hgi hg =>
      Or.resolve_left h hfg hgi (by rw [Polynomial.map_mul]; exact hg.trans (dvd_mul_right _ _)),
    Or.inr @fun g hgi hg =>
      Or.resolve_left h hfg hgi (by rw [Polynomial.map_mul]; exact hg.trans (dvd_mul_left _ _))⟩

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i f * map i g✝

Tactic:
exact hg.trans (dvd_mul_right _ _)

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i f * map i g✝

Tactic:
exact hg.trans (dvd_mul_left _ _)

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i (f * g✝)

Tactic:
rw [Polynomial.map_mul]

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i f * map i g✝

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i (f * g✝)

Tactic:
rw [Polynomial.map_mul]

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i f * map i g✝
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)]
lemma monovaryOn_inv_left : MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s

Tactic:
simp [MonovaryOn, AntivaryOn]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem SurjOn.inter_inter (h₁ : SurjOn f s₁ t₁) (h₂ : SurjOn f s₂ t₂) (h : InjOn f (s₁ ∪ s₂)) :
    SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
hx₂ : x₁ ∈ s₂
heq : f x₁ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
exact mem_image_of_mem f ⟨hx₁, hx₂⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
hx₂ : x₁ ∈ s₂
heq : f x₁ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
hy : y ∈ t₁ ∩ t₂
⊢ y ∈ f '' (s₁ ∩ s₂)

Tactic:
rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
intro y hy

Result:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
hy : y ∈ t₁ ∩ t₂
⊢ y ∈ f '' (s₁ ∩ s₂)
-- Mathlib/Data/DFinsupp/Defs.lean
theorem zipWith_def {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
    [dec : DecidableEq ι] [∀ i : ι, Zero (β i)] [∀ i : ι, Zero (β₁ i)] [∀ i : ι, Zero (β₂ i)]
    [∀ (i : ι) (x : β₁ i), Decidable (x ≠ 0)] [∀ (i : ι) (x : β₂ i), Decidable (x ≠ 0)]
    {f : ∀ i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :
    zipWith f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) fun i => f i.1 (g₁ i.1) (g₂ i.1)

Proof state:
case h
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
i : ι
⊢ (zipWith f hf g₁ g₂) i = (mk (g₁.support ∪ g₂.support) fun i => f (↑i) (g₁ ↑i) (g₂ ↑i)) i

Tactic:
by_cases h1 : g₁ i ≠ 0 <;> by_cases h2 : g₂ i ≠ 0 <;> simp only [not_not, Ne] at h1 h2 <;>
  simp [h1, h2, hf]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
⊢ zipWith f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) fun i => f (↑i) (g₁ ↑i) (g₂ ↑i)

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
i : ι
⊢ (zipWith f hf g₁ g₂) i = (mk (g₁.support ∪ g₂.support) fun i => f (↑i) (g₁ ↑i) (g₂ ↑i)) i
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem ω_pow_eq_one (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :
    (ω : X (q (p' + 2))) ^ 2 ^ (p' + 2) = 1 :=
  calc
    (ω : X (q (p' + 2))) ^ 2 ^ (p' + 2) = (ω ^ 2 ^ (p' + 1)) ^ 2

Proof state:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 2) = (ω ^ 2 ^ (p' + 1)) ^ 2

Tactic:
rw [← pow_mul, ← Nat.pow_succ]

Result:
no goals

Proof state:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (-1) ^ 2 = 1

Tactic:
simp

Result:
no goals

Proof state:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (ω ^ 2 ^ (p' + 1)) ^ 2 = (-1) ^ 2

Tactic:
rw [ω_pow_eq_neg_one p' h]

Result:
no goals
-- Mathlib/Order/Zorn.lean
theorem zorn_le_nonempty_Ici₀ (a : α)
    (ih : ∀ c ⊆ Ici a, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub) (x : α) (hax : a ≤ x) :
    ∃ m, x ≤ m ∧ IsMax m

Proof state:
case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
have ⟨ub, hub⟩ := ih c hca hc y hy

Result:
case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
ub : α
hub : ∀ z ∈ c, z ≤ ub
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Proof state:
case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
ub : α
hub : ∀ z ∈ c, z ≤ ub
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨ub, (hca hy).trans (hub y hy), hub⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
⊢ ∃ m, x ≤ m ∧ IsMax m

Tactic:
let ⟨m, hxm, ham, hm⟩ := zorn_le_nonempty₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax

Result:
case refine_2
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun x => x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun x => x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ m, x ≤ m ∧ IsMax m

case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub

Proof state:
case refine_2
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun x => x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun x => x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ m, x ≤ m ∧ IsMax m

Tactic:
exact ⟨m, hxm, fun z hmz => hm (ham.trans hmz) hmz⟩

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma MorphismProperty.RightFraction.map_eq_iff
    {X Y : C} (φ ψ : W.RightFraction X Y) :
    φ.map L (Localization.inverts _ _) = ψ.map L (Localization.inverts _ _) ↔
      RightFractionRel φ ψ

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ → (φ.map L ⋯).op = (ψ.map L ⋯).op

Tactic:
apply Quiver.Hom.unop_inj

Result:
no goals

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ (φ.map L ⋯).op = (ψ.map L ⋯).op → φ.map L ⋯ = ψ.map L ⋯

Tactic:
apply Quiver.Hom.op_inj

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ (φ.map L ⋯).op = (ψ.map L ⋯).op

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ → (φ.map L ⋯).op = (ψ.map L ⋯).op

case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ (φ.map L ⋯).op = (ψ.map L ⋯).op → φ.map L ⋯ = ψ.map L ⋯

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ RightFractionRel φ ψ

Tactic:
rw [← leftFractionRel_op_iff, ← LeftFraction.map_eq_iff L.op W.op φ.op ψ.op,
  ← φ.op_map L (Localization.inverts _ _), ← ψ.op_map L (Localization.inverts _ _)]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ (φ.map L ⋯).op = (ψ.map L ⋯).op
-- Mathlib/Data/Real/EReal.lean
theorem coe_ennreal_pos {x : ℝ≥0∞} : (0 : EReal) < x ↔ 0 < x

Proof state:
x : ℝ≥0∞
⊢ 0 < ↑x ↔ 0 < x

Tactic:
rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem size_ofArray_fold_fn {n : Nat} (assignments : Array Assignment)
    (cOpt : Option (DefaultClause n)) :
    (ofArray_fold_fn assignments cOpt).size = assignments.size

Proof state:
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size

Tactic:
split <;> simp [Array.size_modify]

Result:
no goals

Proof state:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (match cOpt with
      | none => assignments
      | some c =>
        match c.isUnit with
        | none => assignments
        | some (l, true) => assignments.modify l.val addPosAssignment
        | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size

Tactic:
split

Result:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size

case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size

Proof state:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (ofArray_fold_fn assignments cOpt).size = assignments.size

Tactic:
rw [ofArray_fold_fn.eq_def]

Result:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (match cOpt with
      | none => assignments
      | some c =>
        match c.isUnit with
        | none => assignments
        | some (l, true) => assignments.modify l.val addPosAssignment
        | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem hasNext : ∀ {it}, ValidFor l r it → (it.hasNext ↔ r ≠ [])
  | it, h => by simp [Iterator.hasNext, ← h.atEnd, Iterator.atEnd]

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.hasNext = true ↔ r ≠ []

Tactic:
simp [Iterator.hasNext, ← h.atEnd, Iterator.atEnd]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Units.lean
lemma degree_pos_of_not_isUnit_of_dvd_monic (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < degree a

Proof state:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : a ∣ p
h : a.degree ≤ 0
⊢ IsUnit a

Tactic:
rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢

Result:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (C (a.coeff 0))

Proof state:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (C (a.coeff 0))

Tactic:
simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
ha : ¬IsUnit a
hap : a ∣ p
⊢ 0 < a.degree

Tactic:
contrapose! ha with h

Result:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : a ∣ p
h : a.degree ≤ 0
⊢ IsUnit a
-- Mathlib/Probability/Kernel/Condexp.lean
theorem measurable_condExpKernel {s : Set Ω} (hs : MeasurableSet s) :
    Measurable[m] fun ω => condExpKernel μ m ω s

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Measurable fun ω => ((condExpKernel μ m) ω) s

Tactic:
simp_rw [condExpKernel_apply_eq_condDistrib]

Result:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Measurable fun ω => ((condDistrib id id μ) (id ω)) s

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Measurable fun ω => ((condDistrib id id μ) (id ω)) s

Tactic:
convert measurable_condDistrib (μ := μ) hs

Result:
case h.e'_3
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ m ⊓ mΩ = MeasurableSpace.comap id (m ⊓ mΩ)

Proof state:
case h.e'_3
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ m ⊓ mΩ = MeasurableSpace.comap id (m ⊓ mΩ)

Tactic:
rw [MeasurableSpace.comap_id]

Result:
no goals

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ((condExpKernel μ m) ω) s

Tactic:
nontriviality Ω

Result:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Measurable fun ω => ((condExpKernel μ m) ω) s
-- Mathlib/Logic/Encodable/Basic.lean
theorem sequence_mono_nat {r : β → β → Prop} {f : α → β} (hf : Directed r f) (n : ℕ) :
    r (f (hf.sequence f n)) (f (hf.sequence f (n + 1)))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n))
    (f
      (match decode n with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Tactic:
generalize hf.sequence f n = p

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match decode n with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Proof state:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match none with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Tactic:
exact (Classical.choose_spec (hf p p)).1

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Tactic:
exact (Classical.choose_spec (hf p a)).1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match decode n with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Tactic:
rcases (decode n : Option α) with - | a

Result:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match none with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))

Tactic:
dsimp [Directed.sequence]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n))
    (f
      (match decode n with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem integrable_pair {f : α →ₛ E} {g : α →ₛ F} :
    Integrable f μ → Integrable g μ → Integrable (pair f g) μ

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
f : α →ₛ E
g : α →ₛ F
⊢ Integrable (⇑f) μ → Integrable (⇑g) μ → Integrable (⇑(f.pair g)) μ

Tactic:
simpa only [integrable_iff_finMeasSupp] using FinMeasSupp.pair

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.triorthogonal_eq_orthogonal [CompleteSpace E] : Kᗮᗮᗮ = Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮ.topologicalClosure = Kᗮ

Tactic:
exact K.isClosed_orthogonal.submodule_topologicalClosure_eq

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮᗮ = Kᗮ

Tactic:
rw [Kᗮ.orthogonal_orthogonal_eq_closure]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮ.topologicalClosure = Kᗮ
-- Mathlib/RepresentationTheory/Maschke.lean
theorem exists_isCompl (p : Submodule (MonoidAlgebra k G) V) :
    ∃ q : Submodule (MonoidAlgebra k G) V, IsCompl p q

Proof state:
case intro
k : Type u
inst✝⁵ : Field k
G : Type u
inst✝⁴ : Fintype G
inst✝³ : NeZero ↑(Fintype.card G)
inst✝² : Group G
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module (MonoidAlgebra k G) V
p : Submodule (MonoidAlgebra k G) V
f : V →ₗ[MonoidAlgebra k G] ↥p
hf : f ∘ₗ p.subtype = LinearMap.id
⊢ ∃ q, IsCompl p q

Tactic:
exact ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| DFunLike.congr_fun hf⟩

Result:
no goals

Proof state:
k : Type u
inst✝⁵ : Field k
G : Type u
inst✝⁴ : Fintype G
inst✝³ : NeZero ↑(Fintype.card G)
inst✝² : Group G
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module (MonoidAlgebra k G) V
p : Submodule (MonoidAlgebra k G) V
⊢ ∃ q, IsCompl p q

Tactic:
rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩

Result:
case intro
k : Type u
inst✝⁵ : Field k
G : Type u
inst✝⁴ : Fintype G
inst✝³ : NeZero ↑(Fintype.card G)
inst✝² : Group G
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module (MonoidAlgebra k G) V
p : Submodule (MonoidAlgebra k G) V
f : V →ₗ[MonoidAlgebra k G] ↥p
hf : f ∘ₗ p.subtype = LinearMap.id
⊢ ∃ q, IsCompl p q