harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem sat_nil {assign : α → Bool} : Sat assign ([] : CNF α)

Proof state:
α : Type u_1
assign : α → Bool
⊢ Sat assign []

Tactic:
simp [sat_def]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
@[simp]
lemma prodMk_fst {a : C} (x : F.obj a) (y : G.obj a) :
    (Limits.prod.fst (X := F)).app a (prodMk x y) = x

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x : F.obj a
y : G.obj a
⊢ Limits.prod.fst.app a (prodMk x y) = x

Tactic:
simp only [prodMk, binaryProductIso_inv_comp_fst_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_zero : range' s 0 step = []

Proof state:
s step : Nat
⊢ range' s 0 step = []

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_inv_reverse : ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).reverse.prod
  | [] => by simp
  | x :: xs => by simp [prod_inv_reverse xs]

Proof state:
G : Type u_7
inst✝ : Group G
x : G
xs : List G
⊢ (x :: xs).prod⁻¹ = (map (fun x => x⁻¹) (x :: xs)).reverse.prod

Tactic:
simp [prod_inv_reverse xs]

Result:
no goals

Proof state:
G : Type u_7
inst✝ : Group G
⊢ [].prod⁻¹ = (map (fun x => x⁻¹) []).reverse.prod

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma unbot_le_iff (hx : x ≠ ⊥) : unbot x hx ≤ b ↔ x ≤ b

Proof state:
case intro
α : Type u_1
b : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx ≤ b ↔ ↑x ≤ ↑b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
b : α
inst✝ : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx ≤ b ↔ x ≤ ↑b

Tactic:
lift x to α using id hx

Result:
case intro
α : Type u_1
b : α
inst✝ : LE α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx ≤ b ↔ ↑x ≤ ↑b
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isIrreducible_iff_vanishingIdeal_isPrime {s : Set (PrimeSpectrum R)} :
    IsIrreducible s ↔ (vanishingIdeal s).IsPrime

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsIrreducible s ↔ (vanishingIdeal s).IsPrime

Tactic:
rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
  isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem lift_range (f : A →ₙₐ[R] C) :
    (lift f).range = Algebra.adjoin R (NonUnitalAlgHom.range f : Set C) :=
  eq_of_forall_ge_iff fun c ↦ by rw [lift_range_le, Algebra.adjoin_le_iff]; rfl

Proof state:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ (lift f).range ≤ c ↔ Algebra.adjoin R ↑(NonUnitalAlgHom.range f) ≤ c

Tactic:
rw [lift_range_le, Algebra.adjoin_le_iff]

Result:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ ↑(NonUnitalAlgHom.range f) ⊆ ↑c

Proof state:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ ↑(NonUnitalAlgHom.range f) ⊆ ↑c

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem image_map_comp_imageSubobjectIso_inv {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z}
    [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
    image.map sq ≫ (imageSubobjectIso _).inv =
      (imageSubobjectIso _).inv ≫ imageSubobjectMap sq

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv = (imageSubobjectIso f).inv ≫ imageSubobjectMap sq

Tactic:
ext

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ (imageSubobject (Arrow.mk g).hom).arrow =
    ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ (imageSubobject (Arrow.mk g).hom).arrow

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ (imageSubobject (Arrow.mk g).hom).arrow =
    ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ (imageSubobject (Arrow.mk g).hom).arrow

Tactic:
simpa using image.map_ι sq

Result:
no goals
-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem AlgHom.card_of_splits (L : Type*) [Field L] [Algebra F L]
    (hL : ∀ x : E, (minpoly F x).Splits (algebraMap F L)) :
    Fintype.card (E →ₐ[F] L) = finrank F E

Proof state:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
hL : ∀ (x : E), Splits (algebraMap F L) (minpoly F x)
⊢ Fintype.card (E →ₐ[F] L) = finrank F E

Tactic:
convert (AlgHom.card_of_powerBasis (L := L) (Field.powerBasisOfFiniteOfSeparable F E)
  (Algebra.IsSeparable.isSeparable _ _) <| hL _).trans
    (PowerBasis.finrank _).symm

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_compMeasurePreserving {s : Set β} (hs : MeasurableSet s)
    (hμs : μb s ≠ ∞) (c : E) (hf : MeasurePreserving f μ μb) :
    Lp.compMeasurePreserving f hf (indicatorConstLp p hs hμs c) =
      indicatorConstLp p (hs.preimage hf.measurable)
        (by rwa [hf.measure_preimage hs.nullMeasurableSet]) c :=
  rfl

Proof state:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
f : α → β
s : Set β
hs : MeasurableSet s
hμs : μb s ≠ ⊤
c : E
hf : MeasurePreserving f μ μb
⊢ μ (f ⁻¹' s) ≠ ⊤

Tactic:
rwa [hf.measure_preimage hs.nullMeasurableSet]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
theorem normalClosure_eq_iSup_adjoin' [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
    normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L)

Proof state:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
⊢ normalClosure F K L = ⨆ x, adjoin F ((minpoly F x).rootSet L)

Tactic:
have ⟨φ⟩ := ne

Result:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ normalClosure F K L = ⨆ x, adjoin F ((minpoly F x).rootSet L)

Proof state:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ Splits (algebraMap F L) (minpoly F (φ x))

Tactic:
apply h.splits

Result:
no goals

Proof state:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ Splits (algebraMap F L) (minpoly F x)

Tactic:
rw [← minpoly.algHom_eq _ φ.injective]

Result:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ Splits (algebraMap F L) (minpoly F (φ x))

Proof state:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
⊢ normalClosure F K L = ⨆ x, adjoin F ((minpoly F x).rootSet L)

Tactic:
refine h.toIsAlgebraic.of_injective φ φ.injective
  |>.normalClosure_eq_iSup_adjoin_of_splits fun x ↦ ?_

Result:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ Splits (algebraMap F L) (minpoly F x)
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem restrict_biInf {ι} {I : Set ι} (hI : I.Nonempty) (s : Set α) (m : ι → OuterMeasure α) :
    restrict s (⨅ i ∈ I, m i) = ⨅ i ∈ I, restrict s (m i)

Proof state:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i, m ↑i) = ⨅ i, (restrict s) (m ↑i)

Tactic:
exact restrict_iInf _ _

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
⊢ (restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)

Tactic:
haveI := hI.to_subtype

Result:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)

Proof state:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)

Tactic:
rw [← iInf_subtype'', ← iInf_subtype'']

Result:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i, m ↑i) = ⨅ i, (restrict s) (m ↑i)
-- Mathlib/Data/Matrix/Basis.lean
theorem stdBasisMatrix_zero (i : m) (j : n) : stdBasisMatrix i j (0 : α) = 0

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
i✝ : m
j✝ : n
⊢ of (fun i' j' => if i = i' ∧ j = j' then 0 else 0) i✝ j✝ = 0 i✝ j✝

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
⊢ (of fun i' j' => if i = i' ∧ j = j' then 0 else 0) = 0

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
i✝ : m
j✝ : n
⊢ of (fun i' j' => if i = i' ∧ j = j' then 0 else 0) i✝ j✝ = 0 i✝ j✝

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
⊢ stdBasisMatrix i j 0 = 0

Tactic:
unfold stdBasisMatrix

Result:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
⊢ (of fun i' j' => if i = i' ∧ j = j' then 0 else 0) = 0
-- Mathlib/Algebra/Order/Group/Basic.lean
@[to_additive zsmul_left_strictAnti]
lemma zpow_right_strictAnti (ha : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
exact mul_lt_of_lt_one_right' (a ^ n) ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : a < 1
⊢ StrictAnti fun n => a ^ n

Tactic:
refine strictAnti_int_of_succ_lt fun n ↦ ?_

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n

Tactic:
rw [zpow_add_one]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l : Vector α n) (l' : Vector α k) :
    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f

Proof state:
case mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
k : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l' : Vector α k
l : Array α
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ } ++ l') = do
    let b ← foldlM f b { toArray := l, size_toArray := ⋯ }
    foldlM f b l'

Tactic:
rcases l' with ⟨l', rfl⟩

Result:
case mk.mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : Array α
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ } ++ { toArray := l', size_toArray := ⋯ }) = do
    let b ← foldlM f b { toArray := l, size_toArray := ⋯ }
    foldlM f b { toArray := l', size_toArray := ⋯ }

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n k : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : Vector α n
l' : Vector α k
⊢ foldlM f b (l ++ l') = do
    let b ← foldlM f b l
    foldlM f b l'

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
k : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l' : Vector α k
l : Array α
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ } ++ l') = do
    let b ← foldlM f b { toArray := l, size_toArray := ⋯ }
    foldlM f b l'

Proof state:
case mk.mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : Array α
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ } ++ { toArray := l', size_toArray := ⋯ }) = do
    let b ← foldlM f b { toArray := l, size_toArray := ⋯ }
    foldlM f b { toArray := l', size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/DershowitzManna.lean
theorem wellFounded_isDershowitzMannaLT [WellFoundedLT α] :
    WellFounded (IsDershowitzMannaLT : Multiset α → Multiset α → Prop)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded (TransGen Multiset.OneStep)

Tactic:
exact isDershowitzMannaLT_singleton_wf.transGen

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded IsDershowitzMannaLT

Tactic:
rw [← transGen_oneStep_eq_isDershowitzMannaLT]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded (TransGen Multiset.OneStep)
-- Mathlib/Data/Nat/Init.lean
protected lemma min_right_comm (a b c : ℕ) : min (min a b) c = min (min a c) b

Proof state:
a b c : ℕ
⊢ min (min a b) c = min (min a c) b

Tactic:
rw [Nat.min_assoc, Nat.min_assoc, b.min_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
@[parity_simps] lemma even_sub (h : n ≤ m) : Even (m - n) ↔ (Even m ↔ Even n)

Proof state:
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)

Tactic:
by_cases h : Even n <;> simp [h]

Result:
no goals

Proof state:
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ (Even m ↔ Even n)

Tactic:
conv_rhs => rw [← Nat.sub_add_cancel h, even_add]

Result:
m n : ℕ
h : n ≤ m
⊢ Even (m - n) ↔ ((Even (m - n) ↔ Even n) ↔ Even n)
-- Mathlib/CategoryTheory/Iso.lean
theorem cancel_iso_hom_left {X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z) :
    f.hom ≫ g = f.hom ≫ g' ↔ g = g'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ≅ Y
g g' : Y ⟶ Z
⊢ f.hom ≫ g = f.hom ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem ofAIG.Inv2 (aig : AIG α) : Inv2 aig.decls aig.decls.size (ofAIG aig)

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)

Tactic:
have := (ofAIGAux aig).inv2

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
this : State.Inv2 aig.decls aig.decls.size (ofAIGAux aig).map
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
this : State.Inv2 aig.decls aig.decls.size (ofAIGAux aig).map
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)

Tactic:
simp [ofAIG, this]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem one_minus_single_neg_mul {x y : HahnSeries Γ R} {r : R} (hr : r * x.leadingCoeff = 1)
    (hxy : x = y + single x.order x.leadingCoeff) (hxo : IsAddUnit x.order) :
    1 - single (IsAddUnit.addUnit hxo).neg r * x = -(single (IsAddUnit.addUnit hxo).neg r * y)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x y : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
hxo : IsAddUnit x.order
⊢ 1 - (single hxo.addUnit.neg) r * x = -((single hxo.addUnit.neg) r * y)

Tactic:
nth_rw 2 [hxy]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x y : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
hxo : IsAddUnit x.order
⊢ 1 - (single hxo.addUnit.neg) r * (y + (single x.order) x.leadingCoeff) = -((single hxo.addUnit.neg) r * y)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x y : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
hxo : IsAddUnit x.order
⊢ 1 - (single hxo.addUnit.neg) r * (y + (single x.order) x.leadingCoeff) = -((single hxo.addUnit.neg) r * y)

Tactic:
rw [mul_add, single_mul_single, hr, AddUnits.neg_eq_val_neg, IsAddUnit.val_neg_add,
sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.rankPos_of_nonempty (hB : M.IsBase B) (h : B.Nonempty) : M.RankPos

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
he : M.IsBase ∅
⊢ False

Tactic:
obtain rfl := he.eq_of_subset_isBase hB (empty_subset B)

Result:
α : Type u_1
M : Matroid α
he hB : M.IsBase ∅
h : ∅.Nonempty
⊢ False

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ ¬M.IsBase ∅

Tactic:
intro he

Result:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
he : M.IsBase ∅
⊢ False

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ M.RankPos

Tactic:
rw [rankPos_iff]

Result:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ ¬M.IsBase ∅

Proof state:
α : Type u_1
M : Matroid α
he hB : M.IsBase ∅
h : ∅.Nonempty
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖x‖ / Real.Angle.sin (o.oangle y (y - x)) = ‖y - x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.left_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
-- Mathlib/Analysis/Convex/Side.lean
theorem sOppSide_smul_vsub_vadd_left {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s)
    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : t < 0) : s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
⊢ s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨wOppSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
⊢ x ∈ s

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
⊢ x ∈ s

Tactic:
rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne,
  vsub_right_mem_direction_iff_mem hp₁] at h

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_inr_image {s : Set β} :
    MeasurableSet (Sum.inr '' s : Set (α ⊕ β)) ↔ MeasurableSet s

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
⊢ MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s

Tactic:
simp [measurableSet_sum_iff, Sum.inr_injective.preimage_image]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : A →ₐ[R] B) (hf : Function.Injective f)
    (s : ι → Subalgebra R A) : (iInf s).map f = ⨅ (i : ι), (s i).map f

Proof state:
case a
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ ↑(Subalgebra.map f (iInf s)) = ↑(⨅ i, Subalgebra.map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ Subalgebra.map f (iInf s) = ⨅ i, Subalgebra.map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ ↑(Subalgebra.map f (iInf s)) = ↑(⨅ i, Subalgebra.map f (s i))
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ioc {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    (Nat.cast : ℕ → α) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Ioc a b = Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋₊ ⌊b⌋₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋₊ ⌊b⌋₊

Tactic:
simp [floor_lt, le_floor_iff, hb, ha]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_vector (α : Type u) (n : ℕ) : #(List.Vector α n) = #α ^ n :=
  (mk_congr (Equiv.vectorEquivFin α n)).trans <| by simp

Proof state:
α : Type u
n : ℕ
⊢ #(Fin n → α) = #α ^ n

Tactic:
simp

Result:
no goals