harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n)
    (p : PosFin n → Bool) (pf : p ⊨ f) :
    (insertRupUnits f (negate c)).2 = true → p ⊨ c

Proof state:
case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : InsertUnitInvariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  InsertUnitInvariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j1 j2 : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j1] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
h2 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j2] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
left✝¹ : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j1 → k ≠ j2 → (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map Literal.negate c.clause)).fst.toList
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map Literal.negate c.clause)).fst.toList
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_false_not_in_c : ¬Literal.negate (i, true) ∈ c.clause
⊢ False

Tactic:
exact i_false_not_in_c i_true_in_insertUnit_fold

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
⊢ false = true → ∃ i, f.assignments[i.val] = both

Tactic:
intro h

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
h : false = true
⊢ ∃ i, f.assignments[i.val] = both
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supported_comap_lmapDomain (f : α → α') (s : Set α') :
    supported M R (f ⁻¹' s) ≤ (supported M R s).comap (lmapDomain M R f)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑l.support ⊆ f ⁻¹' s
⊢ l ∈ comap (lmapDomain M R f) (supported M R s)

Tactic:
show ↑(mapDomain f l).support ⊆ s

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑l.support ⊆ f ⁻¹' s
⊢ ↑(mapDomain f l).support ⊆ s

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
⊢ supported M R (f ⁻¹' s) ≤ comap (lmapDomain M R f) (supported M R s)

Tactic:
intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑l.support ⊆ f ⁻¹' s
⊢ l ∈ comap (lmapDomain M R f) (supported M R s)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
⊢ supported M R (f ⁻¹' s) ≤ comap (lmapDomain M R f) (supported M R s)

Tactic:
classical
intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
show ↑(mapDomain f l).support ⊆ s
rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
exact Set.Subset.trans mapDomain_support hl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑(Finset.image f l.support) ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s

Tactic:
exact Set.Subset.trans mapDomain_support hl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑l.support ⊆ f ⁻¹' s
⊢ ↑(mapDomain f l).support ⊆ s

Tactic:
rw [← Set.image_subset_iff, ← Finset.coe_image] at hl

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : ↑(Finset.image f l.support) ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_left_cancel {n m k : Nat} : n + m = n + k → m = k

Proof state:
case succ
m k n : Nat
ih : n + m = n + k → m = k
h : n + m = n + k
⊢ m = k

Tactic:
apply ih h

Result:
no goals

Proof state:
case zero
m k : Nat
⊢ 0 + m = 0 + k → m = k

Tactic:
simp

Result:
no goals

Proof state:
case succ
m k n : Nat
ih : n + m = n + k → m = k
⊢ n + m = n + k → m = k

Tactic:
intro h

Result:
case succ
m k n : Nat
ih : n + m = n + k → m = k
h : n + m = n + k
⊢ m = k

Proof state:
case succ
m k n : Nat
ih : n + m = n + k → m = k
⊢ n + 1 + m = n + 1 + k → m = k

Tactic:
simp [succ_add, succ.injEq]

Result:
case succ
m k n : Nat
ih : n + m = n + k → m = k
⊢ n + m = n + k → m = k

Proof state:
n m k : Nat
⊢ n + m = n + k → m = k

Tactic:
induction n with
| zero => simp
| succ n ih => simp [succ_add, succ.injEq]; intro h; apply ih h

Result:
no goals
-- Mathlib/Probability/CondVar.lean
lemma condVar_of_not_le (hm : ¬m ≤ m₀) : Var[X; μ | m] = 0

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : ¬m ≤ m₀
⊢ Var[X; μ | m] = 0

Tactic:
rw [condVar, condExp_of_not_le hm]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_directSum {ι : Type v} (M : ι → Type w) [∀ i : ι, AddCommMonoid (M i)]
    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] :
    Module.rank R (⨁ i, M i) = Cardinal.sum fun i => Module.rank R (M i)

Proof state:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) := DFinsupp.basis fun i => B i
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)

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

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Free R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)

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

Result:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)

Proof state:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)

Tactic:
let b : Basis _ R (⨁ i, M i) := DFinsupp.basis fun i => B i

Result:
R : Type u
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)
b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) := DFinsupp.basis fun i => B i
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem selfZPow_mul_neg (d : ℤ) : selfZPow x B d * selfZPow x B (-d) = 1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
by_cases hd : d ≤ 0

Result:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Proof state:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
erw [selfZPow_of_nonneg x B (le_of_not_le hd), selfZPow_of_nonpos, ← map_pow, Int.natAbs_neg,
  @IsLocalization.mk'_spec' R _ (Submonoid.powers x) B _ _ _ 1 (Submonoid.pow x d.natAbs),
  map_one]

Result:
case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ -d ≤ 0

Proof state:
case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ -d ≤ 0

Tactic:
refine nonpos_of_neg_nonneg (le_of_lt ?_)

Result:
case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ 0 < - -d

Proof state:
case pos.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d

Tactic:
apply nonneg_of_neg_nonpos

Result:
case pos.hn.a
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ - -d ≤ 0

Proof state:
case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : ¬d ≤ 0
⊢ 0 < - -d

Tactic:
rwa [neg_neg, ← not_le]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
erw [selfZPow_of_nonpos x B hd, selfZPow_of_nonneg, ← map_pow, Int.natAbs_neg,
  IsLocalization.mk'_spec, map_one]

Result:
case pos.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d

Proof state:
case pos.hn.a
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ - -d ≤ 0

Tactic:
rwa [neg_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem star_mem_iff {x : CliffordAlgebra Q} : star x ∈ spinGroup Q ↔ x ∈ spinGroup Q

Proof state:
case h.e'_5
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ spinGroup Q
⊢ x = star (star x)

Tactic:
exact (star_star x).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ spinGroup Q → x ∈ spinGroup Q

Tactic:
intro hx

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ spinGroup Q
⊢ x ∈ spinGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ spinGroup Q ↔ x ∈ spinGroup Q

Tactic:
refine ⟨?_, star_mem⟩

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ spinGroup Q → x ∈ spinGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ spinGroup Q
⊢ x ∈ spinGroup Q

Tactic:
convert star_mem hx

Result:
case h.e'_5
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ spinGroup Q
⊢ x = star (star x)
-- Mathlib/GroupTheory/Sylow.lean
theorem dvd_card_of_dvd_card [Finite G] {p : ℕ} [Fact p.Prime] (P : Sylow p G)
    (hdvd : p ∣ Nat.card G) : p ∣ Nat.card P

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ p ∣ Nat.card ↥↑P

Tactic:
rw [← pow_one p] at hdvd

Result:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Nat.card G
⊢ p ∣ Nat.card ↥↑P

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Nat.card G
key : p ^ 1 ∣ Nat.card ↥↑P
⊢ p ∣ Nat.card ↥↑P

Tactic:
rwa [pow_one] at key

Result:
no goals

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Nat.card G
⊢ p ∣ Nat.card ↥↑P

Tactic:
have key := P.pow_dvd_card_of_pow_dvd_card hdvd

Result:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Nat.card G
key : p ^ 1 ∣ Nat.card ↥↑P
⊢ p ∣ Nat.card ↥↑P
-- Mathlib/Data/Option/NAry.lean
theorem map₂_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : map₂ f a b = map₂ g b a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ map₂ f a b = map₂ g b a

Tactic:
cases a <;> cases b <;> simp [h_comm]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem _root_.Disjoint.image {s t u : Set α} {f : α → β} (h : Disjoint s t) (hf : u.InjOn f)
    (hs : s ⊆ u) (ht : t ⊆ u) : Disjoint (f '' s) (f '' t)

Proof state:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ Disjoint (f '' s) (f '' t)

Tactic:
rw [disjoint_iff_inter_eq_empty] at h ⊢

Result:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅

Proof state:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅

Tactic:
rw [← hf.image_inter hs ht, h, image_empty]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem degree_prod_of_monic [Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) :
    (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ ∀ f_1 ∈ Multiset.map f s.val, f_1.Monic

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
f : ι → R[X]
inst✝ : Nontrivial R
h : ∀ i ∈ s, (f i).Monic
⊢ (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree

Tactic:
simpa using degree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem monotone_iterate_of_id_le (h : id ≤ f) : Monotone fun m => f^[m] :=
  monotone_nat_of_le_succ fun n x => by
    rw [iterate_succ_apply']
    exact h _

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)

Tactic:
exact h _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply']

Result:
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_eq_getD [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β} :
    getD m a fallback = m.getD a fallback

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback : β
⊢ getD m a fallback = m.getD a fallback

Tactic:
simp_to_model using List.getValueD_eq_getValueCastD

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
/-- If the equalizer comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
equalizer of `(f,g)`.
-/
lemma PreservesEqualizer.of_iso_comparison [i : IsIso (equalizerComparison f g G)] :
    PreservesLimit (parallelPair f g) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ IsLimit (Fork.ofι (G.map (equalizer.ι f g)) ⋯)

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (parallelPair (G.map f) (G.map g))) i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ IsLimit (G.mapCone (Fork.ofι (equalizer.ι f g) ⋯))

Tactic:
apply (isLimitMapConeForkEquiv _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ IsLimit (Fork.ofι (G.map (equalizer.ι f g)) ⋯)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ PreservesLimit (parallelPair f g) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (equalizerIsEqualizer f g)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
i : IsIso (equalizerComparison f g G)
⊢ IsLimit (G.mapCone (Fork.ofι (equalizer.ι f g) ⋯))
-- Mathlib/Tactic/ReduceModChar.lean
lemma CharP.neg_mul_eq_sub_one_mul {α : Type _} [Ring α] (n : ℕ) (inst : CharP α n) (a b : α)
    (na : ℕ) (na' : α) (p : IsNat ((n - 1) * a : α) na) (pa : na = na') :
    -(a * b) = na' * b

Proof state:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -(a * b) = na' * b

Tactic:
rw [← pa, ← p.out, ← neg_one_mul]

Result:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -1 * (a * b) = (↑n - 1) * a * b

Proof state:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -1 * (a * b) = (↑n - 1) * a * b

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_mem_aux (hs : ¬ BddAbove s) (o : Ordinal) :
    enumOrd s o ∈ s ∩ { b | ∀ c, c < o → enumOrd s c < b }

Proof state:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < o, enumOrd s c < b}) ∈ s ∩ {b | ∀ c < o, enumOrd s c < b}

Tactic:
exact csInf_mem (enumOrd_nonempty hs o)

Result:
no goals

Proof state:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ enumOrd s o ∈ s ∩ {b | ∀ c < o, enumOrd s c < b}

Tactic:
rw [enumOrd]

Result:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < o, enumOrd s c < b}) ∈ s ∩ {b | ∀ c < o, enumOrd s c < b}
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_apply (m : ℝ≥0∞ → ℝ≥0∞) (s : Set X) :
    mkMetric m s =
      ⨆ (r : ℝ≥0∞) (_ : 0 < r),
        ⨅ (t : ℕ → Set X) (_ : s ⊆ iUnion t) (_ : ∀ n, diam (t n) ≤ r),
          ∑' n, ⨆ _ : (t n).Nonempty, m (diam (t n))

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Tactic:
by_cases htr : ∀ n, diam (t n) ≤ r

Result:
case pos
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ¬∀ (n : ℕ), diam (t n) ≤ r
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) =
    ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (diam (t n))

Proof state:
case neg.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Tactic:
refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩

Result:
case neg.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Proof state:
case neg.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ ⨆ (_ : (t n).Nonempty), ⨅ (_ : diam (t n) ≤ r), m (diam (t n)) = ⊤

Tactic:
rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]

Result:
case neg.intro.hnc
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ ¬diam (t n) ≤ r

case neg.intro.hc
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < diam (t n)
⊢ (t n).Nonempty