harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma transfiniteCompositions_monotone :
    Monotone (transfiniteCompositions.{w} (C := C))

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
w✝³ : LinearOrder J
w✝² : SuccOrder J
w✝¹ : OrderBot J
w✝ : WellFoundedLT J
hf : W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Tactic:
exact transfiniteCompositionsOfShape_le_transfiniteCompositions _ _ _
  (transfiniteCompositionsOfShape_monotone J h _ hf)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone transfiniteCompositions.{w, v, u}

Tactic:
intro W₁ W₂ h X Y f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W₁ f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Tactic:
obtain ⟨J, _, _, _, _, hf⟩ := hf

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
w✝³ : LinearOrder J
w✝² : SuccOrder J
w✝¹ : OrderBot J
w✝ : WellFoundedLT J
hf : W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W₁ f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Tactic:
rw [transfiniteCompositions_iff] at hf

Result:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f
-- Mathlib/Data/Complex/Trigonometric.lean
theorem exp_ofReal_mul_I_re (x : ℝ) : (exp (x * I)).re = Real.cos x

Proof state:
x : ℝ
⊢ (cexp (↑x * I)).re = Real.cos x

Tactic:
simp [exp_mul_I, cos_ofReal_re]

Result:
no goals
-- Mathlib/Algebra/Colimit/Ring.lean
theorem ringEquiv_of [Nonempty ι] {i g} : ringEquiv G f' (of _ _ i g) = ⟦⟨i, g⟩⟧

Proof state:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty ι
i : ι
g : G i
⊢ (ringEquiv G f') ((of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) g) = ⟦⟨i, g⟩⟧

Tactic:
simp [ringEquiv]

Result:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty ι
i : ι
g : G i
⊢ (DirectLimit.Ring.of G f' i) g = ⟦⟨i, g⟩⟧

Proof state:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h => ⇑(f' i j h)
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty ι
i : ι
g : G i
⊢ (DirectLimit.Ring.of G f' i) g = ⟦⟨i, g⟩⟧

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem IsClosedBelow.sInter {o : Ordinal} {S : Set (Set Ordinal)}
    (h : ∀ C ∈ S, IsClosedBelow C o) : IsClosedBelow (⋂₀ S) o

Proof state:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ ∀ p < o, p.IsAcc (⋂₀ S) → p ∈ ⋂₀ S

Tactic:
intro p plto pAcc C CmemS

Result:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
p : Ordinal.{u_1}
plto : p < o
pAcc : p.IsAcc (⋂₀ S)
C : Set Ordinal.{u_1}
CmemS : C ∈ S
⊢ p ∈ C

Proof state:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
p : Ordinal.{u_1}
plto : p < o
pAcc : p.IsAcc (⋂₀ S)
C : Set Ordinal.{u_1}
CmemS : C ∈ S
⊢ p ∈ C

Tactic:
exact (h C CmemS).forall_lt p plto (pAcc.mono (sInter_subset_of_mem CmemS))

Result:
no goals

Proof state:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ IsClosedBelow (⋂₀ S) o

Tactic:
rw [isClosedBelow_iff]

Result:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ ∀ p < o, p.IsAcc (⋂₀ S) → p ∈ ⋂₀ S
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isCharTwoJEqZeroNF_of_char_two : W.b₈ = W.a₄ ^ 2

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ W.b₈ = W.a₄ ^ 2

Tactic:
rw [b₈_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ -W.a₄ ^ 2 = W.a₄ ^ 2

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ -W.a₄ ^ 2 = W.a₄ ^ 2

Tactic:
linear_combination -W.a₄ ^ 2 * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem decidablePrime_csimp :
    @decidablePrime = @decidablePrime'

Proof state:
⊢ decidablePrime = decidablePrime'

Tactic:
funext

Result:
case h
x✝ : ℕ
⊢ x✝.decidablePrime = x✝.decidablePrime'

Proof state:
case h
x✝ : ℕ
⊢ x✝.decidablePrime = x✝.decidablePrime'

Tactic:
apply Subsingleton.elim

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nndist_eq_of_L1 (x y : WithLp 1 (α × β)) :
    nndist x y = nndist x.fst y.fst + nndist x.snd y.snd :=
  NNReal.eq <| by
    push_cast
    exact prod_dist_eq_of_L1 _ _

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ ↑(nndist x y) = ↑(nndist x.1 y.1 + nndist x.2 y.2)

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ dist x y = dist x.1 y.1 + dist x.2 y.2

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ dist x y = dist x.1 y.1 + dist x.2 y.2

Tactic:
exact prod_dist_eq_of_L1 _ _

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.ofBijective_coeLinearMap_same (h : IsInternal A)
    {i : ι} (x : A i) :
    (LinearEquiv.ofBijective (coeLinearMap A) h).symm x i = x

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
i : ι
x : ↥(A i)
⊢ ((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) i = x

Tactic:
rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_same]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma measure_sub_rnDeriv (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] [IsFiniteMeasure μ] :
    μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
nth_rw 1 [← singularPart_add_rnDeriv μ ν]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : IsFiniteMeasure μ
⊢ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν

Tactic:
exact Measure.add_sub_cancel

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem idealRange_eq_top_of_surjective (h : Function.Surjective f) : f.idealRange = ⊤

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : f.range = ⊤
⊢ f.idealRange = ⊤

Tactic:
rw [idealRange_eq_lieSpan_range, h, ← LieSubalgebra.coe_toSubmodule, ←
  LieSubmodule.toSubmodule_inj, LieSubmodule.top_toSubmodule,
  LieSubalgebra.top_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : f.range = ⊤
⊢ ∃ N, ↑N = ⊤

Proof state:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : f.range = ⊤
⊢ ↑⊤ = ⊤

Tactic:
exact LieSubmodule.top_toSubmodule

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : f.range = ⊤
⊢ ∃ N, ↑N = ⊤

Tactic:
use ⊤

Result:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : f.range = ⊤
⊢ ↑⊤ = ⊤

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
⊢ f.idealRange = ⊤

Tactic:
rw [← f.range_eq_top] at h

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : f.range = ⊤
⊢ f.idealRange = ⊤
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma neg_of_smul_neg_right [SMulPosReflectLT α β] (h : a • b < 0) (hb : 0 ≤ b) : a < 0 :=
  lt_of_smul_lt_smul_right (by rwa [zero_smul]) hb

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : a • b < 0
hb : 0 ≤ b
⊢ a • b < 0 • b

Tactic:
rwa [zero_smul]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem isRotated_prev_eq {l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) :
    l.prev x hx = l'.prev x (h.mem_iff.mp hx)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.reverse.next x ⋯

Tactic:
exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev x hx = l'.prev x ⋯

Tactic:
rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]

Result:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.reverse.next x ⋯
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem Associates.mk_ne_zero' {R : Type*} [CommSemiring R] {r : R} :
    Associates.mk (Ideal.span {r} : Ideal R) ≠ 0 ↔ r ≠ 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0

Tactic:
rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesHasSum.sub {f g : ℕ → ℂ} {s a b : ℂ} (hf : LSeriesHasSum f s a)
    (hg : LSeriesHasSum g s b) :
    LSeriesHasSum (f - g) s (a - b)

Proof state:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f - g) s (a - b)

Tactic:
simpa [LSeriesHasSum, term_sub] using HasSum.sub hf hg

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem disjoint_pmap {p : α → Prop} {f : ∀ a : α, p a → β} {s t : List α}
    (hs : ∀ a ∈ s, p a) (ht : ∀ a ∈ t, p a)
    (hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a')
    (h : Disjoint s t) :
    Disjoint (s.pmap f hs) (t.pmap f ht)

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a ∈ t

Tactic:
rwa [hf a a' (hs a ha) (ht a' ha') ha''.symm]

Result:
no goals

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
⊢ ∀ ⦃a : β⦄, (∃ a_1 h, f a_1 ⋯ = a) → (∃ a_2 h, f a_2 ⋯ = a) → False

Tactic:
rintro b ⟨a, ha, rfl⟩ ⟨a', ha', ha''⟩

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ False

Tactic:
apply h ha

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a ∈ t

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
⊢ (pmap f s hs).Disjoint (pmap f t ht)

Tactic:
simp only [Disjoint, mem_pmap]

Result:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
⊢ ∀ ⦃a : β⦄, (∃ a_1 h, f a_1 ⋯ = a) → (∃ a_2 h, f a_2 ⋯ = a) → False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.IsExtensionBy_trans_left (state1 : State aig) (state2 : State aig)
    (state3 : State aig) (h12 : IsExtensionBy state1 state2 new1 hnew1)
    (h23 : IsExtensionBy state2 state3 new2 hnew2) : IsExtensionBy state1 state3 new1 hnew1

Proof state:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2

Tactic:
exact h23

Result:
no goals

Proof state:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1

Tactic:
exact h12

Result:
no goals

Proof state:
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.IsExtensionBy state3 new1 hnew1

Tactic:
apply  Cache.IsExtensionBy_trans_left

Result:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache.IsExtensionBy ?cache2 state3.cache ?new2 ?hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2
-- Mathlib/Order/Atoms.lean
theorem isAtom_iff' [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α}
    (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥) (h_atom : ∀ a, IsAtom a → u (l a) = a) (b : β) :
    IsAtom (u b) ↔ IsAtom b

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom (u b) ↔ IsAtom b

Tactic:
rw [← gi.isAtom_iff hbot h_atom, gi.l_u_eq]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem eq_of_eq (hg : ∀ y : S, IsUnit (g y)) {x y} (h : f.toMap x = f.toMap y) : g x = g y

Proof state:
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f.toMap x = f.toMap y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ g x = g y

Tactic:
rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.restrict S) hg c]

Result:
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f.toMap x = f.toMap y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.restrict S) hg) c)⁻¹ * (g.restrict S) c * g x = g y

Proof state:
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f.toMap x = f.toMap y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.restrict S) hg) c)⁻¹ * (g.restrict S) c * g x = g y

Tactic:
show _ * g c * _ = _

Result:
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f.toMap x = f.toMap y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.restrict S) hg) c)⁻¹ * g ↑c * g x = g y

Proof state:
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f.toMap x = f.toMap y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.restrict S) hg) c)⁻¹ * g ↑c * g x = g y

Tactic:
rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f.toMap x = f.toMap y
⊢ g x = g y

Tactic:
obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h

Result:
case intro
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f.toMap x = f.toMap y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ g x = g y
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem ae_lt_top_of_comp_ne_top (a : α) (hs : (η ∘ₖ κ) a s ≠ ∞) : ∀ᵐ b ∂κ a, η b s < ∞

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η b) s < ⊤

Tactic:
have h : ∀ᵐ b ∂κ a, η b (toMeasurable ((η ∘ₖ κ) a) s) < ∞ := by
  refine ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_
  rwa [← Kernel.comp_apply' _ _ _ (measurableSet_toMeasurable ..), measure_toMeasurable]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ⊤
h : ∀ᵐ (b : β) ∂κ a, (η b) (toMeasurable ((η ∘ₖ κ) a) s) < ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η b) s < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ⊤
h : ∀ᵐ (b : β) ∂κ a, (η b) (toMeasurable ((η ∘ₖ κ) a) s) < ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η b) s < ⊤

Tactic:
filter_upwards [h] with b hb using (measure_mono (subset_toMeasurable _ _)).trans_lt hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η b) (toMeasurable ((η ∘ₖ κ) a) s) < ⊤

Tactic:
refine ae_lt_top (Kernel.measurable_coe η (measurableSet_toMeasurable ..)) ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ⊤
⊢ ∫⁻ (x : β), (η x) (toMeasurable ((η ∘ₖ κ) a) s) ∂κ a ≠ ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : ((η ∘ₖ κ) a) s ≠ ⊤
⊢ ∫⁻ (x : β), (η x) (toMeasurable ((η ∘ₖ κ) a) s) ∂κ a ≠ ⊤

Tactic:
rwa [← Kernel.comp_apply' _ _ _ (measurableSet_toMeasurable ..), measure_toMeasurable]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem involute_comp_involute : involute.comp involute = AlgHom.id R (CliffordAlgebra Q)

Proof state:
case a.h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ((involute.comp involute).toLinearMap ∘ₗ ι Q) x✝ = ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) x✝

Tactic:
simp

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
⊢ involute.comp involute = AlgHom.id R (CliffordAlgebra Q)

Tactic:
ext

Result:
case a.h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ ((involute.comp involute).toLinearMap ∘ₗ ι Q) x✝ = ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) x✝
-- Mathlib/Order/Filter/Finite.lean
theorem iInf_sets_eq_finite {ι : Type*} (f : ι → Filter α) :
    (⨅ i, f i).sets = ⋃ t : Finset ι, (⨅ i ∈ t, f i).sets

Proof state:
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets

Tactic:
rw [iInf_eq_iInf_finset, iInf_sets_eq]

Result:
case h
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Directed (fun x1 x2 => x1 ≥ x2) fun t => ⨅ i ∈ t, f i

Proof state:
case h
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Directed (fun x1 x2 => x1 ≥ x2) fun t => ⨅ i ∈ t, f i

Tactic:
exact directed_of_isDirected_le fun _ _ => biInf_mono

Result:
no goals