harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
@[simp]
lemma apply_toDual_symm_apply {B : BilinForm K V} {hB : B.Nondegenerate}
    (f : Module.Dual K V) (v : V) :
    B ((B.toDual hB).symm f) v = f v

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
f : Module.Dual K V
v : V
⊢ ((B.toDual hB) ((B.toDual hB).symm f)) v = f v

Tactic:
simp only [LinearEquiv.apply_symm_apply]

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
f : Module.Dual K V
v : V
⊢ (B ((B.toDual hB).symm f)) v = f v

Tactic:
change B.toDual hB ((B.toDual hB).symm f) v = f v

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
f : Module.Dual K V
v : V
⊢ ((B.toDual hB) ((B.toDual hB).symm f)) v = f v
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem coe_inj {q r : ℚ} : (↑q : ℚ_[p]) = ↑r ↔ q = r :=
  ⟨(const_equiv p).1 ∘ Quotient.eq'.1, fun h ↦ by rw [h]⟩

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
h : q = r
⊢ ↑q = ↑r

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/MStructure.lean
theorem Lcomplement {P : M} (h : IsLprojection X P) : IsLprojection X (1 - P) :=
  ⟨h.proj.one_sub, fun x => by
    rw [add_comm, sub_sub_cancel]
    exact h.Lnorm x⟩

Proof state:
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖(1 - P) • x‖ + ‖(1 - (1 - P)) • x‖

Tactic:
rw [add_comm, sub_sub_cancel]

Result:
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖

Proof state:
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖

Tactic:
exact h.Lnorm x

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
theorem mk_coe (f : M →ₗ⁅R,L⁆ N) (h) : (⟨f, h⟩ : M →ₗ⁅R,L⁆ N) = f

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
h : ∀ {x : L} {m : M}, (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆
⊢ { toLinearMap := ↑f, map_lie' := h } = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isOpen_setOf_disjoint_nhds_nhds : IsOpen { p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2) }

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen {p | Disjoint (𝓝 p.1) (𝓝 p.2)}

Tactic:
simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq]

Result:
X : Type u
inst✝ : TopologicalSpace X
⊢ ∀ (a b : X), Disjoint (𝓝 a) (𝓝 b) → {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (a, b)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
⊢ {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Tactic:
obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h

Result:
case intro.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
U : Set X
hU : x ∈ U ∧ IsOpen U
V : Set X
hV : y ∈ V ∧ IsOpen V
hd : Disjoint U V
⊢ {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ ∀ (a b : X), Disjoint (𝓝 a) (𝓝 b) → {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (a, b)

Tactic:
intro x y h

Result:
X : Type u
inst✝ : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
⊢ {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Proof state:
case intro.intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
U : Set X
hU : x ∈ U ∧ IsOpen U
V : Set X
hV : y ∈ V ∧ IsOpen V
hd : Disjoint U V
⊢ {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Tactic:
exact mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
  disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem append_left_le [DecidableEq α] [LT α] [DecidableLT α]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Asymm (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)]
    {l₁ l₂ l₃ : Array α} (h : l₂ ≤ l₃) :
    l₁ ++ l₂ ≤ l₁ ++ l₃

Proof state:
case mk.mk.mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
toList✝² toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } ≤ { toList := toList✝ }
⊢ { toList := toList✝² } ++ { toList := toList✝¹ } ≤ { toList := toList✝² } ++ { toList := toList✝ }

Tactic:
simpa using List.append_left_le h

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₃ : Array α
toList✝¹ toList✝ : List α
h : { toList := toList✝ } ≤ l₃
⊢ { toList := toList✝¹ } ++ { toList := toList✝ } ≤ { toList := toList✝¹ } ++ l₃

Tactic:
cases l₃

Result:
case mk.mk.mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
toList✝² toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } ≤ { toList := toList✝ }
⊢ { toList := toList✝² } ++ { toList := toList✝¹ } ≤ { toList := toList✝² } ++ { toList := toList✝ }

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₁ l₂ l₃ : Array α
h : l₂ ≤ l₃
⊢ l₁ ++ l₂ ≤ l₁ ++ l₃

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₂ l₃ : Array α
h : l₂ ≤ l₃
toList✝ : List α
⊢ { toList := toList✝ } ++ l₂ ≤ { toList := toList✝ } ++ l₃

Proof state:
case mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₂ l₃ : Array α
h : l₂ ≤ l₃
toList✝ : List α
⊢ { toList := toList✝ } ++ l₂ ≤ { toList := toList✝ } ++ l₃

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Asymm fun x1 x2 => x1 < x2
inst✝ : Std.Antisymm fun x1 x2 => ¬x1 < x2
l₃ : Array α
toList✝¹ toList✝ : List α
h : { toList := toList✝ } ≤ l₃
⊢ { toList := toList✝¹ } ++ { toList := toList✝ } ≤ { toList := toList✝¹ } ++ l₃
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma le_one_of_one_le_inv {a : Aˣ} (ha : 1 ≤ (↑a⁻¹ : A)) : (a : A) ≤ 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a⁻¹
⊢ ↑a ≤ 1

Tactic:
simpa using CStarAlgebra.inv_le_one ha

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_smul_ball (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) :
    Metric.ball (0 : 𝕜) r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Proof state:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
⊢ Metric.ball 0 r₁ • p.ball 0 0 ⊆ p.ball 0 (r₁ * 0)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
rcases eq_or_ne r₂ 0 with rfl | hr₂

Result:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
⊢ Metric.ball 0 r₁ • p.ball 0 0 ⊆ p.ball 0 (r₁ * 0)

case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Proof state:
case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ Metric.ball 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
exact (smul_subset_smul_left (ball_subset_closedBall _ _ _)).trans
  (ball_smul_closedBall _ _ hr₂)

Result:
no goals
-- Mathlib/Data/Finset/Finsupp.lean
theorem mem_finsupp_iff_of_support_subset {t : ι →₀ Finset α} (ht : t.support ⊆ s) :
    f ∈ s.finsupp t ↔ ∀ i, f i ∈ t i

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : f i ∈ t i
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0

Tactic:
rwa [H, mem_zero] at h

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
⊢ f ∈ s.finsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i

Tactic:
refine
  mem_finsupp_iff.trans
    (forall_and.symm.trans <|
      forall_congr' fun i =>
        ⟨fun h => ?_, fun h =>
          ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)

Result:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
⊢ f i ∈ t i

case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : f i ∈ t i
hi : i ∈ f.support
H : t i = 0
⊢ f i = 0

Proof state:
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ 0

Tactic:
exact zero_mem_zero

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ f i ∈ t i

Tactic:
rw [not_mem_support_iff.1 (mt h.1 hi), not_mem_support_iff.1 fun H => hi <| ht H]

Result:
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ 0 ∈ 0

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
⊢ f i ∈ t i

Tactic:
by_cases hi : i ∈ s

Result:
case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∈ s
⊢ f i ∈ t i

case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∉ s
⊢ f i ∈ t i

Proof state:
case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
hi : i ∈ s
⊢ f i ∈ t i

Tactic:
exact h.2 hi

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_mul : ghostFun (x * y) = ghostFun x * ghostFun y

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ WittVector.ghostFun (x * y) = WittVector.ghostFun x * WittVector.ghostFun y

Tactic:
ghost_fun_tac X 0 * X 1, ![x.coeff, y.coeff]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem IsStoppingTime.measurableSet_gt (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[f i] {ω | i < τ ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | i < τ ω} ↔ ω ∈ {ω | τ ω ≤ i}ᶜ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | i < τ ω}

Tactic:
have : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ := by
  ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_le]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | i < τ ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | τ ω ≤ i}ᶜ

Tactic:
exact (hτ.measurableSet_le i).compl

Result:
no goals

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | i < τ ω} ↔ ω ∈ {ω | τ ω ≤ i}ᶜ

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_le]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | i < τ ω}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | τ ω ≤ i}ᶜ
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_update_eq_erase (f : α →₀ M) (a : α) (b : M) :
    erase a (update f a b) = erase a f

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ erase a (f.update a b) = erase a f

Tactic:
rw [erase_eq_update_zero, erase_eq_update_zero, update_idem]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem cancel_left_of_respectsIso
    (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso]
    {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [IsAffine Z] : P (f ≫ g) ↔ P g

Proof state:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsAffine Z
⊢ P (f ≫ g) ↔ P g

Tactic:
rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.cancel_left_of_respectsIso]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem continuousInv_inf {t₁ t₂ : TopologicalSpace G} (h₁ : @ContinuousInv G t₁ _)
    (h₂ : @ContinuousInv G t₂ _) : @ContinuousInv G (t₁ ⊓ t₂) _

Proof state:
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
b : Bool
⊢ ContinuousInv G

Tactic:
cases b <;> assumption

Result:
no goals

Proof state:
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

Tactic:
refine continuousInv_iInf fun b => ?_

Result:
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
b : Bool
⊢ ContinuousInv G
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_undef (hX : ¬Integrable (fun ω => exp (t * X ω)) μ) : cgf X μ t = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hX : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ cgf X μ t = 0

Tactic:
simp only [cgf, mgf_undef hX, log_zero]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem HasBasis.liminf_eq_sSup_univ_of_empty {f : ι → α} {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) :
    liminf f v = sSup univ

Proof state:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝ : ConditionallyCompleteLattice α
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
i : ι'
hi : p i
h'i : s i = ∅
⊢ liminf f v = sSup univ

Tactic:
simp [hv.eq_bot_iff.2 ⟨i, hi, h'i⟩, liminf_eq]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
theorem not_two_dvd_bit1 (n : ℕ) : ¬2 ∣ 2 * n + 1

Proof state:
n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
lemma le_add_right (s t : Multiset α) : s ≤ s + t

Proof state:
α : Type u_1
s t : Multiset α
⊢ s ≤ s + t

Tactic:
simpa using Multiset.add_le_add_left (zero_le t)

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem compl_congr {π₁ π₂ : Prepartition I} (h : π₁.iUnion = π₂.iUnion) : π₁.compl = π₂.compl

Proof state:
case e_p
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ (fun π' => π'.iUnion = ↑I \ π₁.iUnion) = fun π' => π'.iUnion = ↑I \ π₂.iUnion

Tactic:
rw [h]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ ⋯.choose = ⋯.choose

Tactic:
congr 1

Result:
case e_p
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ (fun π' => π'.iUnion = ↑I \ π₁.iUnion) = fun π' => π'.iUnion = ↑I \ π₂.iUnion

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ π₁.compl = π₂.compl

Tactic:
dsimp only [compl]

Result:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ ⋯.choose = ⋯.choose
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@[simp]
lemma fst_compProd (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsMarkovKernel κ] :
    (μ ⊗ₘ κ).fst = μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ (μ ⊗ₘ κ).fst = μ

Tactic:
ext s

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
s : Set α
a✝ : MeasurableSet s
⊢ (μ ⊗ₘ κ).fst s = μ s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
s : Set α
a✝ : MeasurableSet s
⊢ (μ ⊗ₘ κ).fst s = μ s

Tactic:
rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem le_of_castSucc_lt_of_succ_lt {a b : Fin (n + 1)} {i : Fin n}
    (hl : castSucc i < a) (hu : b < succ i) : b < a

Proof state:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : ↑i < ↑a
hu : ↑b < ↑i + 1
⊢ ↑b < ↑a

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
⊢ b < a

Tactic:
simp [Fin.lt_def, -val_fin_lt] at *

Result:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : ↑i < ↑a
hu : ↑b < ↑i + 1
⊢ ↑b < ↑a
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive (attr := simp)]
lemma mul_inv_cancel_comm (a b : G) : a * b * a⁻¹ = b

Proof state:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a * b * a⁻¹ = b

Tactic:
rw [mul_comm, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem Spanning.isBase_of_le_cRank [M.RankFinite] (h : M.Spanning X) (le : #X ≤ M.cRank) :
    M.IsBase X

Proof state:
α : Type u
M : Matroid α
X : Set α
inst✝ : M.RankFinite
h : M.Spanning X
le : #↑X ≤ M.cRank
B : Set α
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.IsBase X

Tactic:
rwa [← hB.finite.eq_of_subset_of_encard_le' hBX
  (toENat.monotone' <| le.trans hB.cardinalMk_eq_cRank.ge)]

Result:
no goals

Proof state:
α : Type u
M : Matroid α
X : Set α
inst✝ : M.RankFinite
h : M.Spanning X
le : #↑X ≤ M.cRank
⊢ M.IsBase X

Tactic:
have ⟨B, hB, hBX⟩ := h.exists_isBase_subset

Result:
α : Type u
M : Matroid α
X : Set α
inst✝ : M.RankFinite
h : M.Spanning X
le : #↑X ≤ M.cRank
B : Set α
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.IsBase X
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem exists_root_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : degree (f.map i) ≠ 0) :
    ∃ x, eval₂ i x f = 0 :=
  letI := Classical.decEq L
  if hf0' : f.map i = 0 then by simp [eval₂_eq_eval_map, hf0']
  else
    let ⟨g, hg⟩ :=
      WfDvdMonoid.exists_irreducible_factor
        (show ¬IsUnit (f.map i) from mt isUnit_iff_degree_eq_zero.1 hf0) hf0'
    let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0' hg.1 hg.2)
    let ⟨i, hi⟩ := hg.2
    ⟨x, by rw [← eval_map, hi, eval_mul, show _ = _ from hx, zero_mul]⟩

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).degree ≠ 0
this : DecidableEq L := Classical.decEq L
hf0' : map i f = 0
⊢ ∃ x, eval₂ i x f = 0

Tactic:
simp [eval₂_eq_eval_map, hf0']

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i✝ : K →+* L
f : K[X]
hs : Splits i✝ f
hf0 : (map i✝ f).degree ≠ 0
this : DecidableEq L := Classical.decEq L
hf0' : ¬map i✝ f = 0
g : L[X]
hg : Irreducible g ∧ g ∣ map i✝ f
x : L
hx : g.IsRoot x
i : L[X]
hi : map i✝ f = g * i
⊢ eval₂ i✝ x f = 0

Tactic:
rw [← eval_map, hi, eval_mul, show _ = _ from hx, zero_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [MeasurableSpace β']
    {f : α → α'} {g : β → β'} (f_mble : Measurable f) (g_mble : Measurable g) :
    (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g)

Proof state:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)

Tactic:
rw [Measure.map_prod_map _ _ f_mble g_mble]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g)

Tactic:
apply Subtype.ext

Result:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ ↑((μ.map f).prod (ν.map g)) = ↑((μ.prod ν).map (Prod.map f g))

Proof state:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ ↑((μ.map f).prod (ν.map g)) = ↑((μ.prod ν).map (Prod.map f g))

Tactic:
simp only [val_eq_toMeasure, toMeasure_prod, toMeasure_map]

Result:
case a
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
theorem mk'_eq_mk' {x y : G} : mk' N x = mk' N y ↔ ∃ z ∈ N, x * z = y :=
  QuotientGroup.eq.trans <| by
    simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z ∈ N, x * z = y

Tactic:
simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]

Result:
no goals