harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem y_neg (D : ℝ) (x : E) : y D (-x) = y D x

Proof state:
case h1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, w D (-x) = w D x

Tactic:
filter_upwards with x

Result:
case h1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x✝ x : E
⊢ w D (-x) = w D x

Proof state:
case h1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x✝ x : E
⊢ w D (-x) = w D x

Tactic:
simp only [w_def, Real.rpow_natCast, mul_inv_rev, smul_neg, u_neg, smul_eq_mul, forall_const]

Result:
no goals

Proof state:
case h2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, φ (-x) = φ x

Tactic:
filter_upwards with x

Result:
case h2.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x✝ x : E
⊢ φ (-x) = φ x

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ y D (-x) = y D x

Tactic:
apply convolution_neg_of_neg_eq

Result:
case h1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, w D (-x) = w D x

case h2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, φ (-x) = φ x

Proof state:
case h2.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x✝ x : E
⊢ φ (-x) = φ x

Tactic:
simp only [φ, indicator, mem_closedBall, dist_zero_right, norm_neg, forall_const]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_equiv_apply {f : α ≃ β} (x : α →₀ M) (a : β) :
    mapDomain f x a = x (f.symm a)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
⊢ (mapDomain (⇑f) x) a = x (f.symm a)

Tactic:
conv_lhs => rw [← f.apply_symm_apply a]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
⊢ (mapDomain (⇑f) x) (f (f.symm a)) = x (f.symm a)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
⊢ (mapDomain (⇑f) x) (f (f.symm a)) = x (f.symm a)

Tactic:
exact mapDomain_apply f.injective _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_empty_list_of_contains_eq_false [LawfulBEq α]
    {l : List ((a : α) × β a)} {k : α}
    (h : (l.map Sigma.fst).contains k = false) :
    (insertMany empty l).1.get? k = none

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
h : (List.map Sigma.fst l).contains k = false
⊢ (empty.insertMany l).val.get? k = none

Tactic:
simp [get?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biInter_pair (a b : α) (s : α → Set β) : ⋂ x ∈ ({a, b} : Set α), s x = s a ∩ s b

Proof state:
α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋂ x ∈ {a, b}, s x = s a ∩ s b

Tactic:
rw [biInter_insert, biInter_singleton]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem eq_of_monic_of_associated (hp : p.Monic) (hq : q.Monic) (hpq : Associated p q) : p = q

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
u : R[X]ˣ
hq : (p * ↑u).Monic
⊢ p = p * ↑u

Tactic:
rw [(hp.of_mul_monic_left hq).eq_one_of_isUnit u.isUnit, mul_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hpq : Associated p q
⊢ p = q

Tactic:
obtain ⟨u, rfl⟩ := hpq

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
u : R[X]ˣ
hq : (p * ↑u).Monic
⊢ p = p * ↑u
-- Mathlib/Order/ModularLattice.lean
theorem wellFounded_lt_exact_sequence {β γ : Type*} [PartialOrder β] [Preorder γ]
    [h₁ : WellFoundedLT β] [h₂ : WellFoundedLT γ] (K : α)
    (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂)
    (gi : GaloisInsertion g₂ g₁) (hf : ∀ a, f₁ (f₂ a) = a ⊓ K) (hg : ∀ a, g₁ (g₂ a) = a ⊔ K) :
    WellFoundedLT α :=
  StrictMono.wellFoundedLT (f := fun A ↦ (f₂ A, g₂ A)) fun A B hAB ↦ by
    simp only [Prod.le_def, lt_iff_le_not_le, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg]
    exact strictMono_inf_prod_sup hAB

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFoundedLT β
h₂ : WellFoundedLT γ
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ (A ⊓ K ≤ B ⊓ K ∧ A ⊔ K ≤ B ⊔ K) ∧ ¬(B ⊓ K ≤ A ⊓ K ∧ B ⊔ K ≤ A ⊔ K)

Tactic:
exact strictMono_inf_prod_sup hAB

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFoundedLT β
h₂ : WellFoundedLT γ
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ (fun A => (f₂ A, g₂ A)) A < (fun A => (f₂ A, g₂ A)) B

Tactic:
simp only [Prod.le_def, lt_iff_le_not_le, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg]

Result:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFoundedLT β
h₂ : WellFoundedLT γ
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ (A ⊓ K ≤ B ⊓ K ∧ A ⊔ K ≤ B ⊔ K) ∧ ¬(B ⊓ K ≤ A ⊓ K ∧ B ⊔ K ≤ A ⊔ K)
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem isUniformOfEmpty (hP : P.parts = ∅) : P.IsUniform G ε

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.parts = ∅
⊢ P.IsUniform G ε

Tactic:
simp [IsUniform, hP, nonUniforms]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem isClosed_innerDualCone : IsClosed (s.innerDualCone : Set H)

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
⊢ IsClosed (⋂ i, ↑{↑i}.innerDualCone)

Tactic:
apply isClosed_iInter

Result:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
⊢ ∀ (i : ↑s), IsClosed ↑{↑i}.innerDualCone

Proof state:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : ↑s
h : ↑{↑x}.innerDualCone = inner ↑x ⁻¹' Ici 0
⊢ IsClosed ↑{↑x}.innerDualCone

Tactic:
rw [h]

Result:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : ↑s
h : ↑{↑x}.innerDualCone = inner ↑x ⁻¹' Ici 0
⊢ IsClosed (inner ↑x ⁻¹' Ici 0)

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
⊢ IsClosed ↑s.innerDualCone

Tactic:
rw [innerDualCone_eq_iInter_innerDualCone_singleton]

Result:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
⊢ IsClosed (⋂ i, ↑{↑i}.innerDualCone)

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : ↑s
⊢ ↑{↑x}.innerDualCone = inner ↑x ⁻¹' Ici 0

Tactic:
rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]

Result:
no goals

Proof state:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
⊢ ∀ (i : ↑s), IsClosed ↑{↑i}.innerDualCone

Tactic:
intro x

Result:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : ↑s
⊢ IsClosed ↑{↑x}.innerDualCone

Proof state:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : ↑s
h : ↑{↑x}.innerDualCone = inner ↑x ⁻¹' Ici 0
⊢ IsClosed (inner ↑x ⁻¹' Ici 0)

Tactic:
exact isClosed_Ici.preimage (continuous_const.inner continuous_id')

Result:
no goals

Proof state:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : ↑s
⊢ IsClosed ↑{↑x}.innerDualCone

Tactic:
have h : ({↑x} : Set H).innerDualCone = (inner x : H → ℝ) ⁻¹' Set.Ici 0 := by
  rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]

Result:
case h
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : ↑s
h : ↑{↑x}.innerDualCone = inner ↑x ⁻¹' Ici 0
⊢ IsClosed ↑{↑x}.innerDualCone
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_coeff_eq_zero_of_basis (b : Basis ι R L) (b' : Basis ι' R L) (k : ℕ)
    (H : (polyCharpoly φ b).coeff k = 0) :
    (polyCharpoly φ b').coeff k = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
H :
  (MvPolynomial.bind₁ g)
      (↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k)) =
    (MvPolynomial.bind₁ g) 0
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0

Tactic:
have : toMvPolynomial b' B φ = fun i ↦ (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i) :=
  funext <| toMvPolynomial_comp b' b B φ LinearMap.id

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) := (Free.chooseBasis R M).end
g : ι → MvPolynomial ι' R := toMvPolynomial b' b id
H :
  (MvPolynomial.bind₁ g)
      (↑(MvPolynomial.bind₁ (toMvPolynomial b B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k)) =
    (MvPolynomial.bind₁ g) 0
this : toMvPolynomial b' B φ = fun i => (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i)
⊢ ↑(MvPolynomial.bind₁ (toMvPolynomial b' B φ)) ((charpoly.univ R (Free.ChooseBasisIndex R M)).coeff k) = 0
-- Mathlib/Probability/Process/Stopping.lean
theorem max [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → ι} (hτ : IsStoppingTime f τ)
    (hπ : IsStoppingTime f π) : IsStoppingTime f fun ω => max (τ ω) (π ω)

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ IsStoppingTime f fun ω => τ ω ⊔ π ω

Tactic:
intro i

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet {ω | (fun ω => τ ω ⊔ π ω) ω ≤ i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet {ω | (fun ω => τ ω ⊔ π ω) ω ≤ i}

Tactic:
simp_rw [max_le_iff, Set.setOf_and]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet ({a | τ a ≤ i} ∩ {a | π a ≤ i})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet ({a | τ a ≤ i} ∩ {a | π a ≤ i})

Tactic:
exact (hτ i).inter (hπ i)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma IsTotallyUnimodular.transpose {A : Matrix m n R} (hA : A.IsTotallyUnimodular) :
    Aᵀ.IsTotallyUnimodular

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → n
g✝ : Fin k✝ → m
⊢ (A.submatrix g✝ f✝).det ∈ Set.range SignType.cast

Tactic:
apply hA

Result:
no goals

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f : Fin k → n) (g : Fin k → m), (A.submatrix g f).det ∈ Set.range SignType.cast

Tactic:
intro _ _ _

Result:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → n
g✝ : Fin k✝ → m
⊢ (A.submatrix g✝ f✝).det ∈ Set.range SignType.cast

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
⊢ Aᵀ.IsTotallyUnimodular

Tactic:
simp only [isTotallyUnimodular_iff, ← transpose_submatrix, det_transpose] at hA ⊢

Result:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f : Fin k → n) (g : Fin k → m), (A.submatrix g f).det ∈ Set.range SignType.cast
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
    [i : Std.Total (¬ · < · : α → α → Prop)]
    {l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂

Proof state:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
h' : l₂ ≤ l₁
⊢ l₁ ≤ l₂

Tactic:
exfalso

Result:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
h' : l₂ ≤ l₁
⊢ False

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
⊢ l₁ ≤ l₂

Tactic:
obtain (h' | h') := List.le_total l₁ l₂

Result:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
h' : l₁ ≤ l₂
⊢ l₁ ≤ l₂

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
h' : l₂ ≤ l₁
⊢ l₁ ≤ l₂

Proof state:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
h' : l₁ ≤ l₂
⊢ l₁ ≤ l₂

Tactic:
exact h'

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : List α
h : l₁ < l₂
h' : l₂ ≤ l₁
⊢ False

Tactic:
exact h' h

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
lemma reciprocalFactors_even {n : ℕ} (h0 : n ≠ 0) (h2 : Even n) :
    reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Proof state:
n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ n ≠ 1

Tactic:
rintro rfl

Result:
h0 : 1 ≠ 0
h2 : Even 1
⊢ False

Proof state:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Tactic:
rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_pos h2]

Result:
no goals

Proof state:
n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Tactic:
have h1 : n ≠ 1 := by
  rintro rfl
  norm_num at h2

Result:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Proof state:
h0 : 1 ≠ 0
h2 : Even 1
⊢ False

Tactic:
norm_num at h2

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.exists_isBase_subset_spanning (hI : M.Indep I) (hS : M.Spanning S) (hIS : I ⊆ S) :
    ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Proof state:
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
⊢ ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
obtain ⟨B, hB⟩ := hI.subset_isBasis_of_subset hIS

Result:
case intro
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
B : Set α
hB : M.IsBasis B S ∧ I ⊆ B
⊢ ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Proof state:
case intro
α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
B : Set α
hB : M.IsBasis B S ∧ I ⊆ B
⊢ ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
exact ⟨B, hB.1.isBase_of_spanning hS, hB.2, hB.1.subset⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_intMin {w i : Nat} :
    (intMin w).getMsbD i = (decide (0 < w) && decide (i = 0))

Proof state:
w✝ i✝ w i : Nat
⊢ (decide (i + 1 < w + 1) && decide (w + 1 - 1 - (i + 1) + 1 = w + 1)) = (decide (0 < w + 1) && decide (i + 1 = 0))

Tactic:
simp

Result:
w✝ i✝ w i : Nat
⊢ i < w → ¬w - (i + 1) = w

Proof state:
w i : Nat
⊢ (intMin w).getMsbD i = (decide (0 < w) && decide (i = 0))

Tactic:
simp only [getMsbD, getLsbD_intMin]

Result:
w i : Nat
⊢ (decide (i < w) && decide (w - 1 - i + 1 = w)) = (decide (0 < w) && decide (i = 0))

Proof state:
w✝ i✝ w i : Nat
⊢ i < w → ¬w - (i + 1) = w

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
⊢ (decide (i < w) && decide (w - 1 - i + 1 = w)) = (decide (0 < w) && decide (i = 0))

Tactic:
match w, i with
| 0,   _    => simp
| w+1, 0    => simp
| w+1, i+1  => simp; omega

Result:
no goals

Proof state:
w✝ i w : Nat
⊢ (decide (0 < w + 1) && decide (w + 1 - 1 - 0 + 1 = w + 1)) = (decide (0 < w + 1) && decide (0 = 0))

Tactic:
simp

Result:
no goals

Proof state:
w i x✝ : Nat
⊢ (decide (x✝ < 0) && decide (0 - 1 - x✝ + 1 = 0)) = (decide (0 < 0) && decide (x✝ = 0))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
    get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
k a : α
v : β
⊢ get! (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then v else get! m a

Tactic:
exact Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
k a : α
v : β
⊢ get! (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then v else get! m a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
k a : α
v : β
⊢ get! (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then v else get! m a
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem mul_log_eq_log_iff {x y z : ℝ} (hx : 0 < x) (hz : 0 < z) :
    y * log x = log z ↔ x ^ y = z :=
  ⟨fun h ↦ log_injOn_pos (rpow_pos_of_pos hx _) hz <| log_rpow hx _ |>.trans h,
  by rintro rfl; rw [log_rpow hx]⟩

Proof state:
x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
⊢ y * log x = log (x ^ y)

Tactic:
rw [log_rpow hx]

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 < x
hz : 0 < z
⊢ x ^ y = z → y * log x = log z

Tactic:
rintro rfl

Result:
x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
⊢ y * log x = log (x ^ y)
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem linearIndependent_mul_of_flat (H : M.LinearDisjoint N)
    (hf : Module.Flat R M ∨ Module.Flat R N)
    {κ ι : Type*} {m : κ → M} {n : ι → N} (hm : LinearIndependent R m)
    (hn : LinearIndependent R n) : LinearIndependent R fun (i : κ × ι) ↦ (m i.1).1 * (n i.2).1

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)

Tactic:
rcases hf with _ | _

Result:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Module.Flat R ↥M
⊢ LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)

case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Module.Flat R ↥N
⊢ LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)

Proof state:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Module.Flat R ↥N
⊢ LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)

Tactic:
exact H.linearIndependent_mul_of_flat_right hm hn

Result:
no goals

Proof state:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Module.Flat R ↥M
⊢ LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)

Tactic:
exact H.linearIndependent_mul_of_flat_left hm hn

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k : α} :
    (Const.insertMany m l).1.contains k = (m.contains k || (l.map Prod.fst).contains k)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k : α
⊢ (insertMany m l).val.contains k = (m.contains k || (List.map Prod.fst l).contains k)

Tactic:
simp_to_model [Const.insertMany] using List.containsKey_insertListConst

Result:
no goals