harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Basic.lean
theorem xor_iff_or_and_not_and (a b : Prop) : Xor' a b ↔ (a ∨ b) ∧ (¬ (a ∧ b))

Proof state:
a b : Prop
⊢ Xor' a b ↔ (a ∨ b) ∧ ¬(a ∧ b)

Tactic:
rw [Xor', or_and_right, not_and_or, and_or_left, and_not_self_iff, false_or,
  and_or_left, and_not_self_iff, or_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_ushiftRight (x : BitVec w) (i n : Nat) (h : i < w) :
    (x >>> n)[i] = x.getLsbD (n + i)

Proof state:
w : Nat
x : BitVec w
i n : Nat
h : i < w
⊢ (x >>> n)[i] = x.getLsbD (n + i)

Tactic:
simp [getElem_eq_testBit_toNat, toNat_ushiftRight, Nat.testBit_shiftRight, getLsbD]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem measure_eq_iSup (H : InnerRegularWRT μ p q) (hU : q U) :
    μ U = ⨆ (K) (_ : K ⊆ U) (_ : p K), μ K

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
⊢ μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K

Tactic:
refine
  le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
r : ℝ≥0∞
hr : r < μ U
⊢ r < ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
r : ℝ≥0∞
hr : r < μ U
⊢ r < ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K

Tactic:
simpa only [lt_iSup_iff, exists_prop] using H hU r hr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem unsat_relabel {f : CNF α} (r : α → β) (h : Unsat f) :
    Unsat (relabel r f)

Proof state:
α : Type u_1
β : Type u_2
f : CNF α
r : α → β
h : f.Unsat
⊢ (relabel r f).Unsat

Tactic:
simp_all [unsat_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem mem_lifts_iff_mem_alg (R : Type u) [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S]
    (p : S[X]) : p ∈ lifts (algebraMap R S) ↔ p ∈ AlgHom.range (@mapAlg R _ S _ _)

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
⊢ p ∈ lifts (algebraMap R S) ↔ p ∈ (mapAlg R S).range

Tactic:
simp only [coe_mapRingHom, lifts, mapAlg_eq_map, AlgHom.mem_range, RingHom.mem_rangeS]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalComp_cons (α : f ≅ g) (η : g ⟶ h) {ηs : h ⟶ i} {θ : i ⟶ j} {ι : h ⟶ j}
    (e_ι : ηs ≫ θ = ι)  :
    (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h i j : a ⟶ b
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
simp [e_ι]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem one_le_norm_mul_norm_symm [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :
    1 ≤ ‖(e : E →SL[σ₁₂] F)‖ * ‖(e.symm : F →SL[σ₂₁] E)‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑e.symm‖ * ‖↑e‖

Tactic:
convert (e.symm : F →SL[σ₂₁] E).opNorm_comp_le (e : E →SL[σ₁₂] F)

Result:
case h.e'_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 = ‖(↑e.symm).comp ↑e‖

Proof state:
case h.e'_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 = ‖(↑e.symm).comp ↑e‖

Tactic:
rw [e.coe_symm_comp_coe, ContinuousLinearMap.norm_id]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑e‖ * ‖↑e.symm‖

Tactic:
rw [mul_comm]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑e.symm‖ * ‖↑e‖
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bddAbove_range_comp {ι : Type u} {f : ι → Ordinal.{v}} (hf : BddAbove (range f))
    (g : Ordinal.{v} → Ordinal.{max v w}) : BddAbove (range (g ∘ f))

Proof state:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (range (g ∘ f))

Tactic:
rw [range_comp]

Result:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (g '' range f)

Proof state:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
exact bddAbove_image hf g

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_id (p : G.Walk u v) : p.map Hom.id = p

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Walk.map Hom.id p = p

Tactic:
induction p with
| nil => rfl
| cons _ p' ih => simp [ih]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Walk.map Hom.id nil = nil

Tactic:
rfl

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : Walk.map Hom.id p' = p'
⊢ Walk.map Hom.id (cons h✝ p') = cons h✝ p'

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Defs.lean
theorem OrderedCommGroup.toMulLeftReflectLE (α : Type u) [OrderedCommGroup α] :
    MulLeftReflectLE α where
      elim a b c bc

Proof state:
α : Type u
inst✝ : OrderedCommGroup α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c

Tactic:
simpa using mul_le_mul_left' bc a⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (insertEntry k v l).isEmpty = false

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ (insertEntry k v l).isEmpty = false

Tactic:
rw [insertEntry_of_containsKey h, isEmpty_replaceEntry, isEmpty_eq_false_of_containsKey h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (insertEntry k v l).isEmpty = false

Tactic:
cases h : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ (insertEntry k v l).isEmpty = false

case true
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ (insertEntry k v l).isEmpty = false

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ (insertEntry k v l).isEmpty = false

Tactic:
simp [insertEntry_of_containsKey_eq_false h]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem zero_CNF {o : Ordinal} (ho : o ≠ 0) : CNF 0 o = [(0, o)]

Proof state:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 0 o = [(0, o)]

Tactic:
simp [CNF_ne_zero ho]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_of_lf_of_le {x y z : PGame} (h₁ : x ⧏ y) (h₂ : y ≤ z) : x ⧏ z

Proof state:
x y z : PGame
h₁ : x ⧏ y
h₂ : y ≤ z
⊢ x ⧏ z

Tactic:
rw [← PGame.not_le] at h₁ ⊢

Result:
x y z : PGame
h₁ : ¬y ≤ x
h₂ : y ≤ z
⊢ ¬z ≤ x

Proof state:
x y z : PGame
h₁ : ¬y ≤ x
h₂ : y ≤ z
⊢ ¬z ≤ x

Tactic:
exact fun h₃ => h₁ (h₂.trans h₃)

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem subset_center_units : ((↑) : Mˣ → M) ⁻¹' center M ⊆ Set.center Mˣ :=
  fun _ ha => by
  rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← Units.eq_iff, Units.val_mul, Units.val_mul, ha.comm]

Proof state:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ g✝ * x✝ = x✝ * g✝

Tactic:
rw [← Units.eq_iff, Units.val_mul, Units.val_mul, ha.comm]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
⊢ ∀ (g : Mˣ), g * x✝ = x✝ * g

Tactic:
intro _

Result:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ g✝ * x✝ = x✝ * g✝

Proof state:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
⊢ x✝ ∈ center Mˣ

Tactic:
rw [_root_.Semigroup.mem_center_iff]

Result:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
⊢ ∀ (g : Mˣ), g * x✝ = x✝ * g
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_eq_matrix_trace_of_finset {s : Finset M} (b : Basis s R M) (f : M →ₗ[R] M) :
    trace R M f = Matrix.trace (LinearMap.toMatrix b b f)

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
have : ∃ s : Finset M, Nonempty (Basis s R M) := ⟨s, ⟨b⟩⟩

Result:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R M) f = ((toMatrix b b) f).trace

Proof state:
case e_a
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ traceAux R ⋯.some = traceAux R b

Tactic:
apply traceAux_eq

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
rw [trace, dif_pos this, ← traceAux_def]

Result:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (traceAux R ⋯.some) f = (traceAux R b) f

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (traceAux R ⋯.some) f = (traceAux R b) f

Tactic:
congr 1

Result:
case e_a
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ traceAux R ⋯.some = traceAux R b
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
@[simp] lemma op_boundaryLE_iff {j : ι} : e.op.BoundaryLE j ↔ e.BoundaryGE j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
⊢ e.op.BoundaryLE j ↔ e.BoundaryGE j

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_smul (a : R) : (a • p).mirror = a • p.mirror

Proof state:
R : Type u_1
inst✝¹ : Ring R
p : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ (a • p).mirror = a • p.mirror

Tactic:
rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_modifyKey_self [EquivBEq α] {k : α} {fallback : β} {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
    getValueD k (modifyKey k f l) fallback = ((getValue? k l).map f).getD fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
fallback : β
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValueD k (modifyKey k f l) fallback = (Option.map f (getValue? k l)).getD fallback

Tactic:
simp [getValueD_modifyKey, hl]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerLeft_nil (f : a ⟶ b) {g h : b ⟶ c} (α : g ≅ h) :
    (whiskerLeftIso f α).hom = (whiskerLeftIso f α).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
α : g ≅ h
⊢ (whiskerLeftIso f α).hom = (whiskerLeftIso f α).hom

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
lemma swap_mulVec (i j : n) (a : n → R) :
    swap R i j *ᵥ a = a ∘ Equiv.swap i j

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ swap R i j *ᵥ a = a ∘ ⇑(Equiv.swap i j)

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
@[simp]
lemma pullback_mem_iff_of_isIso {i : X ⟶ Y} [IsIso i] {S : Sieve Y} :
    S.pullback i ∈ J _ ↔ S ∈ J _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S ∈ J Y

Tactic:
convert J.pullback_stable (inv i) H

Result:
case h.e'_5
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S = Sieve.pullback (inv i) (Sieve.pullback i S)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
⊢ Sieve.pullback i S ∈ J X ↔ S ∈ J Y

Tactic:
refine ⟨fun H ↦ ?_, J.pullback_stable i⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S ∈ J Y

Proof state:
case h.e'_5
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S = Sieve.pullback (inv i) (Sieve.pullback i S)

Tactic:
rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂ : List α} :
    ¬ Lex r (a :: l₁) (b :: l₂) ↔ (¬ r a b ∧ a ≠ b) ∨ (¬ r a b ∧ ¬ Lex r l₁ l₂)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidableRel r
a b : α
l₁ l₂ : List α
⊢ ¬Lex r (a :: l₁) (b :: l₂) ↔ ¬r a b ∧ a ≠ b ∨ ¬r a b ∧ ¬Lex r l₁ l₂

Tactic:
rw [cons_lex_cons_iff, not_or, Decidable.not_and_iff_or_not, and_or_left]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_inj' (h : 1 < n ∨ 1 < m) : n ! = m ! ↔ n = m

Proof state:
case inl
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
exact factorial_inj hn

Result:
no goals

Proof state:
m n : ℕ
h : 1 < n ∨ 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
obtain hn|hm := h

Result:
case inl
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

case inr
m n : ℕ
hm : 1 < m
⊢ n ! = m ! ↔ n = m

Proof state:
case inr
m n : ℕ
hm : 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
rw [eq_comm, factorial_inj hm, eq_comm]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem eq_empty_of_not_terminates {s} (H : ¬Terminates s) : s = empty α

Proof state:
case a.h.some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : ↑s n = some val✝
⊢ some val✝ = ↑(empty α) n

Tactic:
refine absurd ?_ H

Result:
case a.h.some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : ↑s n = some val✝
⊢ s.Terminates

Proof state:
case a
α : Type u
s : Computation α
H : ¬s.Terminates
⊢ ↑s = ↑(empty α)

Tactic:
funext n

Result:
case a.h
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
⊢ ↑s n = ↑(empty α) n

Proof state:
α : Type u
s : Computation α
H : ¬s.Terminates
⊢ s = empty α

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
s : Computation α
H : ¬s.Terminates
⊢ ↑s = ↑(empty α)

Proof state:
case a.h.some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : ↑s n = some val✝
⊢ s.Terminates

Tactic:
exact ⟨⟨_, _, h.symm⟩⟩

Result:
no goals

Proof state:
case a.h
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
⊢ ↑s n = ↑(empty α) n

Tactic:
induction' h : s.val n with _

Result:
case a.h.none
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
h : ↑s n = none
⊢ none = ↑(empty α) n

case a.h.some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : ↑s n = some val✝
⊢ some val✝ = ↑(empty α) n

Proof state:
case a.h.none
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
h : ↑s n = none
⊢ none = ↑(empty α) n

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem not_lt {a b : ℚ} : ¬a < b ↔ b ≤ a

Proof state:
a b : ℚ
⊢ ¬a < b ↔ b ≤ a

Tactic:
rw [← Rat.not_le, not_not]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem hasNext_cons_addChar (c : Char) (cs : List Char) (i : Pos) :
    hasNext ⟨⟨c :: cs⟩, i + c⟩ = hasNext ⟨⟨cs⟩, i⟩

Proof state:
c : Char
cs : List Char
i : Pos
⊢ { s := { data := c :: cs }, i := i + c }.hasNext = { s := { data := cs }, i := i }.hasNext

Tactic:
simp [hasNext, Nat.add_lt_add_iff_right]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem continuousOn_iff [PseudoMetricSpace β] {f : α → β} {s : Set α} :
    ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_reverse (f : α → β) (l : Vector α n) : l.reverse.map f = (l.map f).reverse

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
⊢ map f l.reverse = (map f l).reverse

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f { toArray := l, size_toArray := ⋯ }.reverse = (map f { toArray := l, size_toArray := ⋯ }).reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f { toArray := l, size_toArray := ⋯ }.reverse = (map f { toArray := l, size_toArray := ⋯ }).reverse

Tactic:
simp [Array.map_reverse]

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
@[simp] lemma toLowerSet_specializes_toLowerSet {a b : α} :
    toLowerSet a ⤳ toLowerSet b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toLowerSet a ⤳ toLowerSet b ↔ a ≤ b

Tactic:
simp_rw [specializes_iff_closure_subset, IsLowerSet.closure_singleton, Ici_subset_Ici,
  toLowerSet_le_iff]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem mul_inv_cancel (x : R[R⁰⁻¹]) (h : x ≠ 0) : x * x⁻¹ = 1

Proof state:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if h : False then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Tactic:
apply OreLocalization.mul_inv ⟨r, _⟩

Result:
no goals

Proof state:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ r /ₒ s * (r /ₒ s)⁻¹ = 1

Tactic:
rw [OreLocalization.inv_def, OreLocalization.one_def]

Result:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Proof state:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Tactic:
simp only [hr]

Result:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if h : False then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R⁰ R
h : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
induction' x with r s

Result:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ r /ₒ s * (r /ₒ s)⁻¹ = 1

Proof state:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Tactic:
have hr : r ≠ 0 := by
  rintro rfl
  simp at h

Result:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
s : ↥R⁰
h : 0 /ₒ s ≠ 0
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ r ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
s : ↥R⁰
h : 0 /ₒ s ≠ 0
⊢ False

Proof state:
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if h : False then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Tactic:
with_unfolding_all apply OreLocalization.mul_inv ⟨r, _⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowingε₀_zero : fastGrowingε₀ 0 = 1

Proof state:
⊢ fastGrowingε₀ 0 = 1

Tactic:
simp [fastGrowingε₀]

Result:
no goals
-- Mathlib/Algebra/Polynomial/CoeffMem.lean
lemma idealSpan_range_update_divByMonic (hij : i ≠ j) (v : ι → R[X]) (hi : (v i).Monic) :
    span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v)

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
hi : (v i).Monic
⊢ span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v)

Tactic:
rw [modByMonic_eq_sub_mul_div _ hi, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
  Submodule.span_range_update_sub_smul hij]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem cast_eq_cast {i j} (h : i = j) :
    ⇑(cast R M h) = _root_.cast (congrArg (fun i => ⨂[R]^i M) h)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ⇑(cast R M ⋯) = _root_.cast ⋯

Tactic:
rw [cast_refl]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ⇑(LinearEquiv.refl R (⨂[R]^i M)) = _root_.cast ⋯

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
h : i = j
⊢ ⇑(cast R M h) = _root_.cast ⋯

Tactic:
subst h

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ⇑(cast R M ⋯) = _root_.cast ⋯

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ⇑(LinearEquiv.refl R (⨂[R]^i M)) = _root_.cast ⋯

Tactic:
rfl

Result:
no goals