harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
theorem PInfty_comp_PInftyToNormalizedMooreComplex (X : SimplicialObject A) :
    PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/RestrictGen.lean
theorem isClosed_iff (hS : RestrictGenTopology S) :
    IsClosed t ↔ ∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
t : Set X
hS : RestrictGenTopology S
⊢ IsClosed t ↔ ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)

Tactic:
simp only [← isOpen_compl_iff, hS.isOpen_iff, preimage_compl]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_comp (e : Basis ι A M) (f : M →ₗ[A] M) (v : ι → M) :
    e.det (f ∘ v) = (LinearMap.det f) * e.det v

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ e.det (⇑f ∘ v) = LinearMap.det f * e.det v

Tactic:
rw [Basis.det_apply, Basis.det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
  e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
  e.constr_comp]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma balance_idem (f : ι → G) : balance (balance f) = balance f

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
⊢ balance (balance f) = balance f

Tactic:
cases isEmpty_or_nonempty ι <;> ext x <;> simp [balance, expect_sub_distrib, univ_nonempty]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem compl_sInter (S : Set (Set α)) : (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Proof state:
α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Tactic:
rw [sUnion_eq_compl_sInter_compl, compl_compl_image]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_add_swap {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle y z + o.oangle x y = o.oangle x z

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle y z + o.oangle x y = o.oangle x z

Tactic:
rw [add_comm, o.oangle_add hx hy hz]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem natCast_ceil_eq_intCast_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : α) = ⌈a⌉

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ↑⌈a⌉

Tactic:
rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem continuousAt_oangle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
    ContinuousAt (fun y : V × V => o.oangle y.1 y.2) x

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y => o.oangle y.1 y.2) x

Tactic:
refine (Complex.continuousAt_arg_coe_angle ?_).comp ?_

Result:
case refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ (o.kahler x.1) x.2 ≠ 0

case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y => (o.kahler y.1) y.2) x

Proof state:
case refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ (o.kahler x.1) x.2 ≠ 0

Tactic:
exact o.kahler_ne_zero hx1 hx2

Result:
no goals

Proof state:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y => (o.kahler y.1) y.2) x

Tactic:
exact ((continuous_ofReal.comp continuous_inner).add
  ((continuous_ofReal.comp o.areaForm'.continuous₂).mul continuous_const)).continuousAt

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_admissibleIndex_iff {B : Box ι} {ν : ι → ℤ} :
    ν ∈ admissibleIndex n B ↔ box n ν ≤ B

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
⊢ ν ∈ admissibleIndex n B ↔ box n ν ≤ B

Tactic:
rw [admissibleIndex, Set.Finite.mem_toFinset, Set.mem_setOf_eq, Box.coe_subset_coe]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem invFunOn_neg (h : ¬∃ a ∈ s, f a = b) : invFunOn f s b = Classical.choice ‹Nonempty α›

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ¬∃ a ∈ s, f a = b
⊢ invFunOn f s b = Classical.choice inst✝

Tactic:
rw [invFunOn, dif_neg h]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem coe_sup' : ((s.sup' H f : α) : WithBot α) = s.sup ((↑) ∘ f)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
⊢ ↑(s.sup' H f) = s.sup (WithBot.some ∘ f)

Tactic:
rw [sup', WithBot.coe_unbot]

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Odd.smul_odd [Ring β] [AddCommGroup γ] [Module β γ] (hf : f.Odd) (hg : g.Odd) :
    (f • g).Even

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Even (f • g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = (f • g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f • g) (-a) = (f • g) a

Tactic:
simp only [Pi.smul_apply', hf a, hg a, smul_neg, neg_smul, neg_neg]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem nndist_equiv_symm_fst (x₁ x₂ : α) :
    nndist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) =
      nndist x₁ x₂

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ nndist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) = nndist x₁ x₂

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← WithLp.equiv_symm_sub, Prod.mk_sub_mk, sub_zero,
  nnnorm_equiv_symm_fst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_getThenInsertIfNew? [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α}
    {b : β a} (h : Raw.WFImp m.1) : Raw.WFImp (m.getThenInsertIfNew? a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.insertIfNewₘ a b).val

Tactic:
exact wfImp_insertIfNewₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.getThenInsertIfNew? a b).snd.val

Tactic:
rw [getThenInsertIfNew?_eq_insertIfNewₘ]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.insertIfNewₘ a b).val
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract.go₁_zero_utf8Len (s : List Char) : go₁ s 0 0 ⟨utf8Len s⟩ = s :=
  (go₁_append_right [] s 0 0 ⟨utf8Len s⟩ rfl).trans <| by
    simpa using go₂_append_left s [] 0 (utf8Len s) rfl

Proof state:
s : List Char
⊢ go₂ s { byteIdx := 0 } { byteIdx := utf8Len s } = s

Tactic:
simpa using go₂_append_left s [] 0 (utf8Len s) rfl

Result:
no goals
-- Mathlib/Algebra/Colimit/Module.lean
lemma congr_symm_apply_of (e : (i : ι) → G i ≃ₗ[R] G' i)
    (he : ∀ i j h, e j ∘ₗ f i j h = f' i j h ∘ₗ e i) {i : ι} (g : G' i) :
    (congr e he).symm (of _ _ G' f' i g) = of _ _ G f i ((e i).symm g) :=
  map_apply_of _ (fun i j h ↦ by
    rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
      refl_toLinearMap, comp_id]) _

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ ↑(e j).symm ∘ₗ f' i j h = f i j h ∘ₗ ↑(e i).symm

Tactic:
rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
  refl_toLinearMap, comp_id]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem Decidable.forall_or_right {q} {p : α → Prop} [Decidable q] :
    (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q

Proof state:
α : Sort u_1
q : Prop
p : α → Prop
inst✝ : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

Tactic:
simp [or_comm, Decidable.forall_or_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
⊢ (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem ZLattice.comap_discreteTopology [hL : DiscreteTopology L] {e : F →ₗ[K] E}
    (he₁ : Continuous e) (he₂ : Function.Injective e) :
    DiscreteTopology (ZLattice.comap K L e)

Proof state:
K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
hL : DiscreteTopology ↥L
e : F →ₗ[K] E
he₁ : Continuous ⇑e
he₂ : Function.Injective ⇑e
⊢ DiscreteTopology ↥(ZLattice.comap K L e)

Tactic:
exact DiscreteTopology.preimage_of_continuous_injective L he₁ he₂

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_ne_moveRight {G : PGame} [G.Impartial] (i : G.RightMoves) :
    grundyValue (G.moveRight i) ≠ grundyValue G

Proof state:
G : PGame
inst✝ : G.Impartial
i : G.RightMoves
⊢ (G.moveRight i).grundyValue ≠ G.grundyValue

Tactic:
convert grundyValue_ne_moveLeft (toLeftMovesNeg i) using 1 <;> simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma coe_lt_iff : a < y ↔ ∀ b : α, y = b → a < b

Proof state:
α : Type u_1
a : α
inst✝ : LT α
y : WithTop α
⊢ ↑a < y ↔ ∀ (b : α), y = ↑b → a < b

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y < π / 2)
    (hxy : x < y) : tan x < tan y :=
  tan_lt_tan_of_lt_of_lt_pi_div_two (by linarith) hy₂ hxy

Proof state:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ -(π / 2) < x

Tactic:
linarith

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem singleton_disjoint : Disjoint [a] l ↔ a ∉ l

Proof state:
α✝ : Type u_1
a : α✝
l : List α✝
⊢ [a].Disjoint l ↔ ¬a ∈ l

Tactic:
simp [Disjoint]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem toLinearEquiv_injective :
    Function.Injective (toLinearEquiv : (M₁ ≃SL[σ₁₂] M₂) → M₁ ≃ₛₗ[σ₁₂] M₂)

Proof state:
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
⊢ Function.Injective toLinearEquiv

Tactic:
rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl

Result:
case mk.mk
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝¹ : Continuous (↑e).toFun
continuous_invFun✝¹ : Continuous e.invFun
continuous_toFun✝ :
  Continuous
    (↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹,
            continuous_invFun := continuous_invFun✝¹ }.toLinearEquiv).toFun
continuous_invFun✝ :
  Continuous
    { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.invFun
⊢ { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    {
      toLinearEquiv :=
        { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹,
            continuous_invFun := continuous_invFun✝¹ }.toLinearEquiv,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }

Proof state:
case mk.mk
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝¹ : Continuous (↑e).toFun
continuous_invFun✝¹ : Continuous e.invFun
continuous_toFun✝ :
  Continuous
    (↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹,
            continuous_invFun := continuous_invFun✝¹ }.toLinearEquiv).toFun
continuous_invFun✝ :
  Continuous
    { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.invFun
⊢ { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    {
      toLinearEquiv :=
        { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹,
            continuous_invFun := continuous_invFun✝¹ }.toLinearEquiv,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsLimit.one_lt {o : Ordinal} (h : IsLimit o) : 1 < o

Proof state:
o : Ordinal.{u_4}
h : o.IsLimit
⊢ 1 < o

Tactic:
simpa only [succ_zero] using h.succ_lt h.pos

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Semiconj.lean
lemma zpow_right₀ {a x y : G₀} (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
  | (n : ℕ) => by simp [h.pow_right n]
  | .negSucc n => by simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]

Proof state:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)

Tactic:
simp [h.pow_right n]

Result:
no goals

Proof state:
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_sshiftRight {b : BitVec w} :
    ~~~b.sshiftRight n = (~~~b).sshiftRight n

Proof state:
w n : Nat
b : BitVec w
⊢ ~~~b.sshiftRight n = (~~~b).sshiftRight n

Tactic:
ext i

Result:
case pred
w n : Nat
b : BitVec w
i : Nat
a✝ : i < w
⊢ (~~~b.sshiftRight n).getLsbD i = ((~~~b).sshiftRight n).getLsbD i

Proof state:
case pred
w n : Nat
b : BitVec w
i : Nat
a✝ : i < w
⊢ (~~~b.sshiftRight n).getLsbD i = ((~~~b).sshiftRight n).getLsbD i

Tactic:
simp only [getLsbD_not, Fin.is_lt, decide_true, getLsbD_sshiftRight, Bool.not_and, Bool.not_not,
  Bool.true_and, msb_not]

Result:
case pred
w n : Nat
b : BitVec w
i : Nat
a✝ : i < w
⊢ (decide (i < w) && (decide (w ≤ i) || !if n + i < w then b.getLsbD (n + i) else b.msb)) =
    (!decide (w ≤ i) && if n + i < w then decide (n + i < w) && !b.getLsbD (n + i) else decide (0 < w) && !b.msb)

Proof state:
case pred
w n : Nat
b : BitVec w
i : Nat
a✝ : i < w
⊢ (decide (i < w) && (decide (w ≤ i) || !if n + i < w then b.getLsbD (n + i) else b.msb)) =
    (!decide (w ≤ i) && if n + i < w then decide (n + i < w) && !b.getLsbD (n + i) else decide (0 < w) && !b.msb)

Tactic:
by_cases h : w ≤ i
<;> by_cases h' : n + i < w
<;> by_cases h'' : 0 < w
<;> simp [h, h', h'']
<;> omega

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_subset (x y : E × F) :
    openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Tactic:
exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_add_mul_left_left (h : IsCoprime (x + y * z) y) : IsCoprime x y :=
  let ⟨a, b, H⟩ := h
  ⟨a, a * z + b, by
    simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm,
      mul_left_comm] using H⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
a b : R
H : a * (x + y * z) + b * y = 1
⊢ a * x + (a * z + b) * y = 1

Tactic:
simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm,
  mul_left_comm] using H

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bodd_mul (m n : ℤ) : bodd (m * n) = (bodd m && bodd n)

Proof state:
m n : ℤ
⊢ (m * n).bodd = (m.bodd && n.bodd)

Tactic:
rcases m with m | m <;> rcases n with n | n <;>
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
           negSucc_mul_negSucc] <;>
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_mul]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma of_eq_top {P : MorphismProperty C} (h : P = ⊤) {X Y : C} (f : X ⟶ Y) : P f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P = ⊤
X Y : C
f : X ⟶ Y
⊢ P f

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/CompleteField.lean
theorem lt_inducedMap_iff : b < inducedMap α β a ↔ ∃ q : ℚ, b < q ∧ (q : α) < a :=
  ⟨fun h => (exists_rat_btwn h).imp fun _ => And.imp_right coe_lt_inducedMap_iff.1,
    fun ⟨q, hbq, hqa⟩ => hbq.trans <| by rwa [coe_lt_inducedMap_iff]⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
a : α
b : β
x✝ : ∃ q, b < ↑q ∧ ↑q < a
q : ℚ
hbq : b < ↑q
hqa : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
rwa [coe_lt_inducedMap_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_equation (hf : Function.Injective f) :
    (W'.baseChange B).toAffine.Equation (f x) (f y) ↔ (W'.baseChange A).toAffine.Equation x y

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
hf : Function.Injective ⇑f
⊢ (baseChange W' B).toAffine.Equation (f x) (f y) ↔ (baseChange W' A).toAffine.Equation x y

Tactic:
rw [← map_equation _ _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem toRel_symmetric (s : Set (Sym2 α)) : Symmetric (ToRel s) := fun x y => by simp [eq_swap]

Proof state:
α : Type u_1
s : Set (Sym2 α)
x y : α
⊢ ToRel s x y → ToRel s y x

Tactic:
simp [eq_swap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem replaceEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
    {v' : β k'} (h : (k' == k) = false) :
    replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: replaceEntry k v l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
⊢ replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: replaceEntry k v l

Tactic:
simp [replaceEntry, h]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonpos_of_nonpos_of_nonneg [SMulPosMono α β] (ha : a ≤ 0) (hb : 0 ≤ b) : a • b ≤ 0

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

Tactic:
simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem dist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
    dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖

Proof state:
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖

Tactic:
rw [dist_eq_norm_div, Set.apply_mulIndicator_symmDiff norm_inv']

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem _root_.LinearIndependent.rank_matrix [Field R] [Fintype m]
    {M : Matrix m n R} (h : LinearIndependent R M) : M.rank = Fintype.card m

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Fintype m
M : Matrix m n R
h : LinearIndependent R M
⊢ M.rank = Fintype.card m

Tactic:
rw [M.rank_eq_finrank_span_row, linearIndependent_iff_card_eq_finrank_span.mp h, Set.finrank]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[reassoc]
lemma comp_homOfVector {X Y : Scheme} (v : n → Γ(Y, ⊤)) (f : X ⟶ Y) (g : Y ⟶ S) :
    f ≫ homOfVector g v = homOfVector (f ≫ g) (f.appTop ∘ v)

Proof state:
n : Type v
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
⊢ f ≫ homOfVector g v = homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v)

Tactic:
ext1 <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem neg (f : ContDiffBump (0 : E)) (x : E) : f (-x) = f x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
f : ContDiffBump 0
x : E
⊢ ↑f (-x) = ↑f x

Tactic:
simp_rw [← zero_sub, f.sub, zero_add]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem isClosed_iff' (hf : IsInducing f) {s : Set X} :
    IsClosed s ↔ ∀ x, f x ∈ closure (f '' s) → x ∈ s

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed s ↔ ∀ (x : X), f x ∈ closure (f '' s) → x ∈ s

Tactic:
rw [hf.eq_induced, isClosed_induced_iff']

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Nat.lean
lemma isCompl_even_odd : IsCompl { n : ℕ | Even n } { n | Odd n }

Proof state:
⊢ IsCompl {n | Even n} {n | Odd n}

Tactic:
simp only [← Set.compl_setOf, isCompl_compl, ← not_even_iff_odd]

Result:
no goals